Definition weqtotal2comm {A B : UU} {C : A → B → UU} : (∑ (a : A) (b : B), C a b) ≃ (∑ (b : B) (a : A), C a b). Proof. use weq_iso. - exact (λ pair, pr1 (pr2 pair),, pr1 pair,, pr2 (pr2 pair)). - exact (λ pair, pr1 (pr2 pair),, pr1 pair,, pr2 (pr2 pair)). - reflexivity. - reflexivity. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.