fact: Definition iscontrweqb_compute {X Y} (w:X ≃ Y) (is:iscontr Y) : iscontrpr1 (iscontrweqb w is) = invmap w (iscontrpr1 is).
imports: UniMath.Foundations.All UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Equivalences