Definition inverseEquivalence {X Y} : Equivalence X Y -> Equivalence Y X. Proof. intros [f [g [p [q h]]]]. simple refine (makeEquivalence Y X g f q p _). intro y. apply other_adjoint. assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.