proposition: Lemma iscontr_weq (X Y : UU) : iscontr X → iscontr Y → iscontr (X ≃ Y).
proof: Proof. intros cX cY. exists (weqcontrcontr cX cY ). intro f. apply subtypePath. { exact isapropisweq. } apply funextfun. cbn. intro x. apply (pr2 cY). Defined.
imports: UniMath.Foundations.Propositions UniMath.Foundations.UnivalenceAxiom