In type theory, a polynomial functor (or container functor) is a kind of endofunctor of a category of types that is intimately related to the concept of inductive and coinductive types.
M-types) are (isomorphic to) initial algebras (resp.
Polynomial functors have been studied in the more general setting of a pretopos with Σ-types;[1] this article deals only with the applications of this concept inside the category of types of a Martin-Löf style type theory.
The pair (A, B) is sometimes called a signature[2] or a container.
[7] The action of P on functions is defined by Note that this assignment is only truly functorial in extensional type theories (see #Properties).