> > 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ó : > > > 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>>: >> >> > 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 >> . >> 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 > HomotopyTypeThe...@googlegroups.com>. >> For more options, visit https://groups.google.com/d/optout. >> > > -- > http://www.cs.bham.ac.uk/~mhe >