{\mathrel{\downarrow}}(p {\mathrel{\oplus}}p')$ are the same shape, which is marked by a dashed boundary in the figure. Finally, law 5 (well-typed only because of law 2) says that the two alternative ways to translate a position $p''$ in shape $s''$ into a position in shape $s$ agree with each other.

Lists cannot form a directed container, as the shape $0$ (for the empty list), having no positions, has no possible root position.

But the container of *non-empty lists* (with $S = {\mathsf{Nat}}$ and $P\,s
= {\mathsf{Fin}}\,(s +1)$) is a directed container with respect to *non-empty suffixes* as sublists. The subshape given by a position $p$ in a shape $s$ (for lists of length $s+1$) is the shape of the corresponding suffix, given by $s {\mathrel{\downarrow}}p = s - p$. The root ${\mathsf{o}}\, {\{s\}}$ is the position $0$ of the head node. A position in the global shape is recovered from a position $p'$ in the subshape of the position $p$ by $p {\mathrel{\oplus}}p' = p + p'$.

Fig. \[fig:dcontainernelist\] shows an example of the shape and positions of a non-empty list with length 6, i.e., with shape $s = 5$. This figure also shows that the subshape determined by a position 