I need one more lemma showing that inj₁ x ≡ inj₂ y
is absurd as part of a larger theorem about disjoint union types (⊎
) in Agda.
This result would follow directly from the two constructors for ⊎
, namely inj₁
and inj₂
, being disjoint. Is that the case in Agda? How do I prove it?
Here is the complete lemma:
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 = ?
The data type constructors are disjoint. I'd say it's a theorem in Agda's type-system meta-theory.
You can try to case the eq
proof (C-c C-c
), and Agda will find the contradiction:
lemma : ∀ {a b} {A : Set a} {B : Set b} {x : A} {y : B} → ¬ inj₁ x ≡ inj₂ y
lemma ()
This happily type-checks.