Lemma sec_total2_distributivity {A : UU} {B : A -> UU} (C : ∏ a, B a -> UU) : (∏ a : A, ∑ b : B a, C a b) ≃ (∑ b : ∏ a : A, B a, ∏ a, C a (b a)). Proof. use weq_iso. - intro f. use tpair. + exact (fun a => pr1 (f a)). + exact (fun a => pr2 (f a)). - intro f. intro a. exists ((pr1 f) a). apply (pr2 f). - apply idpath. - apply idpath. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.PartB.