Spahn polynomial monad

A polynomial monad is a monad whose underlying endofunctor is a polynomial functor polynomial functor. This is of course equivalent to being a monad in the category of polynomial functors.

Examples

A basic example is the free-monoid monad, Example 1.9. It is exhibited by the polynomial 1 11\leftarrow \mathbb{N}^\prime\rightarrow \mathbb{N}\rightarrow 1 where the middle arrow is such that for all nn\in \mathbb{N} its fiber over nn has cardinality nn.

One can construct the free monad on a polynomial endofunctor.

An extensive category EE (which in particular has finite sums) has W-types iff every polynomial functor in a single variable on EE has an initial algebra. The “W” in the name of this notion refers to the fact Martin-Löf’s types of wellfounded trees (translated into category theory) are initial algebras for polynomial endofunctors in a single variable. Initial algebras for (general) polynomial functors correspond to Petersson-Synek tree types.

Reference