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.

## Contents

* 1 Definition
* 2 Properties
* 3 Inline citations
* 4 References
* 5 External links

## 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]

P:U⟶UX⟼∑a:A(B(a)->X)

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)

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:

P*(f∘g)=P*f∘P*gP*(idX)=idPX

for any functions f and g and any type X, where idX is the identity function on the type X.[8]

## Inline citations

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.
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

* 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

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Polynomial functor (type theory). Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Polynomial_functor_(type_theory)&oldid=231902"