Re: [HoTT] A puzzle about "univalent equality"

[Dan Licata <d...@cs.cmu.edu>]

and the issue only comes up if you don’t have K, which would equate (ap (λ u → u True True) e) and Refl

-Dan

> On Sep 6, 2016, at 8:32 AM, Michael Shulman <shu...@sandiego.edu> wrote:
> 
> Although, as Voevodsky showed, weak funext implies strong funext.
> 
> On Tue, Sep 6, 2016 at 12:30 AM, Andrew Polonsky
> <andrew....@gmail.com> wrote:
>> Thanks, Mike and Dan.  And congratulations on giving essentially
>> identical solutions at essentially identical times, in two different
>> languages!
>> 
>>> I would be very surprised if there was something like this that was not provable in "book HoTT”.
>> 
>> I believe there can't be, either.  But maybe this "belief" is really a
>> matter of definition, in that the equalities which are "supposed to"
>> hold, are precisely those which can be derived in book HoTT.
>> 
>> What I find subtle in the above example is that it apparently cannot
>> be done with the "pre-HoTT" FunExt axiom; you need to use the stronger
>> formulation, that the canonical map (f=g -> f==g) is an equivalence,
>> to make the transports compute.
>> 
>> Cheers,
>> Andrew
>> 
>> --
>> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
>> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
>> For more options, visit https://groups.google.com/d/optout.
> 
> -- 
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.