On Wednesday, 29 November 2017 21:13:27 UTC, E 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 a natural equivalence as the 
univalence axiom demands) then Id_X : X -> (X -> U) is an embedding for 
all X:U.

It is natural to ask whether the converse holds (particularly given my original wrong claim recorded in the subject of this thread). Do you think it does?

Martin

 

> Evan
>
> 2017-11-28 4:40 GMT-05:00 Andrej Bauer <andr...@andrej.com <javascript:>
> >:
>
>> > 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 <javascript:>.
>> For more options, visit https://groups.google.com/d/optout.
>>
>
>