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