Definition maponcomplincl {X Y : UU} (f : X -> Y) (is : isincl f) (x : X) : compl X x -> compl Y (f x) := λ x0' : _, match x0' with tpair _ x' neqx => tpair _ (f x') (negf (invmaponpathsincl _ is x x') neqx) end.