В Агде конструкторы не пересекаются? (или как опровергнуть травму)

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) и Агда найдет противоречие

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

Это радостно проверено.