Theorem weqinvweq (X Y : UU) : (X ≃ Y) ≃ (Y ≃ X). Proof. intros. apply (weq_iso invweq invweq). - intro. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. apply homotrefl. - intro. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. apply homotrefl. Defined.