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