Spahn
polynomial functor (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Definition

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

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

which If we denote consider by P C P C , is as called a semantics for a type theory we can ask howpolynomial functorP=Σ hΠ gf *P=\Sigma_h \Pi_g f^* . If 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. SincegΣ h=()f g \Sigma_h=(-)\circ f , is this the preserves identity display we maps call if P h P h is a display maps and these are closed under composition.linear polynomial functorf *f^* . This forms construction pullbacks exists along e.g. if C f C f , is and locally cartesian closed.Π\Pi forms exponential objects. In particular for PP to preserve display maps it is sufficient that gg and hh are display maps.

Polynomial functors and 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.

If Initial algebras for polynomial functors, inductive families: A (weakly) initial algebra for an inductive polynomial functor we consider call anCCinductive family . as An a inductive semantics family exists for a all type inductive theory polynomial we functors. can ask howP=Σ 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 Examples: 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

(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\}

A (2a) (weakly) If initial algebra for an inductive polynomial functor we call aninductive familyX=X=\emptyset . An (the inductive corresponding family exists for all inductive polynomial functors. functorPP 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.