Definition locsplitsec (X : UU) (Y : UU) (f : X -> Y) (ls : locsplit f) : dnegimage f -> X := λ u, match u with tpair y psi => match (ls y) with ii1 z => pr1 z| ii2 phi => fromempty (psi phi) end end.