[Agda] Stymied by a proof irrelevance requirement
Nils Anders Danielsson
nad at chalmers.se
Tue Apr 2 12:28:48 CEST 2013
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
More information about the Agda
mailing list