polynomial functor (Rev #2)

Let WfXgYhZW\stackrel{f}{\leftarrow}X\stackrel{g}{\to}Y\stackrel{h}{\to}Z be a diagram in a category CC; a diagram of this type is called a container or a indexed container. Let f *f^*, Π g\Pi_g, Σ\Sigma denote base change resp. dependent product resp. dependent sum. Then the composite

C/Wf *C/XΠ gC/YΣ hC/ZC/W\stackrel{f^*}{\to}C/X\stackrel{\Pi_g}{\to}C/Y\stackrel{\Sigma_h}{\to}C/Z

which we denote by PP, is called a polynomial functor. If gg is the identity we call PP a linear polynomial functor. This construction exists e.g. if CC is locally cartesian closed.

If we consider CC as a semantics for a type theory we can ask how P=Σ hΠ gf *P=\Sigma_h \Pi_g f^* interacts with display maps: recall that by definition the class of display maps is closed under composition, pullbacks along arbitrary morphisms, and forming exponential objects. Since Σ h=()f\Sigma_h=(-)\circ f, this preserves display maps if hh is a display maps and these are closed under composition. f *f^* forms pullbacks along ff, and Π\Pi forms exponential objects. In particular for PP to preserve display maps it is sufficient that gg and hh are display maps.

A polynomial functor Σ hΠ gf *\Sigma_h\Pi_g f^* where gg (but not necessarily hh) is a display map, restricted to display maps, one could call a dependent polynomial functor or better an inductive polynomial functor.

Initial algebras for polynomial functors, inductive families: A (weakly) initial algebra for an inductive polynomial functor we call an inductive family. An inductive family exists for all inductive polynomial functors.


(1) If h=Δ:ZZ×Zh=\Delta:Z\to Z\times Z is a display map, then Id Z(z,z)={refl}Id_Z(z,z)=\{refl\}

(2a) If X=X=\emptyset (the corresponding polynomial functor PP is then constant) and hh is a display map, then the initial algebra of the polynomial functor is hh. In particular the functor for identity types is of this form.

(2b) If in the same situation as in (2a) hh is not a display map, then the initial algebra of PP is a map h^:A^Z\hat h:\hat A\to Z equipped with a map hˇ:hh^\check{h}:h\to \hat h over ZZ with the property that every other map hqh\to q over ZZ with qq a display map, factors through h^\hat h.

The Coq defining an inductive family is

Inductive hfiber {A X} (I: A ->X) : (X->Type):=
inj : forall (x:A), hfiber I(Ix).

Revision on February 28, 2013 at 06:13:25 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.