Definition weqcoprodsplit {X Y Z : UU} (f : X -> coprod Y Z) : X ≃ (∑ y : Y, hfiber f (ii1 y)) ⨿ (∑ z : Z, hfiber f (ii2 z)). Proof. intros. set (w1 := weqtococonusf f). set (w2 := weqtotal2overcoprod (λ yz : coprod Y Z, hfiber f yz)). apply (weqcomp w1 w2). Defined.