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