{\mathrel{\cdot^\mathrm{c}}}C_1 \rrbracket^\mathrm{c}}$ defined by ${\mathsf{e}}\, x = ({{\ast}},\lambda {{\ast}}.\, x)$ and ${\mathsf{m}}\, (s,v) = ((s,\lambda p.\, {\mathsf{fst}}\,
(v\, p)), \lambda (p,p').\, {\mathsf{snd}}\, (v\, p)\, p')$ satisfying the appropriate coherence conditions.

The functor ${\llbracket - \rrbracket^\mathrm{c}}$ is a monoidal functor.

Constructions of Containers
---------------------------

Containers are closed under various constructions such as products, coproducts and constant exponentiation, preserved by interpretation.

#### Products

For two containers $C_0 = S_0 \lhd P_0$ and $C_1 = S_1 \lhd
  P_1$, their *product* $C_0 \times C_1$ is the container $S \lhd
  P$ defined by $S = S_0 \times S_1$ and $P\, (s_0, s_1) = P_0\, s_0 +
  P_1\, s_1$. It holds that ${\llbracket C_0 \times C_1 \rrbracket^\mathrm{c}} \cong {\llbracket C_0 \rrbracket^\mathrm{c}}
  \times {\llbracket C_1 \rrbracket^\mathrm{c}}$.

#### Coproducts

The *coproduct* $C_0 + C_1$ of containers $C_0 = S_0 \lhd
  P_0$ and $C_1 = S_1 \lhd P_1$ is the container $S \lhd P$ defined by $S = S_0 + S_1$, $P\, ({\mathsf{inl}}\, s) = P_0\, s$ and $P\, ({\mathsf{inr}}\, s) =
  P_1\, s$. It is the case that ${\llbracket C_0 + C_1 \rrbracket^\mathrm{c}} \cong {\llbracket C_0 \rrbracket^\mathrm{c}} +
  {\llbracket C_1 \rrbracket^\mathrm{c}}$.

#### Exponentials

For a set $K \in {\mathsf{Set}}$ and a container $C_0 = S_0 \lhd P_0$, the 