interpreted as a natural transformation between ${\llbracket C \rrbracket^\mathrm{c}}$ and ${\llbracket C' \rrbracket^\mathrm{c}}$, i.e., as a polymorphic function ${\llbracket h \rrbracket^\mathrm{c}}
: \forall {\{X\}}.\, (\Sigma s: S.\, P\, s \to X) \to \Sigma s' : S'.\,
P'\, s' \to X$ that is natural. It is defined by ${\llbracket h \rrbracket^\mathrm{c}}\, (s, v) =
(t\, s, v {\circ}q\, {\{s\}})$. ${\llbracket - \rrbracket^\mathrm{c}}$ preserves the identities and composition of container morphisms.

The interpretation of the container morphism $h$ for the list head function is ${\llbracket h \rrbracket^\mathrm{c}} : \forall{\{X\}}.\, (\Sigma s: {\mathsf{Nat}}.\,
{\mathsf{Fin}}\, (s+1) \to X) \to \Sigma {{\ast}}: 1.\, 1 \to X$ defined by ${\llbracket h \rrbracket^\mathrm{c}}\, (s, v) = ({{\ast}}, \lambda {{\ast}}.\, v\, 0)$.

${\llbracket - \rrbracket^\mathrm{c}}$ is a functor from ${\mathbf{Cont}}$ to ${[{\mathbf{Set}},{\mathbf{Set}}]}$.

Every natural transformation between container interpretations is the interpretation of some container morphism. For containers $C = S \lhd
P$ and $C' = S' \lhd P'$, a natural transformation $\tau$ between ${\llbracket C \rrbracket^\mathrm{c}}$ and ${\llbracket C' \rrbracket^\mathrm{c}}$, i.e., a polymorphic function $\tau :
\forall {\{X\}}.\, (\Sigma s : S.\, P\, s \to X) \to \Sigma s':
S'.\,P'\, s' \to X$ that is natural, can be “quoted” to a container morphism ${\ulcorner \tau \urcorner^\mathrm{c}} = t 