proposition: Theorem weqinvweq (X Y : UU) : (X ≃ Y) ≃ (Y ≃ X).
proof: Proof. intros. apply (weq_iso invweq invweq). - intro. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. apply homotrefl. - intro. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. apply homotrefl. Defined.
imports: UniMath.Foundations.PartC