Are constructors disjoint in Agda? (or how to refute harm)

Question

I need another lemma showing that it inj₁ x ≡ inj₂ yis absurd as part of a larger theorem on disjoint union types ( ⊎) in Agda.

This result will directly follow from two constructors ⊎, namely, inj₁and inj₂, as a disjunct. Is that the case at Agda? How to 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 = ?

Answer 1

Data type constructors do not overlap. I would say that this is a theorem in a metatheory like Agda.

eq (C-c C-c), Agda :

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

.