Polynomial functor (type theory)

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.

Definition

Let Template:Var be a universe of types, let Template:Var : Template:Var, and let Template:Var : Template:Var → Template:Var be a family of types indexed by Template:Var. The pair (Template:Var, Template:Var) is sometimes called a signatureTemplate:Sfn or a container.Template:Sfn The polynomial functor associated to the container (Template:Var, Template:Var) is defined as follows:Template:SfnTemplate:SfnTemplate:Sfn

$\begin{array}{cc}P:U& ⟶U\\ X& ⟼\sum _{a:A}(B(a)\to X)\end{array}$

Any functor naturally isomorphic to Template:Var is called a container functor.Template:Sfn The action of Template:Var on functions is defined by

$\begin{array}{cc}P:(X\to Y)& ⟶(PX\to PY)\\ f& ⟼((a,g)\mapsto (a,g\circ f))\end{array}$

Note that this assignment is only truly functorial in extensional type theories (see #Properties).

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:

$\begin{array}{cc}P(f\circ g)& =Pf\circ Pg\\ P({𝗂𝖽}_X)& ={𝗂𝖽}_{PX}\end{array}$

for any functions Template:Var and Template:Var and any type Template:Var, where ${𝗂𝖽}_X$ is the identity function on the type Template:Var.Template:Sfn

References

• Template:Cite journal
• Template:Cite book
• Template:Cite book
• Template:Cite arXiv
• Template:Cite arXiv

External links

• An extensive collection of Notes on Polynomial Functors