[Agda] Stymied by a proof irrelevance requirement

[Dan Licata]

That 'subst' at a constant function is the identity is definitely part
of the computational story about homotopy type theory, but I don't have
anything implementable for you yet.

BTW, the HoTT answer to Jacques' original question is that,
if you uncurry it, your singleton constructor takes 
something of type Sigma y:A. x = y, and this type 
is contractible, and therefore any two elements of it
are equal (see e.g. here
http://homotopytypetheory.org/2011/04/10/just-kidding-understanding-identity-elimination-in-homotopy-type-theory/
)
So the proof irrelevance that you're using here is really valid for all
spaces---it's not necessary that the identity type be treated
irrelevantly.  

-Dan


On Apr02, Nils Anders Danielsson wrote:
> 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.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda