Polynomial functor (type theory)

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]

$${\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

$${\displaystyle {\begin{aligned}P^{*}:(X\to Y)&\longrightarrow (P^{*}X\to P^{*}Y)\\(f,(a,g))&\longmapsto (a,g\circ f)\end{aligned}}.}$$

Note that this assignment is not only truly functorial in extensional type theories (see #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:

$${\displaystyle {\begin{aligned}P^{*}(f\circ g)&=P^{*}f\circ P^{*}g\\P^{*}({\mathsf {id}}_{X})&={\mathsf {id}}_{PX}\end{aligned}}.}$$

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

• Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. p. 159.
• 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].
• Ahrens, Benedikt; Capriotti, Paolo; Spadotti, Régis (2015-04-12). "Non-wellfounded trees in Homotopy Type Theory". arXiv:1504.02949. doi:10.4230/LIPIcs.TLCA.2015.17. Cite journal requires |journal= (help)
• 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.

• An extensive collection of Notes on Polynomial Functors