[Agda] Injectivity of Constructors?

[Nils Anders Danielsson]

On Tue, Apr 1, 2008 at 3:03 AM, Shin-Cheng Mu <scm at iis.sinica.edu.tw> wrote:
>
>  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?

This would amount to a lot of boring boiler-plate code. If we had
better support for polytypic programming, like Epigram 2 will have,
then it should be possible to replace these lemmas with something more
general.

However, currently Agda doesn't support polytypic programming, so feel
free to submit library patches.

> 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.

One option is to use heterogeneous equality instead:

pair-injective
  : {A₁ : Set} {B₁ : A₁ -> Set} {p₁ : Σ A₁ B₁}
    {A₂ : Set} {B₂ : A₂ -> Set} {p₂ : Σ A₂ B₂} ->
    p₁ ≅ p₂ -> proj₁ p₁ ≅ proj₁ p₂ × proj₂ p₁ ≅ proj₂ p₂
pair-injective ≅-refl = (≅-refl , ≅-refl)

-- 
/NAD