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