\lhd q$ between $C$ and $C'$ where $t : S \to
S'$ and $q : \Pi {\{s : S\}}.\, P'\, (t\, s) \to P\, s$ are defined by ${\ulcorner \tau \urcorner^\mathrm{c}} = (\lambda s.\, {\mathsf{fst}}\, (\tau\, {\{P\, s\}}\, (s, {\mathsf{id}})))
\lhd (\lambda {\{s\}}.\, {\mathsf{snd}}\, (\tau\, {\{P\, s\}}\, (s, {\mathsf{id}})))$.

For any container morphism $h$, ${\ulcorner {\llbracket h \rrbracket^\mathrm{c}} \urcorner^\mathrm{c}} = h$, and, for any natural transformation $\tau$ and $\tau'$ between container interpretations, ${\ulcorner \tau \urcorner^\mathrm{c}} = {\ulcorner \tau' \urcorner^\mathrm{c}}$ implies $\tau = \tau'$.

\[prop:csemfullyfaithful\] ${\llbracket - \rrbracket^\mathrm{c}}$ is fully faithful.

Monoidal Structure
------------------

We have already seen the *identity* container ${\mathsf{Id}^\mathrm{c}}= 1 \lhd \lambda {{\ast}}.\, 1$. The *composition* $C_0 {\mathrel{\cdot^\mathrm{c}}}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 = \Sigma s : S_0.\, P_0\, s \to
S_1$ and $P\, (s, v) = \Sigma p_0 : P_0\, s.\, P_1\, (v\, p_0)$. It has as shapes pairs of an outer shape $s$ and an assignment of an inner shape to every position in $s$. The positions in the composite container are pairs of a position $p$ in the outer shape and a position in the inner shape assigned 