Menu
Home Explore People Places Arts History Plants & Animals Science Life & Culture Technology
On this page
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.

We don't have any images related to Polynomial functor (type theory) yet.
We don't have any YouTube videos related to Polynomial functor (type theory) yet.
We don't have any PDF documents related to Polynomial functor (type theory) yet.
We don't have any Books related to Polynomial functor (type theory) yet.
We don't have any archived web articles related to Polynomial functor (type theory) yet.

Definition

Let U be a universe of types, let A : U, and let B : A → U be a family of types indexed by A. The pair (A, B) is sometimes called a signature2 or a container.3 The polynomial functor associated to the container (A, B) is defined as follows:456

P : U ⟶ U X ⟼ ∑ a : A ( B ( a ) → X ) {\displaystyle {\begin{aligned}P:U&\longrightarrow U\\X&\longmapsto \sum _{a:A}(B(a)\to X)\end{aligned}}}

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

P : ( X → Y ) ⟶ ( P X → P Y ) f ⟼ ( ( a , g ) ↦ ( a , g ∘ f ) ) {\displaystyle {\begin{aligned}P:(X\to Y)&\longrightarrow (PX\to PY)\\f\qquad &\longmapsto \left((a,g)\mapsto (a,g\circ f)\right)\end{aligned}}}

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:

P ( f ∘ g ) = P f ∘ P g P ( i d X ) = i d P X {\displaystyle {\begin{aligned}P(f\circ g)&=Pf\circ Pg\\P({\mathsf {id}}_{X})&={\mathsf {id}}_{PX}\end{aligned}}}

for any functions f and g and any type X, where i d X {\displaystyle {\mathsf {id}}_{X}} is the identity function on the type X.8

Inline citations

References

  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. /wiki/Doi_(identifier) ↩

  2. Ahrens, Capriotti & Spadotti 2015, Definition 1. - Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). Non-wellfounded trees in Homotopy Type Theory. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 38. pp. 17–30. arXiv:1504.02949. doi:10.4230/LIPIcs.TLCA.2015.17. ISBN 9783939897873. S2CID 15020752. https://arxiv.org/abs/1504.02949 ↩

  3. Abbott, Altenkirch & Ghani 2005, p. 4. - Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 4. CiteSeerX 10.1.1.166.34. doi:10.1016/j.tcs.2005.06.002. https://doi.org/10.1016%2Fj.tcs.2005.06.002 ↩

  4. Univalent Foundations Program 2013, Equation 5.4.6. - Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. p. 159. http://homotopytypetheory.org/book/ ↩

  5. Ahrens, Capriotti & Spadotti 2015, Definition 2. - Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). Non-wellfounded trees in Homotopy Type Theory. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 38. pp. 17–30. arXiv:1504.02949. doi:10.4230/LIPIcs.TLCA.2015.17. ISBN 9783939897873. S2CID 15020752. https://arxiv.org/abs/1504.02949 ↩

  6. Awodey, Gambino & Sojakova 2012, p. 8. - Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2012-01-18). "Inductive types in homotopy type theory". arXiv:1201.3898 [math.LO]. https://arxiv.org/abs/1201.3898 ↩

  7. Abbott, Altenkirch & Ghani 2005, p. 10. - Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science. 342 (1): 4. CiteSeerX 10.1.1.166.34. doi:10.1016/j.tcs.2005.06.002. https://doi.org/10.1016%2Fj.tcs.2005.06.002 ↩

  8. Awodey, Gambino & Sojakova 2015. - Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2015-04-21). "Homotopy-initial algebras in type theory". arXiv:1504.05531 [math.LO]. https://arxiv.org/abs/1504.05531 ↩