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