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

[Peter LeFanu Lumsdaine <p.l.lu...@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2785 bytes --]

On Tue, Sep 6, 2016 at 2:32 PM, Michael Shulman <shu...@sandiego.edu>
wrote:

> Although, as Voevodsky showed, weak funext implies strong funext.


Just to clarify, though, this *doesn’t*  mean that Andews’ original goal
“proj1 Y = tt” is necesarily inhabited, if the funext witness used early in
his development is taken just from weak funext.

The proof “weak funext implies strong funext” shows that given some witness
funext0 of weak funext (i.e. funext0 : (forall X Y f g, f == g -> f = g)),
then you can construct some new witness funext1, which additionally is a
(two-sided) inverse for the canonical map the other way (“ap10” in the
current HoTT library).  (I blogged the details here:
https://homotopytypetheory.org/2011/12/19/strong-funext-from-weak/)

But it *doesn’t* show that the original witness funext0 is an inverse for
ap10, and indeed the proof points to how this may fail: funext0 might
conjugate paths by some family of non-trivial loops in the codomain type.
Andrew’s original goal “proj1 Y = tt” depends on the witness used earlier
for funext — so if that witness happens to conjugate paths Bool –> Bool in
Type by the non-trivial auto-equivalence of Bool, then one could have proj1
Y = ff.

–p.



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

[-- Attachment #2: Type: text/html, Size: 4016 bytes --]