Definition invrecompl_ne (X : UU) (x : X) (neq_x : neqPred x) (is : isisolated X x) : X -> compl_ne X x neq_x ⨿ unit. Proof. intros y. induction (is y) as [k|k]. - exact (ii2 tt). - exact (ii1 (make_compl_ne X x neq_x y (neg_to_negProp k))). Defined.