& & & & & & & &
}$$

The global shape $s$ is marked with a solid boundary and has a root position ${\mathsf{o}}\, {\{s\}}$. Then, any position $p$ in $s$ determines a shape $s' = s {\mathrel{\downarrow}}p$, marked with a dotted boundary, to be thought of as the subshape of $s$ given by this position. The root position in $s'$ is ${\mathsf{o}}\, {\{s'\}}$. Law 3 says that its translation $p
{\mathrel{\oplus}}{\mathsf{o}}\, {\{s'\}}$ into a position in shape $s$ is $p$, reflecting the idea that the subshape given by a position should have that position as the root.

By law 1, the subshape $s {\mathrel{\downarrow}}{\mathsf{o}}\, {\{s\}}$ corresponding to the root position ${\mathsf{o}}{\{s\}}$ in the global shape $s$ is $s$ itself. Law 4, which is only well-typed thanks to law 1, stipulates that the translation of position $p$ in $s {\mathrel{\downarrow}}{\mathsf{o}}\, {\{s\}}$ into a position in $s$ is just $p$ (which is possible, as $P\, (s {\mathrel{\downarrow}}{\mathsf{o}}\, {\{s\}}) = P\, s$).

A further position $p'$ in $s'$ determines a shape $s'' = s'
{\mathrel{\downarrow}}p'$. But $p'$ also translates into a position $p {\mathrel{\oplus}}p'$ in $s$ and that determines a shape $s {\mathrel{\downarrow}}(p {\mathrel{\oplus}}p')$. Law 2 says that $s''$ and $s 