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 HomotopyTypeTheory+unsub...@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 HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.