{X : Type u_2} →
  [inst : SemilatticeInf X] →
    (toFun : X → X) →
      (∀ (a b : X), toFun (a ⊓ b) = toFun a ⊓ toFun b) →
        (∀ (x : X), toFun (toFun x) ≤ toFun x) → (∀ (x : X), x ≤ toFun x) → Nucleus X