Theorem isweqdirprodf {X Y X' Y' : UU} (w : X ≃ Y) (w' : X' ≃ Y') : isweq (dirprodf w w'). Proof. intros. set (f := dirprodf w w'). set (g := dirprodf (invweq w) (invweq w')). assert (egf : ∏ a : _, (g (f a)) = a). intro a. induction a as [ x x' ]. simpl. apply pathsdirprod. apply (homotinvweqweq w x). apply (homotinvweqweq w' x'). assert (efg : ∏ a : _, (f (g a)) = a). intro a. induction a as [ x x' ]. simpl. apply pathsdirprod. apply (homotweqinvweq w x). apply (homotweqinvweq w' x'). apply (isweq_iso _ _ egf efg). Defined.