Jump to content

Polynomial functor (type theory)

From Wikipedia, the free encyclopedia

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;[1] this article deals only with the applications of this concept inside the category of types of a Martin-Löf style type theory.

Definition

[edit]

Let U be a universe of types, let A : U, and let B : AU be a family of types indexed by A. The pair (A, B) is sometimes called a signature[2] or a container.[3] The polynomial functor associated to the container (A, B) is defined as follows:[4][5][6]

Any functor naturally isomorphic to P is called a container functor.[7] The action of P on functions is defined by

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

Properties

[edit]

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 f and g and any type X, where is the identity function on the type X.[8]

Inline citations

[edit]
  1. ^ Moerdijk, Ieke; Palmgren, Erik (2000). "Wellfounded trees in categories". Annals of Pure and Applied Logic. 104 (1–3): 189–218. doi:10.1016/s0168-0072(00)00012-9. hdl:2066/129036.
  2. ^ Ahrens, Capriotti & Spadotti 2015, Definition 1.
  3. ^ Abbott, Altenkirch & Ghani 2005, p. 4.
  4. ^ Univalent Foundations Program 2013, Equation 5.4.6.
  5. ^ Ahrens, Capriotti & Spadotti 2015, Definition 2.
  6. ^ Awodey, Gambino & Sojakova 2012, p. 8.
  7. ^ Abbott, Altenkirch & Ghani 2005, p. 10.
  8. ^ Awodey, Gambino & Sojakova 2015.

References

[edit]


[edit]