Являются ли конструкторы непересекающимися в Агда? (или как опровергнуть inj₁ x ≡ inj₂ y)

Question

Мне нужна еще одна лемма, показывающая, что inj₁ x ≡ inj₂ y абсурден как часть более крупной теоремы о типах несвязных объединений (⊎) в Агда.

Этот результат будет следовать непосредственно из двух конструкторов для ⊎, а именно inj₁ и inj₂, будучи не пересекаются. Это дело в Агда? Как мне это доказать?

Вот полная лемма:

open import Relation.Nullary 
open import Relation.Binary.PropositionalEquality 
open import Data.Sum 


lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y 
lemma eq = ? 

Answer 1

Конструкторы типа данных не пересекаются. Я бы сказал, что это теорема в метатеории типа Агды.

Вы можете попробовать СЛУЧАЙ eq доказательства (C-c C-c), и Agda найти противоречие:

lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y 
lemma() 

Это счастливо-проверку типа.