Definition locsplitsecissec (X Y : UU) (f : X -> Y) (ls : locsplit f) (u:dnegimage f) : paths (xtodnegimage f (locsplitsec f ls u)) u. Proof. intros. set (p := xtodnegimage f). set (s := locsplitsec f ls). assert (paths (pr1 (p (s u))) (pr1 u)). unfold p. unfold xtodnegimage. unfold s. unfold locsplitsec. simpl. induction u. set (lst := ls t). induction lst. simpl. apply (pr2 x0). induction (x y). assert (is : isofhlevelf (S O) (dnegimageincl f)). apply (isofhlevelfpr1 (S O) (λ y : Y, isapropdneg (hfiber f y))). assert (isw: isweq (maponpaths (dnegimageincl f) (p (s u)) u)). apply (isofhlevelfonpaths O _ is). apply (invmap _ isw X0). Defined.