You asked a question privately, but I choose to answer it here.

On Monday, 20 November 2017 03:54:55 UTC, Yuhao Huang wrote:
>
> 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 A : X -> U, Id (X -> U) (Id X x) A is equivalent to A 
> x?
>
>
We have

 A x ≃ Nat (Id x) A           (yoneda)
     = Π(y:Y), Id x y → A y  (definition)
     ≃ Π(y:Y), Id x y ≃ A y (because Σ A is contractible (Yoneda corollary))
     ≃ Π(y:Y), Id x y ≡ A y (by univalence)
     ≃ Id x ≡ A y           (by extensionality)

Martin