Can you elaborate on why it is true? Also as this statement is similar to Yoneda's lemma, do we have something like

For a type X : U and B : X -> U, Id (X -> U) (Id X x) B is equivalent to B x?

On Fri, Nov 17, 2017 at 3:53 PM, Martín Hötzel Escardó <escardo...@gmail.com> wrote:

Consider the identity type former Id of the type X:U in the universe U:

Id : X -> (X -> U).

I've known for some years that this is an embedding of the type X into the type (X->U). This means that the fibers of Id are propositions, or, equivalently, that the maps ap Id : x = y -> Id x = Id y are equivalences for all x,y:X.

This depends on univalence. I've just realized that this is actually *equivalent* to univalence. Has anybody noticed this before?

Martin

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