s: S.\,
P\, s \to X$, so that ${\llbracket C \rrbracket^\mathrm{c}}\, X$ consists of pairs of a shape and an assignment of an element of $X$ to each of the positions in this shape, reflecting the intuitive reading that shapes are “templates" for datatypes and positions identify “blanks" in these templates that can be filled in with data. The interpretation ${\llbracket C \rrbracket^\mathrm{c}} : \forall {\{X\}}, {\{Y\}}.\, (X \to Y) \to (\Sigma s: S.\,
P\, s \to X) \to \Sigma s: S.\, P\, s \to Y$ of $C$ on functions is defined by ${\llbracket C \rrbracket^\mathrm{c}}\, f\, (s, v) = (s, f {\circ}v)$. It is straightforward that ${\llbracket C \rrbracket^\mathrm{c}}$ preserves identity and composition of functions, so it is a set functor (as any datatype should be).

Our example containers denote the datatypes intended. If we let $C$ be the container of lists, we have ${\llbracket C \rrbracket^\mathrm{c}}\, X = \Sigma s : {\mathsf{Nat}}.\,
{\mathsf{Fin}}\, s \to X \cong {\mathsf{List}}\, X$. The container of streams interprets into $\Sigma {{\ast}}: 1.\, {\mathsf{Nat}}\to X \cong {\mathsf{Nat}}\to X \cong {\mathsf{Str}}\, X$. Etc.

A morphism $h = t \lhd q$ between containers $C = S \lhd P$ and $C =
S' \lhd P'$ is 