## 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 $$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. ## Polynomial functors and display maps If we consider $C$ as a semantics for a type theory we 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 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 A (weakly) initial algebra for an inductive polynomial functor we call an *inductive family*. An inductive family exists for all inductive polynomial functors.