defined by $t\, s = s * 2 + 1$ and $q\, \{s\}\, p = p \mod (s + 1)$.

-   For reversal of non-empty lists, they are $t : {\mathsf{Nat}}\to {\mathsf{Nat}}$ and $q : \Pi {\{s :
      {\mathsf{Nat}}\}}.\, {\mathsf{Fin}}\, (s + 1) \to {\mathsf{Fin}}\, (s + 1)$ defined by $t\, s = s$ and $q\, \{s\}\, p = s - p$.

(See Prince et al. [@Prince2008] for more similar examples.)

The *identity* morphism ${\mathsf{id}^\mathrm{c}}\{C\}$ on a container $C = S \lhd
P$ is defined by ${\mathsf{id}^\mathrm{c}}= {\mathsf{id}}\, {\{S\}} \lhd \lambda {\{s\}}.\, {\mathsf{id}}\,
{\{P\, s\}}$. The *composition* $h {\mathrel{\circ^\mathrm{c}}}h'$ of container morphisms $h = t \lhd q$ and $h' = t' \lhd q'$ is defined by $h {\mathrel{\circ^\mathrm{c}}}h' = t {\circ}t' \lhd \lambda {\{s\}}.\, q'\, {\{s\}} {\circ}q\, {\{t'\,
  s\}}$. Composition of container morphisms is associative, identity is the unit.

Containers form a category ${\mathbf{Cont}}$.

Interpretation of Containers
----------------------------

To map containers into datatypes made of data-structures that have the positions in some shape filled with data, we must equip containers with a “semantics”.

For a container $C = S \lhd P$, we define its *interpretation* ${\llbracket C \rrbracket^\mathrm{c}} : {\mathsf{Set}}\to {\mathsf{Set}}$ on sets by ${\llbracket C \rrbracket^\mathrm{c}}\, X = \Sigma 