Definition weqtotal2overcoprod' {W X Y : UU} (P : W -> UU) (f : X ⨿ Y ≃ W) : (∑ w, P w) ≃ (∑ x : X, P (f (ii1 x))) ⨿ (∑ y : Y, P (f (ii2 y))). Proof. intros. exact (weqcomp (invweq (weqfp f _)) (weqtotal2overcoprod (P ∘ f))). Defined.