[Agda] Stymied by a proof irrelevance requirement

[Nils Anders Danielsson]

On 2013-04-02 03:36, Jacques Carette wrote:
> Also, might it be a good idea to "upgrade" the standard library's
> cong₂ to this dependent version?

The dependent one is often more awkward to use. The awkwardness would
disappear if one could make

   subst (λ _ → B) eq x

reduce to x. Perhaps Conor McBride or Dan Licata know how this can be
accomplished.

One can prove a dependent cong using the non-dependent one, uncurry, and
the following characterisation of equality of pairs (where p₁, p₂ :
Σ A B):

   p₁ ≡ p₂
     ↔
   ∃ λ (p : proj₁ p₁ ≡ proj₁ p₂) → subst B p (proj₂ p₁) ≡ proj₂ p₂

I don't think I've included this proof in the standard library. It is
part of my library for use with --without-K.

Note that in OTT heterogeneous equality of pairs is defined so that the
left-hand side of the bijection above computes to something like the
right-hand side.

-- 
/NAD