There is such a thing as coiteration in the category theory sense. It's related to the data/codata and recursion/corecursion distinction. To take a couple examp

There is such a thing as coiteration in the category theory sense. It's related to the data/codata and recursion/corecursion distinction. To take a couple examples from the `free` package [1] for Haskell: iter :: Functor f => (f a -> a) -> Free f a -> a coiter :: Functor f => (a -> f a) -> a -> Cofree f a Like (formal) recursion, `iter` depends on having a base case to work upward from. Like corecursion, `coiter` generates steps from the top down (towards a base that may never come). As is often the case, terminology is overloaded and multiple overloads are attested in the real world. [1] https://hackage.haskell.org/package/free-5.2/docs/Control-Monad-Free.html#v:iter https://hackage.haskell.org/package/free-5.2/docs/Control-Mo... https://hackage.haskell.org/package/free-5.2/docs/Control-Comonad-Cofree.html#v:coiter https://hackage.haskell.org/package/free-5.2/docs/Control-Co...