Definition weqsecovertotal2 {X : UU} (P : X -> UU) (Q : (∑ x, P x) -> UU) : (∏ xp : (∑ x, P x), Q xp) ≃ (∏ x, ∏ p : P x, Q (x,, p)). Proof. intros. set (f := λ a : ∏ xp : (∑ x, P x), Q xp, λ x, λ p : P x, a (x,, p)). set (g := tosecovertotal2 P Q). split with f. assert (egf : ∏ a, g (f a) = a). { intro. apply funextsec. intro xp. induction xp as [ x p ]. apply idpath. } assert (efg : ∏ a, f (g a) = a). { intro. apply funextsec. intro x. apply funextsec. intro p. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.