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). Proof. intros. unfold iscontrretract. destruct is as [ctr uni]. simpl. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.