Definition subsetsplit {X : UU} (f : X -> bool) (x : X) : (hfiber f true) ⨿ (hfiber f false). Proof. intros. induction (boolchoice (f x)) as [ a | b ]. - apply (ii1 (make_hfiber f x a)). - apply (ii2 (make_hfiber f x b)). Defined.