fact: Definition iscontrretract_compute {X Y} (p:X->Y) (s:Y->X) (eps:∏ y : Y, p (s y) = y) (is:iscontr X) : iscontrpr1 (iscontrretract p s eps is) = p (iscontrpr1 is).
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Equivalences