constructor - Agda 中的构造函数是不相交的吗？（或如何反驳 inj₁ x ≡ inj₂ y）

Answer 1

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.