Lemma iscontrweqb' {X Y} (is:iscontr Y) (w:X ≃ Y) : iscontr X. Proof. intros. apply (iscontrweqb (Y:=Y)). assumption. assumption. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.Foundations.Sets UniMath.Foundations.UnivalenceAxiom.