Of course the last line is Id x ≡ A (without the y). Copy-and-paste-and-don't-modify properly phenomenon. 

On Friday, 24 November 2017 23:12:03 UTC, Martín Hötzel Escardó wrote:

 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)


Lat line should have been 

         ≃ Id x ≡ A
 
Martin