Definition Equivalence_toInverseFunction {X Y} : X≅Y -> Y->X. Proof. intros f. exact (pr1 (pr2 f)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.