Definition weqtotal2dirprodcomm {X Y : UU} (P : X × Y -> UU) : (∑ xy : X × Y, P xy) ≃ (∑ xy : Y × X, P (weqdirprodcomm _ _ xy)). Proof. intros. use weq_iso. - intros xyp. exact ((pr2 (pr1 xyp),, pr1 (pr1 xyp)),,pr2 xyp). - intros yxp. exact (((pr2 (pr1 yxp)),, (pr1 (pr1 yxp))),, pr2 yxp). - intros xyp. apply idpath. - intros yxp. apply idpath. Defined.