Lemma total2_assoc_fun_left {A B : UU} (C : A -> B -> UU) (D : (∏ a : A, ∑ b : B, C a b) -> UU) : (∑ (x : ∏ a : A, ∑ b : B, C a b), D x) ≃ ∑ (x : ∏ _ : A, B), ∑ (y : ∏ a : A, C a (x a)), D (fun a : A => (x a,, y a)). Proof. use weq_iso. - intros p. exists (fun a => (pr1 (pr1 p a))). exists (fun a => (pr2 (pr1 p a))). exact (pr2 p). - intros p. use tpair. + intros a. use tpair. * exact (pr1 p a). * exact (pr1 (pr2 p) a). + exact (pr2 (pr2 p)). - reflexivity. - reflexivity. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.