My recollection from real analysis was that I liked sequential continuity a lot (https://en.wikipedia.org/wiki/Continuous_function#Sequences_and_nets https://en

My recollection from real analysis was that I liked sequential continuity a lot (https://en.wikipedia.org/wiki/Continuous_function#Sequences_and_nets https://en.wikipedia.org/wiki/Continuous_function#Sequences_...). Sequences form a nice beginner-friendly monad (`bind` is the diagonal nth from nth), and lifting a real function over a real sequence is just `fmap`! (This is the same notion of sequence that https://clash-lang.org/ https://clash-lang.org/ uses for sequential circuits, but it skips the monad because circuits are first order.) Convergent sequences are like ordered binary tree sets, they do also form a monad, but one in a sub-category: sequentially continuous functions are precisely those that are in the domain of the underlying functor! :)