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