comonad morphism between ${\llbracket E \rrbracket^\mathrm{dc}}$ and ${\llbracket E' \rrbracket^\mathrm{dc}}$.

Since the category ${\mathbf{Comonads({{\mathbf{Set}}})}}$ inherits its identities and composition from $[{\mathbf{Set}}, {\mathbf{Set}}]$, the functor ${\llbracket - \rrbracket^\mathrm{dc}}$ also preserves the identities and composition.

${\llbracket - \rrbracket^\mathrm{dc}}$ is a functor from ${\mathbf{DCont}}$ to ${\mathbf{Comonads({{\mathbf{Set}}})}}$. \[prop:dcsemfunctor\]

Similarly to the case of natural transformations between container interpretations, one can also “quote” comonad morphisms between directed container interpretations into directed container morphisms. For any directed containers $E = (C, {{\mathrel{\downarrow}}}, {\mathsf{o}}, {{\mathrel{\oplus}}})$, $E' =
(C', {{\mathrel{\downarrow'}}}, {\mathsf{o'}}, {{\mathrel{\oplus'}}})$ and any morphism $\tau$ between the comonads ${\llbracket E \rrbracket^\mathrm{dc}}$ and ${\llbracket E' \rrbracket^\mathrm{dc}}$ (which is a natural transformation between ${\llbracket C \rrbracket^\mathrm{c}}$ and ${\llbracket C' \rrbracket^\mathrm{c}}$), the container morphism ${\ulcorner \tau \urcorner^\mathrm{dc}} = {\ulcorner \tau \urcorner^\mathrm{c}}$ between the underlying containers $C$ and $C'$ is also a directed container morphism between $E$ and $E'$. The directed container morphism laws follow from the comonad morphism laws.

From what we already know about interpretation and quoting of container morphisms, it is immediate that ${\ulcorner {\llbracket h \rrbracket^\mathrm{dc}} \urcorner^\mathrm{dc}} = h$ for any directed container morphism $h$ and that ${\ulcorner \tau \urcorner^\mathrm{dc}} =
{\ulcorner \tau' \urcorner^\mathrm{dc}}$ implies $\tau = \tau'$ for any comonad morphisms $\tau$ and $\tau'$ between directed 