[Agda] Stymied by a proof irrelevance requirement

Dan Licata drl at cs.cmu.edu
Wed Apr 3 17:46:07 CEST 2013

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


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

More information about the Agda mailing list