On 20/11/17 03:54, y wrote:
> Can you elaborate on why it is true? 

I am writing this in Agda to be absolutely sure of all the
details. But this is going slowly because lack of time. When It is
done I will give you a link and also a proof in English prose.

> Also as this statement is similar
> to Yoneda's lemma, do we have something like

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

As I said privately to you, yes. This follows from one of the Yoneda
Lemmas, namely that if Sigma B is contractible then the recursively
defined map

  Pi(y : Y), Id x y -> B y is an equivalence

for every x : X and b : B x (and conversely).

The Id-fiber of B is Sigma(x : X), Id x = B.

If (x:X, p : Id x = B) is in the fiber, then

   ap Sigma p : Sigma(Id x) = Sigma B,

and hence, being equal to a contractible type, Sigma B is
contractible.

This doesn't use univalence or function extensionality.

Next you have to use the contractibility of Sigma B to show that the
Id-fiber of B is contractible. It is this step which uses the (above
form of the) Yoneda Lemma and univalence, so show that this fiber is
equivalence to Sigma B (being a retract suffices, but we do in fact
get an equivalence automatically: it is laborious to check the
retraction condition; the section condition, which is not nedeed, is
much easier).

With this you get that Id is an embedding.

That from this (for all types) you get univalence is subtler, and I
want to check everything before I sketch an argument in public. But I
didn't want to do this if somebody told me, in response to the message
below, that this has been already done, but nobody did.

Martin