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>:

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