Theorem weqtotal2overcoprod {X Y : UU} (P : X ⨿ Y -> UU) : (∑ xy, P xy) ≃ (∑ x : X, P (ii1 x)) ⨿ (∑ y : Y, P (ii2 y)). Proof. intros. set (f := fromtotal2overcoprod P). set (g := tototal2overcoprod P). split with f. assert (egf : ∏ a : _ , (g (f a)) = a). { intro a. induction a as [ xy p ]. induction xy as [ x | y ]. simpl. apply idpath. simpl. apply idpath. } assert (efg : ∏ a : _ , (f (g a)) = a). { intro a. induction a as [ xp | yp ]. induction xp as [ x p ]. simpl. apply idpath. induction yp as [ y p ]. apply idpath. } apply (isweq_iso _ _ egf efg). Defined.