ENat natCast as functor

Stream: mathlib4

[Robert Maxton]

Where's the best place for this def to live:

@[simps!]
def ENat.ofNatFunctor : ℕ ⥤ ℕ∞ :=
  Monotone.functor fun {_ _} ↦ WithTop.coe_le_coe.mpr

Alternatively, is there any sort of 'monotoneNatCast' typeclass I don't know about that would allow this to be generalized so that it has an obvious place to live?

[Robert Maxton]

The current bid is "awkwardly inserted at the top of Mathlib.Topology.CWComplex.ClassicalToAbstract" (which doesn't exist yet), which shouldn't be hard to beat!

[Robert Maxton]

Hmmm... I could generalize it to WithTop, and then argue it fits in Mathlib.CategoryTheory.Category.Preorder, perhaps?