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