Polynomial functor (type theory)


In type theory, a polynomial 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 are initial algebras 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.

Definition

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 not only truly functorial in extensional type theories.

Properties

In intensional type theories, such functions are not truly functors, because the universe type is not strictly a 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.

Inline citations