Theorem weqfweq (X : UU) {Y Z : UU} (w : Y ≃ Z) : (X ≃ Y) ≃ (X ≃ Z). Proof. intros. set (f := λ a : X ≃ Y, weqcomp a w). set (g := λ b : X ≃ Z, weqcomp b (invweq w)). split with f. assert (egf : ∏ a, g (f a) = a). { intro a. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. intro x. apply (homotinvweqweq w (a x)). } assert (efg : ∏ b, f (g b) = b). { intro b. apply (invmaponpathsincl _ (isinclpr1weq _ _)). apply funextfun. intro x. apply (homotweqinvweq w (b x)). } apply (isweq_iso _ _ egf efg). Defined.