Definition iscontrweqb_compute {X Y} (w:X ≃ Y) (is:iscontr Y) : iscontrpr1 (iscontrweqb w is) = invmap w (iscontrpr1 is). Proof. intros. unfold iscontrweqb. rewrite iscontrretract_compute. reflexivity. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Equivalences.