S \to {\mathsf{Set}}$ of *positions*. Intuitively, shapes are “templates” for data-structures and positions identify “blanks” in these templates that can be filled with data.

The datatype of lists is represented by $S \lhd P$ where the shapes $S
= {\mathsf{Nat}}$ are the possible lengths of lists and the positions $P\, s =
{\mathsf{Fin}}\, s = \{0,\ldots,s-1\}$ provide $s$ places for data in lists of length $s$. Non-empty lists are obtained by letting $S = {\mathsf{Nat}}$ and $P\, s = {\mathsf{Fin}}\, (s+1)$ (so that shape $s$ has $s+1$ rather than $s$ positions).

Streams are characterized by a single shape with natural number positions: $S = 1 = \{{{\ast}}\}$ and $P\, {{\ast}}= {\mathsf{Nat}}$. The singleton datatype has one shape and one position: $S = 1$, $P\, {{\ast}}= 1$.

A *morphism* between containers $S \lhd P$ and $S' \lhd P'$ is a pair $t \lhd q$ of maps $t : S \to S'$ and $q : \Pi {\{s : S\}}.\, P'\,
(t\, s) \to P\, s$ (the shape map and position map). Note how the positions are mapped backwards. The intuition is that, if a function between two datatypes does not look at the data, then the shape of a data-structure given to 