Spahn polynomial functor

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.

Examples:

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

It is just the homotopy fiber of II. In particular the identity type of XX is the homotopy fiber of the diagonal Δ:XX×X\Delta:X\to X\times X.

Last revised on February 28, 2013 at 07:36:58. See the history of this page for a list of all contributions to it.