{A B} (e : A <~> B) {f : A -> B} {g : B -> A} (h : f == e) (k : g == e^-1) : A <~> B. Proof. snrapply equiv_adjointify. - exact f. - exact g. - intro a. exact (ap f (k a) @ h _ @ eisretr e a). - intro b. exact (ap g (h b) @ k _ @ eissect e b). Defined.
Require Import