Re: [HoTT] Yet another characterization of univalence

[Evan Cavallo <evanc...@gmail.com>]

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

>
> Can you show the converse?
>

I don't think so (or at least, I don't see how it could be done).

Evan

2017-11-29 17:12 GMT-05:00 Martín Hötzel Escardó <m.es...@cs.bham.ac.uk>:

>
>
> On 29/11/17 21:12, Evan Cavallo wrote:
>
>> Maybe this is interesting: assuming funext, if the canonical map Id A B
>> -> A ≃ B is an embedding for all A,B, then Martin's axiom holds. Since Id x
>> y is always equivalent to (Π(z:X), Id x z ≃ Id y z), showing that it is
>> equivalent to Id (Id x) (Id y) can be reduced to showing that the map Id
>> (Id x) (Id y) -> (Π(z:X), Id x z ≃ Id y z) is an embedding.
>>
>> Id A B -> A ≃ B is an embedding both if univalence holds and if axiom K
>> holds.
>>
>
>
> I like it. You say that (assuming funext) if idtoeq : (A B : U) -> A = B
> -> A ≃ B is a natural embedding (rather than an equivalence as the
> univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for all
> X:U.
>
> Can you show the converse?
>
> Martin
>
>
>
>> Evan
>>
>> 2017-11-28 4:40 GMT-05:00 Andrej Bauer <andrej...@andrej.com <mailto:
>> andrej...@andrej.com>>:
>>
>>     > If univalence holds, then Id : X -> (X -> U) is an embedding.
>>     >
>>     > But If the K axiom holds, then again Id : X -> (X -> U) is an
>> embedding.
>>     >
>>     > And hence there is no hope to deduce univalence from the fact that
>> Id_X is
>>     > an embedding for every X:U.
>>     >
>>     > (And, as a side remark, I can't see how to prove that Id_X is an
>> embedding
>>     > without using K or univalence.)
>>
>>     So you've invented a new axiom?
>>
>>        Escardo's axiom: Id : X → (X → U) is an embedding.
>>
>>     (We could call it Martin's axiom to create lots of confusion.)
>>
>>     With kind regards,
>>
>>     Andrej
>>
>>     --
>>     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
>>     <mailto:HomotopyTypeTheo...@googlegroups.com>.
>>     For more options, visit https://groups.google.com/d/optout
>>     <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 <mailto:
>> HomotopyTypeThe...@googlegroups.com>.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
> --
> http://www.cs.bham.ac.uk/~mhe
>

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