Definition weqdirprodcomm (X Y : UU) : X × Y ≃ Y × X. Proof. intros. set (f := λ xy : X × Y, make_dirprod (pr2 xy) (pr1 xy)). set (g := λ yx : Y × X, make_dirprod (pr2 yx) (pr1 yx)). assert (egf : ∏ xy : _, (g (f xy)) = xy). intro. induction xy. apply idpath. assert (efg : ∏ yx : _, (f (g yx)) = yx). intro. induction yx. apply idpath. split with f. apply (isweq_iso _ _ egf efg). Defined.