to $p$. The (horizontal) composition $h_0 {\mathrel{\cdot^\mathrm{c}}}h_1$ of container morphisms $h _0 = t_0 \lhd
q_0$ and $h_1 = t_1 \lhd q_1$ is the container morphism $t \lhd q$ defined by $t\, (s, v) = (t_0\, s, t_1 {\circ}v {\circ}q_0\, {\{s\}})$ and $q\, {\{s, v\}}\, (p_0, p_1) = (q_0\, {\{s\}}\, p_0, q_1\, {\{v\,
  (q_0\, {\{s\}}\, p_0)\}}\, p_1)$. The horizontal composition preserves the identity container morphisms and the (vertical) composition of container morphisms, which means that ${-} {\mathrel{\cdot^\mathrm{c}}}{-}$ is a bifunctor.

${\mathbf{Cont}}$ has isomorphisms $\rho : \forall {\{C\}}.\, C {\mathrel{\cdot^\mathrm{c}}}{\mathsf{Id}^\mathrm{c}}\to
C$, $\lambda : \forall {\{C\}}.\, {\mathsf{Id}^\mathrm{c}}{\mathrel{\cdot^\mathrm{c}}}C \to C$ and $\alpha :
\forall {\{C,C',C''\}}.\, (C {\mathrel{\cdot^\mathrm{c}}}C') {\mathrel{\cdot^\mathrm{c}}}C'' \to C
{\mathrel{\cdot^\mathrm{c}}}(C' {\mathrel{\cdot^\mathrm{c}}}C'')$, given by $\rho = \lambda (s, v).\, s \lhd
\lambda {\{s,v\}}.\, \lambda p.\, (p, {{\ast}})$, $\lambda = \lambda
({{\ast}},v).\, v\, {{\ast}}\lhd \lambda {\{{{\ast}},v\}}.\, \lambda p.\, ({{\ast}}, p)$ and $\alpha = \lambda ((s, v), v').\, (s , \lambda p.\, (v\, p, \lambda
p'.\, v'\, (p,p'))) \lhd \linebreak \lambda {\{(s, v), v'\}}.\, \lambda
(p,(p',p'')).\, ((p, p'), p'')$. They satisfy Mac Lane’s coherence conditions.

\[prop:monoidalcategory\] The category ${\mathbf{Cont}}$ is a monoidal category.

There are also natural isomorphisms ${\mathsf{e}}: {\mathsf{Id}}\to {\llbracket {\mathsf{Id}^\mathrm{c}}\rrbracket^\mathrm{c}}$ and ${\mathsf{m}}: \forall {\{C_0,C_1\}}.\, {\llbracket C_0 \rrbracket^\mathrm{c}} {\cdot}{\llbracket C_1 \rrbracket^\mathrm{c}}$ $\to$ ${\llbracket C_0 