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;{{Cite journal|last1=Moerdijk|first1=Ieke|last2=Palmgren|first2=Erik|title=Wellfounded trees in categories|journal=Annals of Pure and Applied Logic|volume=104|issue=1–3|pages=189–218|doi=10.1016/s0168-0072(00)00012-9|year=2000|hdl=2066/129036|hdl-access=free}} 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 {{var|U}} be a universe of types, let {{var|A}} : {{var|U}}, and let {{var|B}} : {{var|A}} → {{var|U}} be a family of types indexed by {{var|A}}. The pair ({{var|A}}, {{var|B}}) is sometimes called a signature{{sfn|Ahrens|Capriotti|Spadotti|2015|loc=Definition 1}} or a container.{{sfn|Abbott|Altenkirch|Ghani|2005|p=4}} The polynomial functor associated to the container ({{var|A}}, {{var|B}}) is defined as follows:{{sfn|Univalent Foundations Program|2013|loc=Equation 5.4.6}}{{sfn|Ahrens|Capriotti|Spadotti|2015|loc=Definition 2}}{{sfn|Awodey|Gambino|Sojakova|2012|p=8}}

: $\begin{align}
P : U &\longrightarrow U \\
X &\longmapsto \sum_{a:A} (B(a) \to X)
\end{align}$

Any functor naturally isomorphic to {{var|P}} is called a container functor.{{sfn|Abbott|Altenkirch|Ghani|2005|p=10}} The action of {{var|P}} on functions is defined by

: $\begin{align}
P : (X\to Y) &\longrightarrow (PX\to PY) \\
f \qquad &\longmapsto \left((a,g) \mapsto (a,g\circ f)\right)
\end{align}$

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{align}
P(f\circ g) &= Pf\circ Pg \\
P(\mathsf{id}_X) &= \mathsf{id}_{PX}
\end{align}$

for any functions {{var|f}} and {{var|g}} and any type {{var|X}}, where $\mathsf{id}_X$ is the identity function on the type {{var|X}}.{{sfn|Awodey|Gambino|Sojakova|2015}}

Inline citations

References

{{Cite journal|last1=Abbott|first1=Michael|last2=Altenkirch|first2=Thorsten|last3=Ghani|first3=Neil|title=Containers: Constructing strictly positive types|journal=Theoretical Computer Science|volume=342|issue=1|page=4|doi=10.1016/j.tcs.2005.06.002|year=2005|doi-access=free|citeseerx=10.1.1.166.34}}
{{cite book|last1=Ahrens|first1=Benedikt|last2=Capriotti|first2=Paolo|last3=Spadotti|first3=Régis|date=2015-04-12|title=Non-wellfounded trees in Homotopy Type Theory|series=Leibniz International Proceedings in Informatics (LIPIcs)|volume=38|pages=17–30|arxiv=1504.02949 |doi=10.4230/LIPIcs.TLCA.2015.17|doi-access=free |isbn=9783939897873|s2cid=15020752}}
{{Cite book|author=Univalent Foundations Program|title=Homotopy Type Theory: Univalent Foundations of Mathematics|year=2013|publisher=Institute for Advanced Study|url=http://homotopytypetheory.org/book/|pages=159}}
{{cite arXiv|last1=Awodey|first1=Steve|last2=Gambino|first2=Nicola|last3=Sojakova|first3=Kristina|date=2012-01-18|title=Inductive types in homotopy type theory|eprint=1201.3898 |class=math.LO}}
{{cite arXiv|last1=Awodey|first1=Steve|last2=Gambino|first2=Nicola|last3=Sojakova|first3=Kristina|date=2015-04-21|title=Homotopy-initial algebras in type theory|eprint=1504.05531 |class=math.LO}}

External links

An extensive collection of [http://mat.uab.cat/~kock/cat/polynomial.pdf Notes on Polynomial Functors]

Category:Type theory