Definition isEquivalence_toInverseFunction {X Y} {f:X->Y} : isEquivalence f -> Y->X := pr1.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Notations. Require Import UniMath.MoreFoundations.Tactics.