{A B : Type} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : f == g) : IsEquiv g. Proof. snrapply isequiv_adjointify. - exact f^-1. - intro b. exact ((h _)^ @ eisretr f b). - intro a. exact (ap f^-1 (h a)^ @ eissect f a). Defined.
Require Import