Theorem weqsubsetsplit {X : UU} (f : X -> bool) : weq X ((hfiber f true) ⨿ (hfiber f false)). Proof. intros. set (ff := subsetsplit f). set (gg := subsetsplitinv f). split with ff. assert (egf : ∏ a : _, paths (gg (ff a)) a). { intros. unfold ff. unfold subsetsplit. induction (boolchoice (f a)) as [ et | ef ]. simpl. apply idpath. simpl. apply idpath. } assert (efg : ∏ a : _, paths (ff (gg a)) a). { intros. induction a as [ et | ef ]. - induction et as [ x et' ]. simpl. unfold ff. unfold subsetsplit. induction (boolchoice (f x)) as [ e1 | e2 ]. + apply (maponpaths (@ii1 _ _ )). apply (maponpaths (make_hfiber f x)). apply uip. apply isasetbool. + induction (nopathstruetofalse (pathscomp0 (pathsinv0 et') e2)). - induction ef as [ x et' ]. simpl. unfold ff. unfold subsetsplit. induction (boolchoice (f x)) as [ e1 | e2 ]. + induction (nopathsfalsetotrue (pathscomp0 (pathsinv0 et') e1)). + apply (maponpaths (@ii2 _ _ )). apply (maponpaths (make_hfiber f x)). apply uip. apply isasetbool. } apply (isweq_iso _ _ egf efg). Defined.