proposition: 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: 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.
imports: UniMath.Foundations.PartA