Definition fromtotal2overcoprod {X Y : UU} (P : X ⨿ Y -> UU) (xyp : total2 P) : coprod (∑ x : X, P (ii1 x)) (∑ y : Y, P (ii2 y)). Proof. intros. set (PX := λ x : X, P (ii1 x)). set (PY := λ y : Y, P (ii2 y)). induction xyp as [ xy p ]. induction xy as [ x | y ]. apply (ii1 (tpair PX x p)). apply (ii2 (tpair PY y p)). Defined.