Lemma issurjective_coprod_carrier_binary_union {X} (A B : hsubtype X) : issurjective (coprod_carrier_binary_union A B). Proof. intros [x aub]. use(hinhfun _ aub). apply sumofmaps ; (intro y; use make_hfiber) ; try (apply subtypePath_prop). - exact(inl (x ,, y)). - apply idpath. - exact(inr (x ,, y)). - apply idpath. Qed.