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;[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
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 signature[2] or a container.[3] The polynomial functor associated to the container (A, B) is defined as follows:[4][5][6]
- [math]\displaystyle{ \begin{align} P : U &\longrightarrow U \\ X &\longmapsto \sum_{a:A} (B(a) \to X) \end{align} }[/math]
Any functor naturally isomorphic to P is called a container functor.[7] The action of P on functions is defined by
- [math]\displaystyle{ \begin{align} P^* : (X\to Y) &\longrightarrow (P^*X\to P^*Y) \\ (f, (a,g)) &\longmapsto (a,g\circ f) \end{align} }[/math]
Note that this assignment is not 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:
- [math]\displaystyle{ \begin{align} P^*(f\circ g) &= P^*f\circ P^*g \\ P^*(\mathsf{id}_X) &= \mathsf{id}_{PX} \end{align} }[/math]
for any functions f and g and any type X, where [math]\displaystyle{ \mathsf{id}_X }[/math] is the identity function on the type X.[8]
Inline citations
- ↑ 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.
- ↑ Ahrens, Capriotti & Spadotti 2015, Definition 1.
- ↑ Abbott, Altenkirch & Ghani 2005, p. 4.
- ↑ Univalent Foundations Program 2013, Equation 5.4.6.
- ↑ Ahrens, Capriotti & Spadotti 2015, Definition 2.
- ↑ Awodey, Gambino & Sojakova 2012, p. 8.
- ↑ Abbott, Altenkirch & Ghani 2005, p. 10.
- ↑ Awodey, Gambino & Sojakova 2015.
References
- Abbott, Michael; Altenkirch, Thorsten; Ghani, Neil (2005). "Containers: Constructing strictly positive types". Theoretical Computer Science 342 (1): 4. doi:10.1016/j.tcs.2005.06.002.
- Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). Non-wellfounded trees in Homotopy Type Theory. Leibniz International Proceedings in Informatics (LIPIcs). 38. pp. 17–30. doi:10.4230/LIPIcs.TLCA.2015.17. ISBN 9783939897873.
- Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. pp. 159. http://homotopytypetheory.org/book/.
- Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2012-01-18). "Inductive types in homotopy type theory". arXiv:1201.3898 [math.LO].
- Awodey, Steve; Gambino, Nicola; Sojakova, Kristina (2015-04-21). "Homotopy-initial algebras in type theory". arXiv:1504.05531 [math.LO].
External links
- An extensive collection of Notes on Polynomial Functors
 |  |
