[Agda] Injectivity of Constructors?

[Shin-Cheng Mu]

Hi,

Every once in a while I find myself needing a proof of, for
example, b ≡ b', while having only proved inj₂ b ≡ inj₂ b'.
Do you think should each data constructor defined in the
standard library come with a proposition that it is injective?

For inj₂, this will do:

   inj₂-injective : {A B : Set}{b b' : B} ->
        inj₂ {A}{B} b ≡ inj₂ b' -> b ≡ b'
   inj₂-injective ≡-refl = ≡-refl

I thought these propositions are easy but they turn out to
be not always trivial. In pair-injective below, for example:

   pair-injective : {A B : Set}{a a' : A}{b b' : B} ->
      _,_ {A}{\_ -> B} a b ≡ (a' , b') -> (a ≡ a') × (b ≡ b')
   pair-injective ≡-refl = (≡-refl , ≡-refl)

It is probably pointless to generalise the first explicit
argument to:

   _,_ {A}{B} a b ≡ (a' , b')  where B : A -> Set

because we would need a proof of a ≡ a' in the first place
to show that B a and B a' yield the same type.

sincerely,
Shin