Definition weqtotal2comm12 {X} (P Q : X -> UU) : (∑ (w : ∑ x, P x), Q (pr1 w)) ≃ (∑ (w : ∑ x, Q x), P (pr1 w)). Proof. intros. use weq_iso. - intro xpq. exact ((pr1 (pr1 xpq),,pr2 xpq),, pr2 (pr1 xpq)). - intro xqp. exact ((pr1 (pr1 xqp),, pr2 xqp),, pr2 (pr1 xqp)). - intro. apply idpath. - intro. apply idpath. Defined.