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

[Martin Escardo <escardo...@googlemail.com>]

I've been asking myself a similar question for some time now, and
perhaps it is the time to share it, although I was waiting to have a
more precise formulation, which I still don't. (So fill free to improve
my question or to say why it can't be answered.)

The nature of the type Id U X Y, in MLTT, is under-specified by the
(intensional) MLTT "axioms".

Maybe isProp(Id U X Y). This is the K-axiom (for the universe U).

Maybe Id U X Y is canonically equivalent to the type X~Y of
equivalences. This is the univalence axiom (for the universe U).

Maybe ... many more interesting things are possible? What else is
consistent beyond K and univalence, and possibly interesting?

Some people like the K-axiom for U because ... (let them fill the answer).

We like the univalence axiom for U because, "magically", it makes Id
behave as we think equality should behave (equality of groups should be
group isomorphism, for instance, and it is, under univalence).

But ... can we avoid the magical aspect?

Can we stare at the type (Id U X Y) objectively, mathematically, say
within intensional MLTT, where it was introduced, and, internally in
MLTT, ponder what it can be, and identify the only "compelling" thing it
can be as the type of equivalences X~Y, where "compelling" is a notion
remote from univalence?

At the moment, univalence is "experimentally" interesting/compelling: it
gives function extensionality, it gives propositional extensionality, it
gives that the fundamental group of the circle HIT is Z, it gives that
equality of categories is categorical equivalence, and much more.

But can we "ultimately" justify it as the "intrinsically mathematically
appealing" determination of Id U X Y, before we consider the interesting
experimental consequences?

Martin



On 06/09/16 14:44, Andrew Polonsky wrote:
> These are all good points.  I now have an exhaustive answer to my
> motivating question.
>
> Thanks,
> Andrew
>
> On Tue, Sep 6, 2016 at 2:57 PM, Peter LeFanu Lumsdaine
> <p.l.lu...@gmail.com> wrote:
>> 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.
>>
>>
>