fact: Definition isEquivalence_toSourceHomotopy {X Y} {f:X->Y} (i:isEquivalence f) : ∏ x, isEquivalence_toInverseFunction i (f x) = x := pr122 i.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics