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