Spahn polynomial functor (Rev #2, changes)

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

Definition

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

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

$C/W\stackrel{f^*}{\to}C/X\stackrel{\Pi_g}{\to}C/Y\stackrel{\Sigma_h}{\to}C/Z$
$C/W\stackrel{f^*}{\to}C/X\stackrel{\Pi_g}{\to}C/Y\stackrel{\Sigma_h}{\to}C/Z$

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

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

Polynomial functors and display maps

A polynomial functor $\Sigma_h\Pi_g f^*$ where $g$ (but not necessarily $h$) 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 an$C$inductive family . as An a inductive semantics family exists for a all type inductive theory polynomial we functors. can ask how$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 $\Sigma_h=(-)\circ f$, this preserves display maps if $h$ is a display maps and these are closed under composition. $f^*$ forms pullbacks along $f$, and $\Pi$ forms exponential objects. In particular for $P$ to preserve display maps it is sufficient that $g$ and $h$ are display maps.

A Examples: polynomial functor$\Sigma_h\Pi_g f^*$ where $g$ (but not necessarily $h$) 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=\Delta:Z\to Z\times Z$ is a display map, then $Id_Z(z,z)=\{refl\}$

A (2a) (weakly) If initial algebra for an inductive polynomial functor we call aninductive family$X=\emptyset$ . An (the inductive corresponding family exists for all inductive polynomial functors. functor$P$ is then constant) and $h$ is a display map, then the initial algebra of the polynomial functor is $h$. In particular the functor for identity types is of this form.

(2b) If in the same situation as in (2a) $h$ is not a display map, then the initial algebra of $P$ is a map $\hat h:\hat A\to Z$ equipped with a map $\check{h}:h\to \hat h$ over $Z$ with the property that every other map $h\to q$ over $Z$ with $q$ a display map, factors through $\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.