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