On Friday, 24 November 2017 12:21:58 UTC, Martín Hötzel Escardó wrote:
>
> On 20/11/17 03:54, y wrote:
> > Can you elaborate on why it is true? 
>

Actually, my argument was fundamentally flawed, because this is not 
provable.

If univalence holds, then Id : X -> (X -> U) is an embedding.

But If the K axiom holds, then again Id : X -> (X -> U) is an embedding.

And hence there is no hope to deduce univalence from the fact that Id_X is 
an embedding for every X:U.

(And, as a side remark, I can't see how to prove that Id_X is an embedding 
without using K or univalence.)

Martin




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