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. Specifically, all W-types (resp. M-types) are (isomorphic to) initial algebras (resp. final coalgebras) of such functors.
Polynomial functors have been studied in the more general setting of a pretopos with ã-types; this article deals only with the applications of this concept inside the category of types of a Martin-Löf style type theory.
Let be a universe of types, let : , and let : â be a family of types indexed by . The pair (, ) is sometimes called a signature or a container. The polynomial functor associated to the container (, ) is defined as follows:
Any functor naturally isomorphic to is called a container functor. The action of on functions is defined by
Note that this assignment is only truly functorial in extensional type theories (see #Properties).
In intensional type theories, such functions are not truly functors, because the universe type is not strictly a category (the field of homotopy type theory is dedicated to exploring how the universe type behaves more like a higher category). However, it is functorial up to propositional equalities, that is, the following identity types are inhabited:
for any functions and and any type , where is the identity function on the type .