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.

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