*exponential* $K \to C_0$ is the container $S \lhd P$ where $S
  = K \to S_0$ and $P\, f = \Sigma k : K.\, P \,(f\, k)$. We have that ${\llbracket K \to C_0 \rrbracket^\mathrm{c}} \cong K \to {\llbracket C_0 \rrbracket^\mathrm{c}}$.

Directed Containers {#sec:dcontainers}
===================

We now proceed to our contribution, directed containers. We define the category of directed containers and a fully-faithful functor interpreting directed containers as comonads, and discuss some examples and constructions.

Directed Containers {#sec:dcont}
-------------------

Parametrized datatypes often carry some additional structure that is worth making explicit. For example, each node in a list or non-empty list defines a sublist (a suffix). In container terms, this corresponds to every position in a shape determining another shape, the subshape corresponding to this position. The theory of containers alone does not account for such additional structure. Directed containers, studied in the rest of this paper, axiomatize subshapes and translation of positions in a subshape into the global shape.

A *directed container* is a container $S \lhd P$ together with three operations

${{\mathrel{\downarrow}}} : \Pi s : S.\, P\, s \to S$ (the subshape corresponding to a position),

${\mathsf{o}}: \Pi {\{s : S\}}.\, P\, s$ (the root),

${{\mathrel{\oplus}}} : 