But we will present a proof of this fact from an alternative perspective: by appealing to the left coclosure of $\tri$.

The composition product is left coclosed.
That is, there exists a left coclosure operation, which we denote $\lchom{-}{-}\colon\poly\op\times\poly\to\poly$,
such that there is a natural isomorphism

\begin{equation} \label{eqn.lchom_adj_iso}
\poly(p, r\tri q)\iso\poly\left(\lchom{q}{p}, r\right).
\end{equation}

In particular, the left coclosure operation sends $q,p\in\poly$ to

\begin{equation} \label{eqn.lchom_def}
\lchom{q}{p}\coloneqq\sum_{i\in p(\1)}\yon^{q(p[i])}.
\end{equation}

We present an argument using polyboxes; we leave it to the reader to write this proof in more standard mathematical notation in <ref>.

As in <ref>, a lens $\varphi\colon p\to r\tri q$ can be written as follows:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p$" left] (p) {$a$\at$i$};
\node[poly, cod, right=1.5cm of p.south, yshift=-1ex, "$r$" right] (r) {$c$\at$k$};
\node[poly, cod, above=of r, "$q$" right] (q) {$b$\at$j$};
\draw (p_pos) to[first] node[below] {$\varphi^r$} (r_pos);
\draw (r_dir) to[climb] node[right] {$\varphi^q$} (q_pos);
\draw (q_dir) to[last] node[above] {$\varphi^\sharp$} (p_dir);
\end{tikzpicture}
\]

But this is equivalent to the following gadget (to visualize this equivalence, imagine leaving the positions box for $p$, the arrow $\varphi^r$, and the polyboxes for $r$ untouched, while dragging the polyboxes for $q$ leftward to the directions box for $p$, merging all the data from $q$ and the arrows $\varphi^q$ and $\varphi^\sharp$ into a single on-directions arrow and directions box):

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\lchom{q}{p}$" left] (l) {$(j,\varphi^\sharp)$\at$i$};
\node[poly, cod, "$r$" right, right=of l, yshift=-0.5ex] (r) {$c$\at$k$};
\draw (l_pos) -- node[below] {$\varphi^r$} (r_pos);
\draw (r_dir) -- node[above] {} (l_dir);
\end{tikzpicture}
\]

Here the on-directions function encodes the behaviors of both $\varphi^q$ and $\varphi^\sharp$ by sending each $r[k]$-direction $c$ to both a $q$-position $j$, as $\varphi^q$ does, and a function sending $q[j]$-directions to $p[i]$-directions, as $\varphi^\sharp$ does.
So the polyboxes on the left represent a polynomial whose positions are the same as those of $p$, but whose directions at $i\in p(\1)$ are pairs $(j,\varphi^\sharp)$ consisting of a $q$-position $j$ and a function $\varphi^\sharp\colon q[j]\to p[i]$.
Such pairs are precisely the elements of $q(p[i])$, so the polynomial represented by the polyboxes on the left is indeed the one defined as $\lchom{q}{p}$ in (<ref>).
It follows that there is a natural isomorphism between lenses $p\to r\tri q$ and lenses $\lchom{q}{p}\to r$.

Translate the polyboxes proof of <ref> into standard mathematical notation, i.e. the $\sum$ and $\prod$ notation we have been using up till now.

We prove <ref> by observing that

\begin{align*}
\poly(p,r\tri q)&\iso\prod_{i\in p(\1)}r(q(p[i])) \tag*{\eqref{eqn.main_formula}} \\
&\iso\poly\left(\sum_{i\in p(\1)}\yon^{q(p[i])}, r\right) \tag*{\eqref{eqn.main_formula}} \\
&\iso\poly\left(\lchom{q}{p}, r\right) \tag*{\eqref{eqn.lchom_def}}.
\end{align*}

The proof you came up with in <ref> may be more obviously rigorous and concise than the one we presented in the main text.
But polyboxes help us see right on paper exactly what is going on in this adjunction: how data on the codomain-side of a lens $p\to r\tri q$ can be simply repackaged and transferred to the domain-side of a new lens $\lchom{q}{p}\to r$.

In stating <ref>, we implicitly assumed that $\lchom{-}{-}$ is a functor $\poly\op\times\poly\to\poly$.
Here we show that this is indeed the case.

* Given a polynomial $q$ and a lens $\varphi\colon p\to p'$, to what lens $\lchom{q}{p}\to\lchom{q}{p'}$ should the covariant functor $\lchom{q}{-}$ send $\varphi$?
Prove that your construction is functorial.

* Given a polynomial $p$ and a lens $\psi\colon q'\to q$, to what lens $\lchom{q}{p}\to\lchom{q'}{p}$ should the contravariant functor $\lchom{-}{p}$ send $\psi$?
Prove that your construction is functorial.

* Given a polynomial $q$ and a lens $\varphi\colon p\to p'$, the functor $\lchom{q}{-}$ should send $\varphi$ to a lens $\lchom{q}{p}\to\lchom{q}{p'}$; by (<ref>), this is a lens

\[
\lchom{q}{\varphi}\colon\sum_{i\in p(\1)}\yon^{q(p[i])}\to\sum_{i'\in p'(\1)}\yon^{q(p'[i'])}.
\]

We give $\lchom{q}{\varphi}$ the same on-positions function $p(\1)\to p'(\1)$ that $\varphi$ has.
Then viewing $q$ as a functor, we define the on-directions function $\lchom{q}{\varphi}^\sharp_i\colon q(p'[\varphi_\1(i)])\to q(p[i])$ for each $i\in p(\1)$ to be the function obtained by applying $q$ to the corresponding on-directions function $\varphi^\sharp_i\colon p'[\varphi_\1(i)]\to p[i]$.
Functoriality follows trivially on positions and by the functoriality of $q$ itself on directions.

* Given a polynomial $p$ and a lens $\psi\colon q'\to q$, the functor $\lchom{-}{p}$ should send $\psi$ to a lens $\lchom{q}{p}\to\lchom{q'}{p}$; by (<ref>), this is a lens

\[
\lchom{\psi}{p}\colon\sum_{i\in p(\1)}\yon^{q(p[i])}\to\sum_{i\in p(\1)}\yon^{q'(p[i])}.
\]

We let the on-positions function of $\lchom{\psi}{p}$ be the identity on $p(\1)$.
Then viewing $\psi$ as a natural transformation, we define the on-directions function $\lchom{\psi}{p}^\sharp_i\colon q'(p[i])\to q(p[i])$ for each $i\in p(\1)$ to be the $p[i]$-component of $\psi$.
Functoriality follows trivially on positions and because natural transformations compose componentwise on directions.

In personal communication, Todd Trimble noted that the left coclosure can be thought of as a left Kan extension

\[
\begin{tikzcd}
\smset\ar[r, "p"]\ar[d, "q"']\ar[dr, phantom, very near start, "\Downarrow"]&
\smset\\
\smset\ar[ur, "\lchom{q}{p}"']&~
\end{tikzcd}
\]

Verify this.

In order for $\lchom{q}{p}$ to be a left Kan extension of $p$ along $q$, we need to first provide a natural transformation $p\to \lchom{q}{p}\tri q$, and second show that it is universal. But this is exactly the content of <ref>: the adjunction (<ref>) provides a unit $p\to \lchom{q}{p}\tri q$ that is universal in the appropriate way.

Let $A$ and $B$ be sets, and let $p$ and $q$ be polynomials.

* Prove that the following natural isomorphism holds:

\begin{equation}\label{eqn.monomials_and_comp}
\poly(A\yon^B,p)\iso\smset(A,p(B)).
\end{equation}

* Prove that the following natural isomorphism holds:

\begin{equation}\label{eqn.flip_reps_lins}
\poly\left(A\yon\tri p\tri \yon^B, q\right)\iso\poly\left(p,\yon^A\tri q\tri By\right).
\end{equation}

(Hint: Break the isomorphism down into two parts.
You may find (<ref>) helpful.)

We are given $A,B\in\smset$ and $p,q\in\poly$

* By (<ref>),

\[
\lchom{B}{A}=\sum_{i\in A}\yon^{B}\iso A\yon^B,
\]

so by (<ref>),

\[
\poly(A\yon^B,p)\iso\poly(A,p\tri B).
\]

But $A$ and $p\tri B\iso p(B)$ are both constants, so a lens $A\to p\tri B$ is just a function $A\to p(B)$ on positions.
Hence (<ref>) follows.

* We prove (<ref>) in two parts: that

\begin{equation} \label{eqn.flipping1}
\poly\left(A\yon\tri p, q\right)\iso\poly\left(p,\yon^A\tri q\right)
\end{equation}

and that

\begin{equation} \label{eqn.flipping2}
\poly\left(p \tri \yon^B, q\right)\cong\poly\left(p, q\tri B\yon\right).
\end{equation}

We have that $A\yon \tri p \iso Ap$ and $\yon^A \tri q \iso q^A$, so (<ref>) follows from (<ref>).
Meanwhile, for (<ref>), we have by (<ref>) that

\[
\lchom{B\yon}{p}=\sum_{i\in p(\1)}\yon^{Bp[i]}\iso p\tri\yon^B,
\]

so (<ref>) follows from (<ref>).
Then combining (<ref>) and (<ref>) yields

\[
\poly\left(A\yon\tri p\tri\yon^B,q\right)\iso\poly\left(p\tri\yon^B,\yon^A\tri q\right)\iso\poly\left(p,\yon^A\tri q\tri B\yon\right).
\]

[Dynamical systems as coalgebras]
Taking $A=B=S\in\smset$ in (<ref>), we find that there is a natural isomorphism between dynamical systems $S\yon^S\to p$ and functions $S\to p(S)$.
Such a function is known as a coalgebra for the functor $p$ or a $p$-coalgebra.
There are two versions of coalgebras we are interested in (and more that we are not) with distinct definitions: a coalgebra for a functor, which is the version used here, and a coalgebra for a comonad, which is a coalgebra for a functor with extra conditions that we will introduce later in <ref>.
The version we are using will usually be clear from context—here, for example, we do not expect $p$ to be a comonad—but we will try to be explicit with our terminology whenever the interpretation may be ambiguous.

Coalgebras as models of dynamical systems have been studied extensively in the context of computer science, most notably by Jacobs in <cit.>.
Indeed, much of what we developed in  stems from the theory of coalgebras.
The coalgebraic perspective has the benefit of staying in the familiar category of sets; moreover, it can be generalized to functors $\smset\to\smset$ that are not polynomial, although many of the interesting examples are.

On the other hand, we have already seen that viewing dynamical systems as lenses $S\yon^S\to p$ rather than as functions $S\to p(S)$ has the benefit of isolating the internal state system to the domain and the external interface to the codomain, aiding both intuition and functionality.
Plus, our adjunction lets us switch to the coalgebraic perspective whenever we see fit: $\poly$ lets us talk about both.

The operation $\tri$ preserves limits on the left (up to natural isomorphism).
That is, if $\cat{J}$ is a category, $p_-\colon\cat{J}\to\poly$ is a functor, and $q\in\poly$ is a polynomial, then there is a natural isomorphism

\begin{equation} \label{eqn.comp_left_pres_lim}
\left(\lim_{j\in\cat{J}}p_j\right)\tri q\iso\lim_{j\in\cat{J}}(p_j\tri q).
\end{equation}

By <ref>, the functor $(-\tri q)\colon\poly\to\poly$ is the right adjoint of the functor $\lchom{q}{-}\colon\poly\to\poly$, and right adjoints preserve limits.

* Complete <ref> <ref> using (<ref>) and (<ref>).

*  Deduce (<ref>) using (<ref>).

* We wish to solve <ref> <ref> using (<ref>) and (<ref>).
If we set $\cat{J}$ in (<ref>) to be the empty category, then the limit of the functor from $\cat{J}$ is just the terminal object.
It follows that $\1\tri p\iso\1$.
In other words, since $\tri$ preserves limits on the left, and since terminal objects are limits, $\tri$ preserves terminal objects on the left.

Then a set $X$ can be written as a sum $\sum_{x\in X}\1$, so by (<ref>),

\[
X\tri p\iso\left(\sum_{x\in X}\1\right)\tri p\iso\sum_{x\in X}(\1\tri p)\iso\sum_{x\in X}\1\iso X.
\]

* If we set $\cat{J}$ in (<ref>) to be the discrete category on the set $A$, then the limit of a functor from $\cat{J}$ is just an $A$-fold product, so (<ref>) follows.
In other words, since $\tri$ preserves limits on the left, and since products are limits, $\tri$ preserves products on the left.

§.§ Interaction with limits on the right

So $\tri$ preserves limits on the left.
How about limits on the right?
We saw in <ref> that $\tri$ does not even preserve products on the right, so it certainly does not preserve all limits.
But it turns out that there is a special class of limits that $\tri$ does preserve on the right.

A connected limit is one whose indexing category $\cat{J}$ is nonempty and connected. That is, $\cat{J}$ has at least one object, and any two objects are connected by a finite zigzag of arrows.

The following categories are connected:

\[
\fbox{$\bullet$}
\qquad
\fbox{$\bullet\tto\bullet$}
\qquad
\fbox{$\bullet\to\bullet\from\bullet$}
\qquad
\fbox{$\bullet\from\bullet\from\bullet\from\cdots$}
\]

In particular, equalizers, pullbacks, and directed limits are examples of connected limits.

The following categories are not connected:

\[
\fbox{$\phantom{\bullet}$}
\qquad
\fbox{$\bullet\quad\bullet$}
\qquad
\fbox{$\bullet\quad\bullet\to \bullet$}
\]

In particular, terminal objects and products are not examples of connected limits.

Connected limits are intimately related to slice categories, which we defined back in <ref>.
For example, products in a slice category $\cat{C}/c$ are just pullbacks in $\cat{C}$, allowing us to view a non-connected limit as a connected one.
By relating $\poly$ to its slice categories via an adjunction, we'll be able to show that $\tri$ preserves connected limits.
(An alternative proof of this fact can be found in <cit.>.)

Recall that objects in a slice category $\cat{C}/c$ are just morphisms with codomain $c$.
For ease of notation, we'll often suppress the actual morphism and just write down the name of its domain when there is a canonical choice for the morphism, or when it is clear from context.
So for example, on the left hand side of (<ref>) below, $p$ represents the lens $f\colon p\to q\tri 1$ and $q\tri r$ represents the lens $q\:\tri\:!\colon q\tri r\to q\tri\1$, both objects in the slice category $\poly/q\tri\1$.

Given polynomials $p,q,r\in\poly$ and a function $f\colon p\to q\tri\1$, there is a natural isomorphism

\begin{equation} \label{eqn.rchom_adj_iso}
\poly/(q\tri\1)\left(p, q\tri r\right)\iso\poly\left(p\rchom{f}q, r\right),
\end{equation}

\begin{equation} \label{eqn.rchom_def}
p\rchom{f}q\coloneqq\sum_{i\in p(\1)}q[f(i)]\yon^{p[i]}.
\end{equation}

Again, we present an argument using polyboxes; we leave it to the reader to write this proof in more standard mathematical notation in <ref>.

Note that to consider $q\tri r$ as an object in $\poly/(q\tri\1)$, we are implicitly using the lens $q\:\tri\:!\colon q\tri r\to q\tri 1$. By definition, morphisms from $f$ to $q\:\tri\:!$ in $\poly/(q\tri\1)$ are lenses $\varphi\colon p\to q\tri r$ for which $\varphi\then(q\:\tri\:!)=f$.
We can write this equation using polyboxes:

\[
\begin{tikzpicture}
\node (a) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p$" left] (p) {\at$i$};
\node[poly, right=1.8 of p.south, yshift=-2.5ex, "$q$" below] (q) {$b$\at$j$};
\node[poly, above=.8 of q, "$r$" above] (r) {\at$k$};
\node[poly, cod, right=of q, "$q$" right] (q') {$b$\at$j$};
\node[poly, terminal, above=.8 of q', "$\1$" right] (1) {};
\draw[double, -] (q_pos) -- node[below] {} (q'_pos);
\draw[double, -] (q'_dir) -- node[above] {} (q_dir);
\draw (r_pos) -- node[below] {} (1_pos);
\draw[densely dotted] (1_dir) -- node[above] {} (r_dir);
\draw (p_pos) to[first] node[below] {$\varphi^q$} (q_pos);
\draw (q_dir) to[climb] node[right] {$\varphi^r$} (r_pos);
\draw (r_dir) to[last] node[above] {$\varphi^\sharp$} (p_dir);
\end{tikzpicture}
\node[right=1.8 of a] (b) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p$" left] (p) {\at$i$};
\node[poly, cod, right=1.8 of p.south, yshift=-1ex, "$q$" right] (q) {$b$\at$f(i)$};
\node[poly, terminal, above=of q, "$\1$" right] (1) {};
\draw (p_pos) to[first] node[below] {$f$} (q_pos);
\draw (q_dir) to[climb] node[right] {} (1_pos);
\draw[densely dotted] (1_dir) to[last] node[above] {$!$} (p_dir);
\end{tikzpicture}
\node at ($(a.east)!.5!(b.west)$) {=};
\end{tikzpicture}
\]

We can read off the picture that a lens $\varphi\colon p\to q\tri r$ is a morphism from $f$ to $q\:\tri\:!$ in $\poly/q\tri\1$ if and only if $\varphi^q=f_\1$.

So morphisms from $f$ to $q\:\tri\:!$ are equivalent to gadgets

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p$" left] (p) {$a$\at$i$};
\node[poly, cod, right=1.8 of p.south, yshift=-2.5ex, "$q$" below] (q) {$b$\at$f_\1(i)$};
\node[poly, cod, above=.8 of q, "$r$" above] (r) {$c$\at$k$};
\draw (p_pos) to[first] node[below] {$f$} (q_pos);
\draw (q_dir) to[climb] node[right] {$\varphi^r$} (r_pos);
\draw (r_dir) to[last] node[above] {$\varphi^\sharp$} (p_dir);
\end{tikzpicture}
\]

with $f_\1$ fixed.
But this, in turn, is equivalent to the following gadget (to visualize this equivalence, imagine leaving the polyboxes for $r$, the arrow $\varphi^\sharp$, and the directions box for $p$ untouched, while dragging the polyboxes for $q$ leftward to the positions box for $p$, merging the data from $q$ and the predetermined arrow $f$ into a single positions box and adapting the arrow $\varphi^r$ into an on-positions arrow):

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p\rchom{f}q$" left] (h) {$a$\at$(i,b)$};
\node[poly, cod, "$r$" right, right=of h] (r) {$c$\at$k$};
\draw (h_pos) -- node[below] {$\varphi^r$} (r_pos);
\draw (r_dir) -- node[above] {$\varphi^\sharp$} (h_dir);
\end{tikzpicture}
\]

Here the user can provide both the $p$-position $i$ and the $q[f(i)]$-direction $b$ right from the start, as they know what to expect from $f$ ahead of time.
Then the on-positions function encodes the behavior of $\varphi^r$.
So the polyboxes on the left represent a polynomial whose positions are pairs $(i,b)$ with $i\in p(\1)$ and $b\in q[f(i)]$, and whose directions at $(i,b)$ are the directions of the original polynomial $p$ at $i$.
This is precisely the polynomial we defined in (<ref>), so the isomorphism holds.

As a lens $p\to q\tri\1$ can be identified with its on-positions function $p(\1)\to q(\1)$, we'll use the notation $p\rchom{f}q$ interchangeably for lenses $f\colon p\to q\tri\1$ and functions $f\colon p(\1)\to q(\1)$.

* Translate the polyboxes proof of <ref> into standard mathematical notation.

* Prove that the following natural isomorphism holds:

\begin{equation}
\poly(p,q\tri r)\iso\sum_{f\colon p(\1)\to q(\1)}\poly\left(p\rchom{f}q,r\right).
\end{equation}

Thus the functor $(q\tri-)\colon\poly\to\poly$ is said to have a left multiadjoint.

* Note that $\poly(p,q\tri \1)\cong\smset(p(1),q(1))$. A lens $p\to q\tri r$ is an element of

\[
\prod_{i\in p(\1)}\sum_{j\in q(\1)}\prod_{b\in q[j]}\sum_{k\in r(\1)}\prod_{c\in r[k]}p[i]\cong\sum_{f\colon p(\1)\to q(\1)}\prod{i\in p(1)}\prod_{b\in q[j]}\sum_{k\in r(\1)}\prod_{c\in r[k]}p[i]
\]

Fixing the function $f\colon p(\1)\to q(\1)$ as implicit in $p$, we get

\begin{align*}
\poly/(q\tri\1)\left(p, q\tri r\right)&\cong
\prod{i\in p(1)}\prod_{b\in q[j]}\sum_{k\in r(\1)}\prod_{c\in r[k]}p[i]\\&\cong
\poly\left(p\rchom{f}q, r\right),
\end{align*}

* This follows from the first isomorphism above.

In stating <ref>, we implicitly assumed that $p\rchom{f}q\in\poly$ is functorial in each variable: covariantly on the left and contravariantly on the right.
Here we show that this is indeed the case.

* Given lenses $f\colon p\to q\tri\1$ and $g\colon p'\to p$, to what lens $p'\rchom{g\then f}q\to p\rchom{f}q$ should the covariant functor $-\rchom{f}q$ send $g$?
Prove that your construction is functorial.

* Given lenses $f\colon p\to q\tri\1$ and $h\colon q\to q'$, to what lens $p\rchom{f\then(h\tri\1)}q'\to p\rchom{f}q$ should the contravariant functor $p\rchom{f}-$ send $h$?
Prove that your construction is functorial.

* Given lenses $f\colon p\to q\tri\1$ and $g\colon p'\to p$, the functor $-\rchom{f}q$ should send $g$ to a lens $p'\rchom{g\then f}q\to p\rchom{f}q$; by (<ref>), this is a lens

\[
g\rchom{f}q\colon\sum_{i'\in p'(\1)}q[f_\1(g_\1(i'))]\yon^{p'[i']}\to\sum_{i\in p(\1)}q[f_\1(i)]\yon^{p[i]}.
\]

We give $g\rchom{f}q$ an on-positions function that is the on-positions function $p'(\1)\to p(\1)$ of $g$ on the first coordinate $i'\in p'(\1)$ and the identity on $q[f_\1(g_\1(i'))]$ on the second.
Then we let the on-directions function at every position with first coordinate $i'\in p'(\1)$ be the on-directions function $g^\sharp_{i'}\colon p[g_\1(i')]\to p'[i']$.
Functoriality follows trivially on both positions and directions.

* Given a polynomial $p$ and lenses $f\colon p\to q\tri\1$ and $h\colon q\to q'$, the functor $p\rchom{f}-$ should send $h$ to a lens $p\rchom{f\then(h\tri\1)}q'\to p\rchom{f}q$; by (<ref>), this is a lens

\[
p\rchom{f}h\colon\sum_{i\in p(\1)}q'[h_\1(f_\1(i))]\yon^{p[i]}\to\sum_{i\in p(\1)}q[f_\1(i)]\yon^{p[i]}.
\]

We let the on-positions function of $p\rchom{f}h$ be the identity on the first coordinate $i\in p(\1)$ and the on-directions function $h^\sharp_{f_\1(i)}\colon q'[h_\1(f_\1(i))]\to q[f_\1(i)]$ on the second.
Then we let the on-directions function at every position with first coordinate $i\in p(\1)$ be the identity on $p[i]$.
Functoriality follows trivially on both positions and directions.

The operation $\tri$ preserves connected limits on both sides.
That is, if $\cat{J}$ is a connected category, $p\colon \cat{J}\to\poly$ is a functor, and $q\in\poly$ is a polynomial, then there are natural isomorphisms

\[
\left(\lim_{j\in \cat{J}} p_j\right)\tri q\iso \lim_{j\in \cat{J}}(p_j\tri q)
\qqand
q\tri\left(\lim_{j\in \cat{J}} p_j\right)\iso \lim_{j\in \cat{J}}(q\tri p_j)
\]

The claim for the left side is just a special case of <ref>; it remains to prove the claim on the right.

By <ref>, $\poly$ is complete, so by <cit.>, it suffices to show that the functor $(q\tri-)\colon\poly\to\poly$ preserves wide pullbacks on the right.
By <ref>, the functor $(q\tri-)\colon\poly\to\poly/q\tri\1$ is a right adjoint, so it preserves limits, including wide pullbacks.
Thus $(q\tri-)$ sends a wide pullback over $r\in\poly$ to a wide pullback over the canonical lens $q\tri r\to q\tri\1$ in $\poly/q\tri\1$, corresponding to a limit in $\poly$ of a diagram consisting of arrows to $q\tri r$ and arrows to $q\tri\1$ factoring through $q\tri r$.
So up to isomorphism, this limit is just a wide pullback in $\poly$ over $q\tri r$, namely $(q\tri-)\colon\poly\to\poly$ applied to the original wide pullback.
So $\tri$ preserves wide pullbacks on the right.

Use <ref> in the following.

* Let $p$ be a polynomial, thought of as a functor $p\colon\smset\to\smset$. Show that $p$ preserves connected limits (of sets).

* Show that for any polynomials $p,q,r$ we have an isomorphism:

\begin{equation} \label{eqn.right_prod_pullback}
p\tri(qr)\iso (p\tri q)\times_{(p\tri\1)}(p\tri r).
\end{equation}

* Take the polynomials $p,q,r$ from the counterexample you found in <ref> <ref> and check that (<ref>) holds.

* Given a polynomial functor $p \colon \smset \to \smset$, we wish to show that $p$ preserves connected limits of sets; that is, for a connected category $\cat{J}$ and a functor $X \colon \cat{J} \to \smset$, we have

\[
p\left(\lim_{j \in \cat{J}} X_j\right) \iso \lim_{j \in \cat{J}} p(X_j).
\]

But we can identify $\smset$ with the full subcategory of constant functors in $\poly$ and instead view $X$ as a functor into $\poly$.
Then by <ref> <ref>, the left hand side of the isomorphism we seek is isomorphic to $p\tri\left(\lim_{j \in \cat{J}} X_j\right)$, while the right hand side is isomorphic to $\lim_{j \in \cat{J}} \left(p \tri X_j\right)$.
These are isomorphic by <ref>.

* Given $p,q,r \in \poly$, we wish to show that (<ref>) holds.
As $\1$ is terminal in $\poly$, the product $qr$ can also be written as the pullback $q \times_\1 r$.
While products are not connected limits, pullbacks are, so by <ref>, they are preserved by precomposition with $p$.
Hence the desired isomorphism follows.

* We'll show that (<ref>) holds for $p\coloneqq\yon+\1, q\coloneqq\1,$ and $r\coloneqq\0$.
We have $p\tri q = p\tri\1 \iso (\yon+\1)\tri\1 \iso \2$ and $p\tri r \iso (\yon+\1)\tri\0 \iso \1$, so $(p\tri q)\times_{(p\tri\1)}(p\tri r) \iso \2 \times_\2 \1$.
We saw in <ref> that the position-set of a pullback in $\poly$ is just the pullback of the position-sets in $\smset$, while the direction-sets are given by a pushout of direction-sets in $\smset$.
As our polynomials have empty direction-sets, their pullback must have an empty direction-set as well, so this pullback is just a pullback of sets: $(p\tri q)\times_{(p\tri\1)}(p\tri r) \iso \2 \times_\2 \1\iso\1$.
And indeed we have $p\tri(qr) \iso (\yon+\1)\tri\0 \iso \1$ as well.

While we're here, it will be helpful to record the following.

For any polynomial $q\in\poly$, tensoring with $q$ (on either side) preserves connected limits. That is, if $\cat{J}$ is connected and $p\colon \cat{J}\to\poly$ is a functor, then there is a natural isomorphism:

\[
\left(\lim_{j\in \cat{J}} p_j\right)\otimes q\cong
\lim_{j\in \cat{J}} (p_j\otimes q).
\]

§.§ Interaction with parallel products

Before we get into how $\otimes$ interacts with $\tri$, here is a warm-up exercise.

Let $A$ and $B$ be arbitrary sets, and let $p$ be an arbitrary polynomial.
Which of the following isomorphisms always hold?

If the isomorphism does not always hold, is there still a canonical lens in one direction or the other?

* $(A\yon)\otimes(B\yon) \iso^? (A\yon)\tri (B\yon)$.

* $\yon^A\otimes\yon^B\iso^?\yon^A\tri\yon^B$.

* $A\otimes B\iso^? A\tri B$.

* $B\yon\otimes p\iso^? B\yon\tri p$.

* $\yon^A\otimes p\iso^? \yon^A\tri p$.

* $p\otimes B\yon\iso^? p\tri B\yon$.

* $p\otimes \yon^A\iso^? p\tri\yon^A$.

What do all of the lenses you found in this exercise have in common (whether or not they were isomorphisms)?

Here $A$ and $B$ are sets and $p$ is a polynomial.

* The isomorphism always holds: we have that $(A\yon)\otimes(B\yon) \iso AB\yon \iso (A\yon)\tri (B\yon)$.

* The isomorphism always holds: we have that $\yon^A\otimes\yon^B \iso \yon^{AB} \iso \yon^A\tri\yon^B$.

* The isomorphism does not always hold: while $A\otimes B \iso AB$, we have that $A\tri B \iso A$.
There is, however, always a canonical projection $AB\to B$; but there is not always a canonical lens $B\to AB$ (for example, take $A=\0\neq B$).

* The isomorphism always holds: we have that $B\yon \otimes p \iso \sum_{i \in p(\1)} B\yon \otimes \yon^{p[i]} \iso \sum_{i \in p(\1)} B\yon^{p[i]} \iso Bp \iso B\yon\tri p$.

* The isomorphism does not always hold: if, say, $p = B$, then $\yon^A \otimes B \iso B$, while $\yon^A \tri B \iso B^A$.
If $A=B=\0$, then $B^A\iso\1$, so there is not always a canonical lens from right to left, either.
There is, however, always a canonical lens from left to right: $\yon^A\otimes p\iso\sum_{i \in p(\1)}\yon^{Ap[i]}$ while $\yon^A\tri p\iso\sum_{\ol{i}\colon A\to p(\1)}\yon^{\sum_{a\in A}p[\ol{i}(a)]}$.
So there is a lens from left to right whose on-positions function sends $i\in p(\1)$ to the constant function $A\to p(\1)$ that always evaluates to $i$; and whose on-directions function at $i$ is the identity on $Ap[i]$.

* The isomorphism does not always hold: if, say, $p = \yon^A$, then $\yon^A \otimes B\yon \iso B\yon^A$, while $\yon^A \otimes B\yon \iso (B\yon)^A \iso B^A\yon^A$.
If $A=B=\0$, then $B\yon^A\iso\0$ while $B^A\yon^A\iso\0^\0\yon^\0\iso\1$, so there is not always a canonical lens from right to left, either.
There is, however, always a canonical lens from left to right: $p\otimes B\yon\iso Bp$ while $p\tri B\yon\iso\sum_{i\in p(\1)}\sum_{\ol{b}\colon p[i]\to B}\yon^{\sum_{a\in p[i]}\1}\iso\sum_{i\in p(\1)}B^{p[i]}\yon^{p[i]}$.
So there is a lens from left to right whose on-positions function sends $(b,i)\in Bp(\1)$ to $(i,c_b)\in\sum_{i\in p(\1)}B^{p[i]}$, where $c_b\colon p[i]\to B$ is the constant function that always evaluates to $b$; and whose on-directions function at $(b,i)$ is the identity on $p[i]$.

* The isomorphism always holds: we have that $p \otimes \yon^A \iso \sum_{i \in p(\1)} \yon^{Ap[i]} \iso p \tri \yon^A$.

Every on-directions function of every lens we found in this exercise are isomorphisms, so every lens we found in this exercise is cartesian.

[Lenses from $\otimes$ to $\tri$]
For any $p$ and $q$, there is an interesting cartesian lens $o_{p,q}\colon p\otimes q\to p\tri q$ that, stated informally, “orders” the operation, taking the symmetric monoidal product $\otimes$ and reinterprets it as a special case of the asymmetric monoidal product $\tri$.
Defining this lens in the usual way is rather tedious and unilluminating, but written in polyboxes, the lens looks like this (recall that positions of $p\otimes q$ are just pairs of positions of $p$ and $q$, while directions at each such pair are pairs of directions of $p$ and $q$, one at each position in the pair; we drop the parentheses around the ordered pair for readability):

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$p\otimes q$" left] (p) {$a,b$\at$i,j$};
\node[poly, cod, "$p$" right, right= 1.5cm of p.south, yshift=-1ex] (q) {$a$\at$i$};
\node[poly, cod, "$q$" right, above=of q] (r) {$b$\at$j$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\]

Usually, the positions box of $q$ is allowed to depend on the directions box of $p$ in the polyboxes for $p\tri q$ on its own.
But in the polyboxes above, $j$ is not allowed to depend on $a$ in $p\otimes q$ on the left, so the arrow from the positions box of $q$ to the directions box of $p$ on the right doesn't actually take $a$ into account at all.
So the lens $o_{p,q}$ is in some sense the inclusion of the order-independent positions of $p\tri q$; when drawn as trees, the positions in its image are the ones whose upper-level corollas are all the same.
And of course we can flip the order using the symmetry $q\otimes p\iso p\otimes q$.
This is, we just as well have a lens $p\otimes q\to q\tri p$.

Both $\otimes$ and $\tri$ have the same monoidal unit, the identity functor $\yon$, whose identity is the unique lens $\yon\to\yon$.
In fact the lenses $o_{p,q}$ constitute a lax monoidal functor $(\poly,\yon,\otimes)\to(\poly,\yon,\tri)$.
In particular, $o_{p,q}$ commutes with associators and unitors.

This can be used in the following way. Lenses $p\to q\tri r$ into composites are fairly easy to understand (through polyboxes, for example), whereas lenses $q\tri r\to p$ are not so easy to think about. However, given such a lens, one may always compose it with $o_{q,r}$ to obtain a lens $q\otimes r\to p$.
This is quite a bit simpler to think about: they are our familiar interaction patterns from <ref>.

It turns out that the monoidal structures $\otimes$ and $\tri$ together satisfy an interesting property known as duoidality.
We won't give the entire definition of what it means for two monoidal structures to be duoidal here—there are a few commutative diagrams to verify for technical reasons—but the key condition is that there is a natural lens

\begin{equation} \label{eqn.duoidal}
(p\tri p')\otimes(q\tri q')\to(p\otimes q)\tri(p'\otimes q').
\end{equation}

The monoidal structures $(\yon,\otimes)$ and $(\yon,\tri)$ together comprise a duoidal structure on $\poly$.

The key is to give the natural lens from (<ref>), as follows.
A position of $p\tri p'$ is a pair $(i,\ol{i'})$ with $i\in p(\1)$ and $\ol{i'}\colon p[i]\to p'(\1)$; similarly, a position $q\tri q'$ is a pair $(j,\ol{j'})$ with $j\in q(\1)$ and $\ol{j'}\colon q[j]\to q'(\1)$.
So we can define the first two parts of the lens using polyboxes, like so (again we drop parentheses around some ordered pairs for readability):

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$(p\tri p')\otimes(q\tri q')$" left] (p) {\at$(i,\ol{i'}),(j,\ol{j'})$};
\node[poly, cod, "$p\otimes q$" right, right=2.5 of p.south, yshift=-1ex] (q) {$a,b$\at$i,j$};
\node[poly, cod, "$p'\otimes q'$" right, above=of q] (r) {$a',b'$\at$\ol{i'}(a),\ol{j'}(b)$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\]

Here $(a,b)$ is a direction of $p\otimes q$ at $(i,j)$, with $a\in p[i]$ and $b\in q[j]$.

Then to fill in the remaining empty box, we need a direction of $p\tri p'$ at $(i,\ol{i'})$, which can be given by the $p[i]$-direction $a$ followed by a $p'[\ol{i'}(a)]$-direction, namely $a'$.
We also need a direction of $q\tri q'$, which can be obtained analogously:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$(p\tri p')\otimes(q\tri q')$" left] (p) {$(a,a'),(b,b')$\at$(i,\ol{i'}),(j,\ol{j'})$};
\node[poly, cod, "$p\otimes q$" right, right=2.5 of p.south, yshift=-1ex] (q) {$a,b$\at$i,j$};
\node[poly, cod, "$p'\otimes q'$" right, above=of q] (r) {$a',b'$\at$\ol{i'}(a),\ol{j'}(b)$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\]

§.§ Interaction with vertical and cartesian lenses

We conclude this section by examining how $\tri$ interacts with vertical and cartesian lenses, as defined in <ref>.

If $\varphi\colon p\to p'$ and $\psi\colon q\to q'$ are cartesian lenses, then so is $\varphi\tri \psi\colon p\tri q \to p'\tri q'$.

We use the third characterization of cartesian lenses given in <ref>, as lenses whose naturality squares are pullbacks.
For any sets $A,B$ and function $h\colon A\to B$, consider the diagram

\[
\begin{tikzcd}[column sep=small]
p\tri q\tri A\ar[r]\ar[d] & p'\tri q\tri A\ar[r]\ar[d] & p'\tri q'\tri A\ar[d] \\
p\tri q\tri B\ar[r] & p'\tri q\tri B\ar[r] & p'\tri q'\tri B.
\end{tikzcd}
\]

The square on the left is a pullback because $\varphi\colon p\to p'$ is cartesian.
Meanwhile, the square on the right is a pullback because $\psi\colon q\to q'$ is cartesian and $\tri$ preserves pullbacks by <ref>.
Hence the outer rectangle is a pullback as well, implying that $\varphi\tri \psi\colon p\tri q \to p'\tri q'$ is cartesian.

Let $\varphi\colon p\to p'$ and $\psi\colon q\to q'$ be lenses.

* Show that if $\varphi$ is an isomorphism and $\psi$ is vertical, then $\varphi\tri \psi$ is vertical.

* Find a vertical lens $\varphi$ and a polynomial $q$ for which $\varphi\tri q\colon p\tri q\to p'\tri q$ is not vertical.

Here $\varphi\colon p\to p'$ and $\psi\colon q\to q'$ are lenses.

* If $\varphi$ is an isomorphism and $\psi$ is vertical, then $\psi\tri\1\colon q\tri\1\to q'\tri\1$ is an isomorphism, so $\varphi\tri \psi\tri\1\colon p\tri q\tri\1\to p'\tri q'\tri\1$ is an isomorphism as well.
Thus $\varphi\tri \psi$ is vertical.

* If $\varphi$ is the unique lens $\yon\to\1$ and $q=\0$, then $\varphi$ is vertical, but since $\yon\tri\0\iso\0$ and $\1\tri\0\iso\1$, the lens $\varphi\tri\0\colon\0\to\1$ is not.

§ SUMMARY AND FURTHER READING

In this chapter we introduced the composition (sometimes called “substitution”) product $\tri$. Given polynomials $p,q$ thought of as functors, their composite is again polynomial and is given by $p\tri q$. We explained how it looks in terms of algebra, e.g. how to compute $\yon^\2\tri(\yon+\1)$; in terms of sets, e.g. as a sum-product-sum-product $\sum\prod\sum\prod$, which can be reduced to a single $\sum\prod$; in terms of trees, by stacking corollas on top of corollas; and in terms of polyboxes. We paid particular attention to lenses into a composite $p\to q\tri r$.

This allowed us to explain how to think of dynamical systems $S\yon^S\to p\tri q$ with composite interfaces as multi-step machines: each state produces a $p$-output, and then for every $p$-input produces a $q$-output, and then for every $q$-input returns an updated $S$-state.

Finally, we discussed some facts of the composition product. For example, we showed that $-\tri q$ has a left adjoint $\lchom{q}{-}$ and that $q\tri -$ has a left multi-adjoint $-\frown q$. We also explained that $p\tri q$ preserves all with limits in the variable $p$ and all connected limits in the variable $q$. We also explained the duoidal interaction between $\otimes$ and $\tri$, i.e. the natural lens $\tri\otimes\tri\to\otimes\tri\otimes$, and how $\tri$ interacts with cartesian lenses.

Polynomial composition is one of the best known aspects of polynomial functors. Again, see <cit.> for more on this. We learned of the left coclosure (see <ref>) from Josh Meyers, though it may have already been known in the containers community.

§ EXERCISE SOLUTIONS

CHAPTER: POLYNOMIAL COMONOIDS AND COFUNCTORS

Imagine a realm where there are various positions you can be in. From every position, there are a number of moves you can make, possibly infinitely many. But whatever move you make, you'll end up in a new position. Well, technically it counts as a move to simply stay where you are, so you might end up in the same position. But wherever you move to, you can move again, and any number of moves from the original position counts as a single move. What sort of realm is this?

The most surprising aspects of $\poly$ really begin with its comonoids.
In 2018, researchers Daniel Ahman and Tarmo Uustalu presented a characterization of comonoids in $(\poly,\yon,\tri)$ as a surprisingly familiar construct.
For us, this story will emerge naturally as we continue to expand our understanding of the humble state system of a dependent dynamical system.
Let's go through it.

§ STATE SYSTEMS, CATEGORICALLY

Since defining dependent dynamical systems in <ref>, we have evolved our understanding of their state systems over the course of the last few chapters.
Let's take this moment to review what we know about these state systems so far.

Our original definition of a state system was as a monomial $S\yon^S$ for some set $S$.
But in <ref>, we noted that this formulation requires us to discuss the positions and directions of a state system at the level of sets rather than in the language of $\poly$.
Instead, let's take an arbitrary polynomial $\car{s}\in\poly$ and attempt to characterize what it means for $\car{s}$ to be a state system using only the categorical machinery of $\poly$.
We will continue to refer to the positions of $\car{s}$ as states, but we will shift from thinking of the directions of $\car{s}$ as states to thinking of them as transitions from one state to another.

§.§ The do-nothing section

In <ref>, we saw that every state system $\car{s}$ is equipped with a do-nothing section: a lens $\epsilon\colon\car{s}\to\yon$ that picks out a direction at each state that we would like to interpret as “doing nothing” and remaining at that state.

We drew $\epsilon$ in polyboxes in <ref>, but that was when we let ourselves assume that the position-set of a state system was equal to each of its direction-sets.
Now all we know is that for each state $s\in\car{s}(\1)$, the do-nothing section chooses an $\car{s}[s]$-direction to signify staying at the same state; it doesn't make sense to say that this direction is literally equal to $s$.
So we need a different name for the $\car{s}[s]$-direction that $\epsilon$ identifies: call it $\id_s$, because it behaves like a sort of identity operation on the state $s$.

So the revised polyboxes for the do-nothing section $\epsilon\colon\car{s}\to\yon$ are as follows:

\begin{equation} \label{eqn.do_nothing_polybox}
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (S) {$\id_s$\at$s$};

\draw (S_pos) to[climb'] node[right] {$\epsilon$} (S_dir);
\end{tikzpicture}
\end{equation}

Say I have a polynomial $\car{s}\in\poly$, and I tell you that there is a lens $\epsilon\colon\car{s}\to\yon$.
What can you say about the polynomial $\car{s}$?

Given a polynomial $\car{s}\in\poly$ equipped with a lens $\epsilon\colon\car{s}\to\yon$, we know that $\epsilon$ picks out a direction at every position of $\car{s}$.
So all we can say about $\car{s}$ is that there is at least one direction at each of its positions.
Equivalently, we could say that $\car{s}$ can be written as the product of $\yon$ and some other polynomial.

[The do-nothing section in tree pictures]
We have seen the do-nothing section drawn in polyboxes, but let's see what it looks like in our tree pictures.
We'll take $\car{s}\coloneqq\{\bul[red],\bul[dgreen],\bul[blue]\}\yon^{\{\bul[red],\bul[dgreen],\bul[blue]\}}$, drawn as follows:

\[
\begin{tikzpicture}[rounded corners]
\node (p1) [draw, "$\car{s}\coloneqq$" left] {
\begin{tikzpicture}[trees, sibling distance=4mm]
\foreach \i/\c in {1/red, 2/dgreen, 3/blue}
\node[\c] at (1.8*\i,0) {$\bullet$}
child [red]
child [dgreen]
child [blue]
\end{tikzpicture}
\end{tikzpicture}
\]

Then the do-nothing section $\epsilon\colon\car{s}\to\yon$ can be drawn like any one of the following three possibilities:

\[
\begin{tikzpicture}[trees, bend right]
\foreach \i/\c in {1/red, 2/dgreen, 3/blue}
\node[\c] (\i) at (3*\i, 0) {$\bullet$}
child [red] {coordinate (\i1)}
child [dgreen] {coordinate (\i2)}
child [blue] {coordinate (\i3)}
\node[right=of \i] (y\i) {$\bullet$}
child{coordinate (y\i')}
\draw[|->, shorten <= 3pt, shorten >= 3pt] (\i) -- (y\i);
\draw[densely dotted, postaction={decorate}] (y\i') to (\i\i);
\end{tikzpicture}
\]

It picks out one direction at each position, namely the one of the same color.

There is not much else we can say about the do-nothing section on its own, so let us revisit the other lens that every state system is equipped with before considering the relationship between the two.

§.§ The transition lens

We saw in <ref> that $\car{s}$ also comes equipped with a transition lens: a lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$, which we can draw as

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {$a_2'$\at$s_0$};
\node[poly, cod, right=1.8 of r.south, yshift=-2.5ex, "$\car{s}$" below] (p) {$a_1$\at$s_0$};
\node[poly, cod, above=.8 of p, "$\car{s}$" above] (p') {$a_2$\at$s_1$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.3] {run} (r_dir);
\end{tikzpicture}
\]

The arrow labeled tgt is the target function: given a state $s_0$ and a direction $a_1$ at that state, $\text{tgt}(s_0,a_1)$ tells us the new state $s_1$ that following $a_1$ from $s_0$ will lead to.
We know that when $s_0$ is fixed, the target function on the second component $a_1$ should be an isomorphism $\car{s}[s_0]\to\car{s}(\1)$; that is, there is exactly one direction at $s_0$ that leads to each state of $\car{s}$.
But this property is a little tricky to state in the language of $\poly$; in fact, we won't attempt to do so just yet.
Instead, we'll use it to make a notational choice: given $s,t\in\car{s}$, we will let $s\to t$ denote the unique direction at $s$ that leads to $t$, so that $\text{tgt}(s,s\to t)=t$.
So we can redraw our transition lens as

\begin{equation} \label{eqn.trans_lens_polybox}
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {$s_0\to s_2$\at$s_0$};
\node[poly, cod, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" right] (p) {$s_0\to s_1$\at$s_0$};
\node[poly, cod, above=.8 of p, "$\car{s}$" right] (p') {$s_1\to s_2$\at$s_1$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.4] {run} (r_dir);
\end{tikzpicture}
\end{equation}

In addition to the fact that $\text{tgt}(s_0,s_0\to s_1)=s_1$ as intended, this picture tells us two more properties of $\delta$.

The first is that the bottom arrow is the identity on $\car{s}(\1)$.
This is something we would like to be able to express categorically in the language of $\poly$.
We'll see that this property falls out naturally when we express how the transition lens plays nicely with the do-nothing section in <ref>.

The second is that the run arrow, which runs the transition $s_0\to s_1$ and the transition $s_1\to s_2$ together into a transition starting at $s_0$, should have the same target as tfhe second transition it follows: in this case, $s_2$.
Equationally, writing the left and right hand sides only in terms of the contents of the blue boxes, we have that

\begin{equation} \label{eqn.state_run_tgt}
\text{tgt}(s_0,\text{run}(s_0,s_0\to s_1,s_1\to s_2))=s_2=\text{tgt}(\text{tgt}(s_0,s_0\to s_1),s_1\to s_2).
\end{equation}

We'll see that this property arises naturally when we we generalize the transition lens to more than two steps in <ref>.

[The transition lens in tree pictures]
Continuing from <ref>, we draw the transition lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$ of $\car{s}\coloneqq\3\yon^\3\iso\{\bul[red],\bul[dgreen],\bul[blue]\}\yon^{\{\bul[red],\bul[dgreen],\bul[blue]\}}$ (where directions are labeled with their targets) in tree pictures as well, recalling that the trees of $\car{s}\tri\car{s}$ are obtained by taking an $\car{s}$-corolla and gluing more $\car{s}$-corollas to each of its leaves:

\[
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=5mm},
level 2/.style={sibling distance=1.5mm},
bend right=60]
\foreach \i/\c in {1/red, 2/dgreen, 3/blue}
\node[\c] (\i) at (4*\i, 0) {$\bullet$}
child [red] {coordinate (\i1)}
child [dgreen] {coordinate (\i2)}
child [blue] {coordinate (\i3)}
\node[right=1.7 of \i, \c] (SS\i) {$\bullet$}
child [red] {node (S\i1) {$\bullet$}
child [red] {coordinate (\i11)}
child [dgreen] {coordinate (\i12)}
child [blue] {coordinate (\i13)}
child [dgreen] {node (S\i2) {$\bullet$}
child [red] {coordinate (\i21)}
child [dgreen] {coordinate (\i22)}
child [blue] {coordinate (\i23)}
child [blue] {node (S\i3) {$\bullet$}
child [red] {coordinate (\i31)}
child [dgreen] {coordinate (\i32)}
child [blue] {coordinate (\i33)}
\draw[|->, shorten <= 3pt, shorten >= 3pt] (\i) -- (SS\i);
\foreach \j in {1,2,3}
\foreach \k\d in {1/red, 2/dgreen, 3/blue}
\draw[densely dotted, postaction={decorate}, \d] (\i\j\k) to (\i\k);
\end{tikzpicture}
\]

On positions, the target function of $\delta$ tells us which root of $\car{s}$ to glue to each leaf of $\car{s}$.
Then on directions, the run function of $\delta$ tells us how to collapse the height-$2$ leaves of the trees we obtain in $\car{s}\tri\car{s}$ down to the original height-$1$ leaves of the corollas of $\car{s}$.

We can draw what the target function is doing more compactly by taking the corollas of $\car{s}$ and “bending the arrows” so that they point to their targets, like so:

\[
\begin{tikzpicture}
\node[circle,minimum size=2cm] (b) {};
\foreach\x/\c in {1/red, 2/dgreen, 3/blue} {
\node[minimum size=0.1cm,draw,circle,\c,fill=\c] (3-\x) at (b.{360/3*\x}){};
\foreach\x/\c in {1/red, 2/dgreen, 3/blue} {
\foreach\y/\d in {1/red, 2/dgreen, 3/blue}{
\ifnum\x=\y
\draw[\d,->] (3-\x) to [in=360/3*\x-15,out=360/3*\x+15,loop] ();
\relax
\else
\draw[\d] (3-\x) edge[->,bend right=10] (3-\y);
\fi
\end{tikzpicture}
\]

So the target function of $\delta$ turns our corolla picture of $\car{s}$ into a complete graph on its roots!
Then the run function takes any two arrows that form a path in the graph and collapses them down to a single arrow that starts (and, according to (<ref>), ends) at the same vertex as the two-arrow path.

If this all sounds suspiciously familiar to you, you're on the right track—hang tight.

§.§ The do-nothing section coheres with the transition lens

For each state $s\in\car{s}(\1)$, the do-nothing section $\epsilon\colon\car{s}\to\yon$ picks out the $\car{s}[s]$-direction $\id_s$ that “does nothing” and keeps the system in the same state $s$.
But it is the transition lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$ that actually sets our state system in motion, specifying the target of each direction and how two directions run together.
Either of these directions could be our do-nothing direction $\id_s$, so let's try to figure out what should happen when we set each one in turn to $\id_s$.

We can draw in polyboxes what happens when we set $\id_s$, as specified by $\epsilon$, to be the first direction that $\delta$ runs together like this:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {\at$s$};
\node[poly, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" below] (p) {$\id_s$\at$s$};
\node[poly, cod, above=.8 of p, xshift=2.5ex, "$\car{s}$" above] (p') {tgt$(s,\id_s)\to t$\at tgt$(s,\id_s)$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_pos) to[climb'] node[right] {$\epsilon$} (p_dir);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.4] {run} (r_dir);
\end{tikzpicture}
\]

Reading this picture from left to right, we see that it depicts the polyboxes of the composite lens $\delta\then(\epsilon\tri\car{s})\colon\car{s}\to\yon\tri\car{s}\iso\car{s}$ (recall that we sometimes denote the identity lens on $\car{s}$ also by $\car{s}$).
To make this interpretation more transparent, we could be a little more verbose with our polybox picture if we wanted to (omitting the contents of the boxes for clarity):

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (r) {};
\node[poly, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" below] (p) {};
\node[poly, cod, above=.8 of p, "$\car{s}$" above] (p') {};

\draw[double, -] (r_pos) to[first]  (p_pos.west);
\draw (p_pos) to[climb'] node[right] {$\epsilon$} (p_dir);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.3] {run} (r_dir);
\end{tikzpicture}
\node[right=1 of 1] (2) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (yX) {};
\node[poly, right=2 of yX.south, yshift=-2.5ex, "$\car{s}$" below] (p) {};
\node[poly, above=.8 of p, "$\car{s}$" above] (p') {};
\node[poly, cod, identity, right=of p, "$\car{s}$" below] (q) {};
\node[poly, cod, above=.8 of q, "$\car{s}$" above] (q') {};
\draw (p_pos) -- node[below] {$\epsilon_\1$} (q_pos);
\draw (q_dir) -- node[above] {$\epsilon^\sharp$} (p_dir);
\draw[double, -] (p'_pos) -- (q'_pos);
\draw[double, -] (q'_dir) -- (p'_dir);
\draw[double, -] (yX_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.3] {run} (yX_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

Now what should $\text{tgt}(\id_s)$ be, and what should go in the direction box on the left?

If following the direction $\id_s$ from the state $s$ is really the same as doing nothing, then its target state should be the same state $s$ that it emerged from.
Moreover, running together $\id_s$ with any other direction $s\to t$ from $s$ should be no different from the direction $s\to t$ on its own.

\[
\text{tgt}(s,\id_s)=s \qqand \text{run}(s,\id_s,s\to t)=s\to t.
\]

In fact, $\id_s$ should really just be the direction $s\to s$.
Pictorially, we have the equation

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {\at$s$};
\node[poly, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" below] (p) {$\id_s$\at$s$};
\node[poly, cod, above=.8 of p, xshift=2.5ex, "$\car{s}$" above] (p') {tgt$(s,\id_s)\to t$\at tgt$(s,\id_s)$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_pos) to[climb'] node[right] {$\epsilon$} (p_dir);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);
\draw (p'_dir) to[last] node[above=.4] {run} (r_dir);
\end{tikzpicture}
\node[right=1.8 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (c) {$s\to t$\at$s$};
\node[poly, cod, right=of c, "$\car{s}$" right] (c') {$s\to t$\at$s$};
\draw[double, -] (c_pos) -- (c'_pos);
\draw[double, -] (c'_dir) -- (c_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

Or, if you prefer, we might say that $\delta\then(\epsilon\tri\car{s})=\id_{\car{s}}$, or that the following diagram commutes:

\[
\begin{tikzcd}[row sep=large]
\yon\tri\car{s} & \car{s}\ar[d, "\delta"]\ar[l, equal] \\
& \car{s}\tri\car{s}\ar[ul, "\epsilon\:\tri\:\car{s}"]
\end{tikzcd}
\]

This commutative diagram captures one way in which $\epsilon$ and $\delta$ always relate—and it's written entirely in the language of $\poly$, without having to talk about individual sets!

What about setting the second direction that $\delta$ runs together to what is specified by $\epsilon$, rather than the first?
To answer this, we should look at the composite lens $\delta\then(\car{s}\tri\epsilon)\colon\car{s}\to\car{s}\tri\yon\iso\car{s}$ instead.
But the do-nothing direction should still do nothing, so here's what the polybox picture should look like:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {$s\to t$\at$s$};
\node[poly, cod, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" below] (p) {$s\to t$\at$s$};
\node[poly, above=.8 of p, "$\car{s}$" above] (p') {$\id_t$\at $t$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {tgt} (p'_pos);	\draw (p'_pos) to[climb'] node[right] {$\epsilon$} (p'_dir);
\draw (p'_dir) to[last] node[above=.4] {run} (r_dir);
\end{tikzpicture}
\node[right=1.8 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (c) {$s\to t$\at$s$};
\node[poly, cod, right=of c, "$\car{s}$" right] (c') {$s\to t$\at$s$};
\draw[double, -] (c_pos) -- (c'_pos);
\draw[double, -] (c'_dir) -- (c_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

The lens depicted on the right hand side of the equation is again the identity lens on $\car{s}$.

If we match up the two white boxes on the right hand side of the equation with the corresponding white boxes on the left, we can actually read two equations off of this polybox picture.
Matching up positions in the codomain tells us that the bottom arrow of $\delta$ on the left must send $s$ to itself: it is the identity function on $\car{s}(\1)$.
Indeed, this is exactly what we wanted to say about that arrow in <ref>.

Meanwhile, matching up directions in the domain tells us that

\[
\text{run}(s,s\to t,\id_t)=s\to t,
\]

as we would expect: $\id_t$ is just be the direction $t\to t$.

More concisely, we can express both these facts in $\poly$ via the equation $\delta\then(\car{s}\tri\epsilon)=\id_{\car{s}}$.
The corresponding commutative diagram is as follows:

\[
\begin{tikzcd}[row sep=large]
\car{s}\ar[d, "\delta"']\ar[r, equal] & \car{s}\tri\yon \\
\car{s}\tri\car{s}.\ar[ur, "\car{s}\:\tri\:\epsilon"']
\end{tikzcd}
\]

We can combine this with our previous commutative diagram to say that the relationship between the do-nothing section $\epsilon\colon\car{s}\to\yon$ and the transition lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$ of a state system $\car{s}$ is captured in $\poly$ by the following commutative diagram:

\begin{equation}\label{eqn.erasure_law_state}
\begin{tikzcd}[row sep=large]
\yon\tri\car{s}&\car{s}\ar[d, "\delta" description]\ar[r, equal]\ar[l, equal]&\car{s}\tri\yon\\&
\car{s}\tri\car{s}.\ar[ul, "\epsilon\:\tri\:\car{s}"]\ar[ur, "\car{s}\:\tri\:\epsilon"']
\end{tikzcd}
\end{equation}

§.§ The transition lens is coassociative

Toward the end of <ref>, we noted that while the transition lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$ gives us a canonical way to model two steps of a dynamical system with state system $\car{s}$, we have a choice of how to model three steps through the same system: we could obtain a lens $\car{s}\to\car{s}\tripow3$ that runs three directions together by taking either one of the composite lenses $\delta\then(\delta\tri\car{s})$ or $\delta\then(\car{s}\tri\delta)$.
That presents a problem for us: which one should we choose?

Happily, it turns out this choice is a false one.
If we write out the two composite lenses in polyboxes, with $\delta\then(\delta\tri\car{s})$ on the left and $\delta\then(\car{s}\tri\delta)$ on the right, we find that they are equal:

\begin{equation}\label{eqn.trans_lens_coassoc_polybox}
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, mapstos, font=\tiny]
\node[poly, dom, "$\car{s}$" left] (m') {$s_0\to s_3$\at$s_0$};
\node[poly, right= of m'.south, yshift=-1ex, "$\car{s}$" below] (mm') {$s_0\to s_2$\at$s_0$};
\node[poly, above=of mm', "$\car{s}$" above] (C') {$s_2\to s_3$\at$s_2$};
\node[poly, cod, right= of mm'.south, yshift=-1ex, "$\car{s}$" right] (D') {$s_0\to s_1$\at$s_0$};
\node[poly, cod, above=of D', "$\car{s}$" right] (mmm') {$s_1\to s_2$\at$s_1$};
\node[poly, cod, above=of mmm', "$\car{s}$" right] (CC') {$s_2\to s_3$\at$s_2$};
\draw[double, -] (m'_pos) to[first] (mm'_pos);
\draw (mm'_dir) to[climb] node[right] {tgt} (C'_pos);
\draw (C'_dir) to[last] node[above, sloped] {run} (m'_dir);
\draw[double, -] (mm'_pos) to[first] (D'_pos);
\draw (D'_dir) to[climb] node[right] {tgt} (mmm'_pos);
\draw (mmm'_dir) to[last] node[above, sloped] {run} (mm'_dir);
\draw[double, -] (C'_pos) to[first] (CC'_pos);
\draw[double, -] (CC'_dir) to[last] (C'_dir);
\end{tikzpicture}
\node (p2) [right=of p1] {
\begin{tikzpicture}[polybox, mapstos, font=\tiny]
\node[poly, dom, "$\car{s}$" left] (m) {$s_0\to s_3$\at$s_0$};
\node[poly, right= of m.south, yshift=-1ex, "$\car{s}$" below] (D) {$s_0\to s_1$\at$s_0$};
\node[poly, above=of D, "$\car{s}$" above] (mm) {$s_1\to s_3$\at$s_1$};
\node[poly, cod, right= of D.south, yshift=-1ex, "$\car{s}$" right] (DD) {$s_0\to s_1$\at$s_0$};
\node[poly, cod, above=of DD, "$\car{s}$" right] (mmm) {$s_1\to s_2$\at$s_1$};
\node[poly, cod, above=of mmm, "$\car{s}$" right] (C) {$s_2\to s_3$\at$s_2$};
\draw[double, -] (m_pos) to[first] (D_pos);
\draw (D_dir) to[climb] node[right] {tgt} (mm_pos);
\draw (mm_dir) to[last] node[above, sloped] {run} (m_dir);
\draw[double, -] (D_pos) to[first] (DD_pos);
\draw[double, -] (DD_dir) to[last] (D_dir);
\draw[double, -] (mm_pos) to[first] (mmm_pos);
\draw (mmm_dir) to[climb] node[right] {tgt} (C_pos);
\draw (C_dir) to[last] node[above, sloped] {run} (mm_dir);
\end{tikzpicture}
\node at ($(p1.south)!.5!(p2.north)$) {$=$};
\end{tikzpicture}
\end{equation}

Remember: the way to read these polyboxes is to start at the lower blue square on the left and follow the path counter clockwise around the diagram; and if you reach a box with no arrows leading out of it, go up to the blue box above it and continue to follow the arrows from there.

There's a lot going on here, so let's break it down—we'll focus on the run functions first.
On the left hand side, we run together $s_0\to s_1$ and $s_1\to s_2$ to obtain $s_0\to s_2$, before running that together with $s_2\to s_3$ to obtain $s_0\to s_3$, as we see in the upper left box.
Meanwhile, on the right, we run together $s_1\to s_2$ and $s_2\to s_3$ to obtain $s_1\to s_3$, before running $s_0\to s_1$ together with our newly obtained $s_1\to s_3$ to again obtain $s_0\to s_3$ in the upper left box.
We could write this all out equationally, but all this is saying is that “running together” the directions of a state system is an associative operation.
When running together three directions, it doesn't matter whether we run the first two together or the last two together to start.
Not only is this guaranteed by the way in which we constructed $\delta$, it also makes intuitive sense.

Using only the contents of the blue boxes and the target and run functions, write down the equation that we can read off of (<ref>) expressing the associativity of the “running together” operation.

Following the arrows on either side of (<ref>) all the way to the domain's direction box, we obtain an expression for each box's contents that we can then set equal to each other.
The easiest way to actually write down these expressions is probably to start at the end with $s_0\to s_3$ and follow the arrows backward, unpacking each term until only the contents of the blue boxes remain (namely $s_0, s_0\to s_1, s_1\to s_2,$ and $s_2\to s_3$).
Here's what we get when we follow this process for the left hand side of (<ref>) (remember where to look for the three inputs to the run function):

\begin{align*}
s_0\to s_3&=\text{run}(s_0,s_0\to s_2,s_2\to s_3)\\
&=\text{run}(s_0,\text{run}(s_0,s_0\to s_1,s_1\to s_2),s_2\to s_3)\\
&=\text{run}(s_0,\text{run}(s_0,s_0\to s_1,s_1\to s_2),s_2\to s_3);
\end{align*}

and here's what we get for the right (also remember where to look for the two inputs to the target function):

\begin{align*}
s_0\to s_3&=\text{run}(s_0,s_0\to s_1,s_1\to s_3)\\
&=\text{run}(s_0,s_0\to s_1,\text{run}(s_1,s_1\to s_2,s_2\to s_3))\\
&=\text{run}(s_0,s_0\to s_1,\text{run}(\text{tgt}(s_0,s_0\to s_1),s_1\to s_2,s_2\to s_3)).
\end{align*}

Setting these equal yields our desired associativity equation:

\[
\text{run}(s_0,\text{run}(s_0,s_0\to s_1,s_1\to s_2),s_2\to s_3)=\text{run}(s_0,s_0\to s_1,\text{run}(\text{tgt}(s_0,s_0\to s_1),s_1\to s_2,s_2\to s_3)).
\]

This associative property is what we get by matching up the white direction boxes on each domain side, but there are three more white position boxes on each codomain side that we can match up as well.
The fact that the lower two of these pairs coincide is a consequence of the fact that the bottom arrow of $\delta$ is the identity, which we already knew from <ref>; so we don't learn anything new there.
On the other hand, the fact that both the upper position boxes in the codomain contain $s_2$ implies that

\begin{align*}
\text{tgt}(s_0,\text{run}(s_0,s_0\to s_1,s_1\to s_2))&=\text{tgt}(s_0,s_0\to s_2)\\
&=\text{tgt}(s_1,s_1\to s_2)\\
&=\text{tgt}(\text{tgt}(s_0,s_0\to s_1),s_1\to s_2),
\end{align*}

which is exactly what we wanted in (<ref>).
In English, this says that when we run together $s_0\to s_1$ and $s_1\to s_2$, the new direction's target is the same as the direction of $s_1\to s_2$, the latter of the two directions that we ran together.
Again, this coincides with our intuition: if we follow two directions in order, we should end up at wherever the latter direction leads us.

Hence both the associativity of running directions together and the relationship between the target and run functions from (<ref>) are captured by the equality of lenses $\delta\then(\delta\tri\car{s})=\delta\then(\car{s}\tri\delta)$.
Equivalently, the following diagram in $\poly$ commutes:

\begin{equation}\label{eqn.coassoc_law_states}
\begin{tikzcd}[row sep=large]
\car{s}\ar[r, "\delta"]\ar[d, "\delta"']&
\car{s}\tri\car{s}\ar[d, "\car{s}\:\tri\:\delta"]\\
\car{s}\tri\car{s}\ar[r, "\delta\:\tri\:\car{s}"']&
\car{s}\tri\car{s}\tri\car{s}.
\end{tikzcd}
\end{equation}

Another way to say this is that $\delta$ is coassociative: while $\delta$ is only a lens $\car{s}\to\car{s}\tripow2$ as defined, the commutativity of (<ref>) tells us that the two ways of getting a lens $\car{s}\to\car{s}\tripow3$ out of $\delta$ are actually the same.
(This is dual to an associative operation, which is a binary operation that gives rise to two identical ternary operations.)

So $\delta$ induces a canonical lens $\car{s}\to\car{s}\tripow3$, which we will call $\delta^{(3)}$, as it has $3$ copies of $\car{s}$ in its codomain.
Armed with this new lens, we can model three steps through a system $\varphi\colon\car{s}\to p$ with interface $p\in\poly$ as the composite lens

\[
\car{s}\To{\delta^{(3)}}\car{s}\tripow3\To{\varphi\tripow3}p\tripow3.
\]

In fact, coassociativity guarantees that $\delta$ induces a canonical lens $\delta^{(n)}\colon\car{s}\to\car{s}\tripow{n}$ for every integer $n\geq2$, starting with $\delta^{(2)}\coloneqq\delta$.
[Perhaps this notation seems a little unnatural, but it helps to think of the original $\delta\colon\car{s}\to\car{s}\tri\car{s}$ as the $n=2$ case of a generalized transition lens modeling $n$ steps through the state system.]
For concreteness, we could then define $\delta^{(n)}$ for $n>2$ inductively by $\delta^{(n)}\coloneqq\delta\then(\delta^{(n-1)}\tri\car{s})$, or just as well by $\delta^{(n)}\coloneqq\delta\then(\car{s}\tri\delta^{(n-1)})$ or even $\delta^{(n)}\coloneqq\delta\then(\delta^{(\ell)}\tri\delta^{(m)})$ for some pair of integers $\ell,m>1$ satisfying $\ell+m=n$.
Regardless, the coassociativity of $\delta$ means that it doesn't matter how we build a lens $\car{s}\to\car{s}\tripow{(n+1)}$ out of $\delta,\then,\tri,$ and identity lenses: we'll always end up with the same lens.
We will state this in more generality in <ref>, but here's some practice with the $n=4$ case for a taste of what's to come.

* Say we know nothing about $\car{s}$ or $\delta$ apart from the fact that $\car{s}\in\poly$ and that $\delta$ is a lens $\car{s}\to\car{s}\tri\car{s}$.
List all the ways to obtain a lens $\car{s}\to\car{s}\tripow4$ using only copies of $\delta,\id_\car{s}$, $\tri$, and $\then$.
(You may write $\car{s}$ for $\id_\car{s}$.)

* Now assume that (<ref>) commutes.
Show that all the lenses on your list are equal.
(Hint: Use the fact that $(f\then g)\tri(h\then k)=(f\tri h)\then(g\tri k)$ for lenses $f,g,h,k$).

* Given $\car{s}\in\poly$ and a lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$, we want all the ways to obtain a lens $\car{s}\to\car{s}\tripow4$ using $\delta,\id_\car{s}$ (i.e. $\car{s}$), $\tri,$ and $\then$.
Starting with $\car{s}$, the only way to get to $\car{s}\tripow2$ is with a single $\delta\colon\car{s}\to\car{s}\tripow2$.
From there, we can get to $\car{s}\tripow4$ directly by composing with $\delta\tri\delta$ to obtain $\delta\then(\delta\tri\delta)$.
Alternatively, we can preserve either the first or the second $\car{s}$ using the identity, then get to $\car{s}\tripow3$ from the other $\car{s}$ in one of two ways: either $\delta\then(\delta\tri\car{s})$ or $\delta\then(\car{s}\tri\delta)$.
This gives us $4$ more ways to write a lens $\car{s}\to\car{s}\tripow4$: either $\delta\then(\car{s}\tri(\delta\then(\delta\tri\car{s})))$ or $\delta\then(\car{s}\tri(\delta\then(\car{s}\tri\delta)))$ if we chose to preserve the first $\car{s}$, and either $\delta\then((\delta\then(\delta\tri\car{s}))\tri\car{s})$ or $\delta\then((\delta\then(\car{s}\tri\delta))\tri\car{s})$ if we chose to preserve the second.
Here's the full list, sorted roughly by how far to the left we try to apply each $\delta$:

* $\delta\then((\delta\then(\delta\tri\car{s}))\tri\car{s})$

* $\delta\then((\delta\then(\car{s}\tri\delta))\tri\car{s})$

* $\delta\then(\delta\tri\delta)$

* $\delta\then(\car{s}\tri(\delta\then(\delta\tri\car{s})))$

* $\delta\then(\car{s}\tri(\delta\then(\car{s}\tri\delta)))$

This coincides with the $5$ different ways to parenthesize a $4$-term expression.

* We wish to show that if (<ref>) commutes, then all the lenses on our list are equal.
The commutativity of (<ref>) implies that $\delta\then(\delta\tri\car{s})=\delta\then(\car{s}\tri\delta)$; so (1) and (2) from our list are equal, as are (4) and (5).
Meanwhile, since $\car{s}=\car{s}\then\car{s}$, we can rewrite (1) as

\[
\delta\then((\delta\then(\delta\tri\car{s}))\tri(\car{s}\then\car{s}))=\delta\then(\delta\tri\car{s})\then(\delta\tri\car{s}\tri\car{s}),
\]

where the associativity of $\tri$ and $\then$ allows us to drop some parentheses.
Then the commutativity of (<ref>) allows us to further rewrite this as

\begin{align*}
\delta\then(\car{s}\tri\delta)\then(\delta\tri\car{s}\tri\car{s})&=\delta\then((\car{s}\then\delta)\tri(\delta\then(\car{s}\tri\car{s})))\\
\end{align*}

so (1) and (3) are equal.
Similarly, we can rewrite (5) as

\begin{align*}
\delta\then((\car{s}\then\car{s})\tri(\delta\then(\car{s}\tri\delta)))&=\delta\then(\car{s}\tri\delta)\then(\car{s}\tri\car{s}\tri\delta)\\
\end{align*}

so (3) and (5) are equal.
Hence all the lenses on our list are equal.

§.§ Running dynamical systems

Finally, we are ready to fulfill our promise from way back in <ref> by using the language of $\poly$ to describe stepping through a dynamical system $n$ times for arbitrary $n\in\nn$.
Given a dynamical system $\varphi\colon\car{s}\to p$ with interface $p\in\poly$, we can construct a new dynamical system that we call $\text{Run}_n(\varphi)$, with the same state system $\car{s}$ but a new interface $p\tripow{n}$, by defining $\text{Run}_n(\varphi)\coloneqq\delta^{(n)}\then\varphi\tripow{n}$.
Visually, we define $\text{Run}_n(\varphi)$ so that the following diagram commutes:

\begin{equation*}%\label{eqn.run}
\begin{tikzcd}
\car{s}\ar[r, "\delta^{(n)}"]\ar[rr, bend right, "{\text{Run}_n(\varphi)}"']&
\car{s}\tripow{n}\ar[r, "\varphi\tripow{n}"]&
p\tripow n
\end{tikzcd}
\end{equation*}

One way to think of this is that $\text{Run}_n(\varphi)$ is a sped-up version of $\varphi$: one step through $\text{Run}_n(\varphi)$ is equivalent to $n$ steps through $\varphi$.
But this is just because a single interaction with the interface $p\tripow{n}$ models a sequence of $n$ interactions with the interface $p$, as detailed in <ref>.
So $\text{Run}_n(\varphi)$ repackages $n$ cycles through $\varphi$ into a single step.
Crucially, $\delta^{(n)}$ is what tells us how to sequence all $n$ of these steps together on the state system side.
We illustrated how $\delta$ does this for the $n=2$ case in <ref>, and here's a polybox picture for the $n=3$ case:

\[
\begin{tikzpicture}
\node (given) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, blue, "$\car{s}$" left] (S) {};
\node[poly, cod, dgreen, right=of S, "$p$" right] (p) {};
\draw (S_pos) to[first] (p_pos);
\draw (p_dir) to[last]  (S_dir);
\node at ($(S.east)!.5!(p.west)$) {$\varphi$};
\end{tikzpicture}
\node[right=of given] (obtain) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, blue, "$\car{s}$" left] (S) {};
\node[poly, blue, right=of S] (S2) {};
\node[poly, blue, below=of S2] (S1) {};
\node[poly, blue, above=of S2] (S3) {};
\node[poly, dgreen, cod, right=of S1, "$p$" right] (p1) {};
\node[poly, dgreen, cod, right=of S2, "$p$" right] (p2) {};
\node[poly, dgreen, cod, right=of S3, "$p$" right] (p3) {};
\draw (S1_pos) to[first] (p1_pos);
\draw (p1_dir) to[last] (S1_dir);
\draw (S2_pos) to[first] (p2_pos);
\draw (p2_dir) to[last]  (S2_dir);
\draw (S3_pos) to[first] (p3_pos);
\draw (p3_dir) to[last]  (S3_dir);
\draw[blue] (S_pos) to[first] (S1_pos);
\draw[blue] (S1_dir) to[climb] (S2_pos);
\draw[blue] (S2_dir) to[climb] (S3_pos);
\draw[blue] (S3_dir) to[last] (S_dir);
\node[blue] at ($(S.east)!.33!(S2.west)$) {$\delta^{(3)}$};
\node at ($(S1.east)!.33!(p1.west)$) {$\varphi$};
\node at ($(S2.east)!.33!(p2.west)$) {$\varphi$};
\node at ($(S3.east)!.33!(p3.west)$) {$\varphi$};
\end{tikzpicture}
\node[above] at (obtain.north) (obtain_lab) {obtain $\text{Run}_3(\varphi)$:};
\node at (given|-obtain_lab) {Given $\varphi\colon \car{s}\to p$,};
\end{tikzpicture}
\]

Notice that we have only defined $\delta^{(n)}$, and thus $\text{Run}_n(\varphi)$, for integers $n\geq2$.
But $n=0$ runs through $n$ is doing nothing, modeled by the do-nothing section $\epsilon\colon\car{s}\to\yon$, while $n=1$ run through $\varphi$ is modeled by $\varphi\colon\car{s}\to\car{s}$ itself.
So we want $\text{Run}_0(\varphi)=\epsilon$ and $\text{Run}_1(\varphi)=\varphi$; we can achieve this by setting $\delta^{(0)}\coloneqq\epsilon$ and $\delta^{(1)}\coloneqq\id_\car{s}$.
Here we should think of the do-nothing section $\delta^{(0)}$ as the transition lens modeling $0$ steps through our state system, and the identity $\delta^{(1)}$ as the transition lens modeling a single step.

Verify that when $\delta^{(0)}=\epsilon$ and $\delta^{(1)}=\id_\car{s}$, if $\text{Run}_n(\varphi)$ is defined as $\delta^{(n)}\then\varphi\tripow{n}$ for all $n\in\nn$, then $\text{Run}_0(\varphi)=\epsilon$ and $\text{Run}_1(\varphi)=\id_\car{s}$.

We have $\text{Run}_n(\varphi)=\delta^{(n)}\then\varphi\tripow{n}$ for all $n\in\nn$, as well as $\delta^{(0)}=\epsilon$ and $\delta^{(1)}=\id_\car{s}$.
Then $\text{Run}_0(\varphi)=\epsilon\then\varphi\tripow0=\epsilon\then\id_\yon=\epsilon$ and $\text{Run}_1(\varphi)=\id_\car{s}\then\varphi\tripow1=\varphi\tripow1=\varphi$.

[Returning every other output]
In <ref>, we built a dynamical system $\varphi\colon S\yon^S\to\nn\yon$ that outputs natural numbers—specifically digits, alternating between $0$'s and the base-$10$ digits of $1/7$ after the decimal point like so:

\[
\begin{tikzpicture}[oriented WD]
\node[bb={1}{2}, fill=blue!10] (inner) {};
\node[bb={0}{0}, inner xsep=1cm, inner ysep=1cm] (outer) {};
\coordinate (outer_out1) at (outer.east|-inner_out1);
\draw[shorten >=-3pt] (inner_out1) -- (outer_out1);
\draw
let \p1=(inner.south east), \p2=(inner.south west), \n1=\bbportlen, \n2=\bby in
(inner_out2) to[in=0] (\x1+\n1,\y1-\n2) -- (\x2-\n1,\y1-\n2) to[out=180] (inner_in1);
\node[right, font=\footnotesize] at (outer_out1) {$0,1,0,4,0,2,0,8,0,5,0,7,0,1,0,4,0,2,0,8,0,5,0,7,0,1,0,4,0,2,0,8,0,5,0,7,\ldots$};
\end{tikzpicture}
\]

Say we only wanted the system to return the digits of $1/7$ after the decimal point; we'd like to do away with all these $0$'s.
In other words, we want a new system $S\yon^S\to\nn\yon$ that acts like $\varphi$, except that it only returns every other output that $\varphi$ returns.

We could build such a system from scratch—or we can simply start from $\varphi$ and apply $\text{Run}_2$, yielding a system $\text{Run}_2(\varphi)\colon S\yon^S\to\nn\yon\tri\nn\yon\iso\nn^\2\yon$ that returns the outputs of $\varphi$ two at a time:

\[
\]

Then we just need to compose $\text{Run}_2(\varphi)$ with a lens $\pi_2\colon\nn^\2\yon\to\nn\yon$ equal to the second coordinate projection on positions (and the identity on directions) to extract the outputs we want.
The new system $S\yon^S\to\nn\yon$ that skips over every output of $\varphi$ is therefore the following composite:

\[
\begin{tikzcd}
S\yon^S\ar[r, "\delta^{(2)}"]\ar[rr, bend right, "{\text{Run}_2(\varphi)}"']&
S\yon^S\tri S\yon^S\ar[r, "\varphi\tripow2"]&
\nn\yon\tri\nn\yon\iso\nn^\2\yon\ar[r,"\pi_2"]&
\nn\yon.
\end{tikzcd}
\]

We can apply this technique in general to skip (or otherwise act on) the outputs of a dynamical system at regular intervals.

One drawback of the $\text{Run}_n(-)$ operation is that we need to keep track of a separate morphism $S\yon^S\to p\tripow{n}$ for every $n\in\nn$, as well as various ways to relate these morphisms for different values of $n$.
Is there a way to package all this information into a single morphism that can model arbitrarily long runs through the system?
We will answer this question in <ref>; but for now, let us investigate what's really going on with our state systems algebraically.

§.§ State systems as comonoids

It turns out that objects equipped with morphisms like those in <ref> that satisfy the commutative diagrams from <ref> are well-known to category theorists.

In a monoidal category $(\Cat{C},\yon,\tri)$, a comonoid $\com{C}\coloneqq(\car{c},\epsilon,\delta)$ consists of

* an object $\car{c}\in\Cat{C}$, called the carrier;

* a morphism $\epsilon\colon\car{c}\to\yon$ in $\Cat{C}$, called the eraser (or the counit); and

* a morphism $\delta\colon\car{c}\to\car{c}\tri\car{c}$ in $\Cat{C}$, called the duplicator (or the comultiplication);

such that the following diagrams, collectively known as the comonoid laws, commute:

\begin{equation}\label{eqn.erasure_law}
\begin{tikzcd}[background color=definitioncolor, row sep=large]
\yon\tri \car{c}&\car{c}\ar[d, "\delta" description]\ar[r, equal]\ar[l, equal]&\car{c}\tri\yon\\&
\car{c}\tri\car{c},\ar[ul, "\epsilon\:\tri\:\car{c}"]\ar[ur, "\car{c}\:\tri\:\epsilon"']
\end{tikzcd}
\end{equation}

where the left triangle is known as the left erasure (or counit) law and the right triangle is known as the right erasure (or counit) law; and

\begin{equation}\label{eqn.coassoc_law}
\begin{tikzcd}[row sep=large]
\car{c}\ar[r, "\delta"]\ar[d, "\delta"']&
\car{c}\tri\car{c}\ar[d, "\car{c}\:\tri\:\delta"]\\
\car{c}\tri \car{c}\ar[r, "\delta\:\tri\:\car{c}"']&
\car{c}\tri\car{c}\tri\car{c},
\end{tikzcd}
\end{equation}

known as the coassociative law.

We may also say that the eraser and duplicator morphisms comprise a comonoid structure on the carrier, or we may identify a comonoid with its carrier if the eraser and duplicator can be inferred from context.

We refer to a comonoid $\com{C}$ in $(\poly,\yon,\tri)$ as a polynomial comonoid.

The concept of a comonoid in a monoidal category is dual to that of a monoid, which may be more familiar.
Monoids come with unit and multiplication morphisms that point the other way, so named because they generalize the unit and multiplication operations of a monoid in $\smset$.
(We'll talk more about monoids in $\smset$ in <ref>.)
Prepending `co-' to each term yields the corresponding terms for comonoids.

The alternative names eraser for the counit and duplicator for the comultiplication are less standard, but we will favor them to avoid confusion between the counit of a comonoid and the counit of an adjunction—and so that their names match up with the Greek letters $\epsilon$ and $\delta$ that we will so often use to label them.
The word “duplicator” comes from the fact that $\delta\colon\car{c}\to\car{c}\tri\car{c}$ effectively turns one $\car{c}$ into two, while the “eraser” $\epsilon\colon\car{c}\to\yon$ erases the $\car{c}$ altogether, leaving only the monoidal unit $\yon$.
Still, it can be helpful to think of comonoids as having a coassociative comultiplication along with a counit satisfying left and right counit laws.

Comonoids in a functor category with respect to the composition product are generally known as comonads.
So it would be a little more precise and familiar to refer to our polynomial comonoids as polynomial comonads.
But since we think of our polynomials more often in terms of positions and directions than as functors, we’ll favor the term comonoid over comonad.

[State systems are polynomial comonoids]
Nearly all our work on state systems up until now can be summarized thusly:

every state system is a polynomial comonoid,

whose eraser is the do-nothing section

and whose duplicator is the transition lens.

The comonoid structure on a state system $\car{s}$ is what allows us to write canonical lenses $\car{s}\to\car{s}\tripow{n}$ for any $n\in\nn$.
We can then model $n$ steps through a dynamical system $\varphi\colon\car{s}\to p$ with interface $p\in\poly$ by composing this canonical lens with $\varphi\tripow{n}$ to obtain a “sped-up” dynamical system $\text{Run}_n(\varphi)$.
This new system has the same state system $\car{s}$, but its interface is now $p\tripow{n}$.

The canonicity of $\car{s}\to\car{s}\tripow{n}$ is due to the following standard result about comonoids, which can be proved inductively.

Given a comonoid $(\car{c},\epsilon,\delta)$, let $\delta^{(n)}\colon\car{c}\to\car{c}\tripow{n}$ be given as follows. Let $\delta^{(0)}\coloneqq\epsilon$ and inductively define $\delta^{(n+1)}\coloneqq\delta\then\left(\delta^{(n)}\tri\car{c}\right)$ for all $n\in\nn$.
Then we have the following:

* $\delta^{(n)}$ is a morphism $\car{c}\to\car{c}\tripow{n}$ for all $n\in\nn$;

* $\delta^{(1)}=\car{c}=\id_\car{c}$;

* $\delta^{(2)}=\delta$; and

* $\delta^{(n)}=\delta\then\left(\delta^{(k)}\tri\delta^{(n-k)}\right)$ for all $k,n\in\nn$ with $k\leq n$, so our choice of morphism $\car{c}\to\car{c}\tripow{(n+1)}$ is canonical.

We leave parts (a), (b), and (c) for <ref>. Part (d) amounts to coassociativity.

We'll continue to use the notation introduced here throughout for general comonoids.

Prove the first three parts of <ref>.

* Prove part (a).

* Prove part (b).

* Prove part (c).

We complete the proof of <ref>, where we are given a comonoid $(\car{c},\epsilon,\delta)$ along with $\delta^{(0)}\coloneqq\epsilon$ and $\delta^{(n+1)}\coloneqq\delta\then\left(\delta^{(n)}\tri\car{c}\right)$ for all $n\in\nn$.

* We will show that $\delta^{(n)}$ is a morphism $\car{c}\to\car{c}\tripow{n}$ for every $n\in\nn$ by induction on $n$.
We know $\delta^{(0)}=\epsilon$ is a morphism $\car{c}\to\yon=\car{c}\tripow0$, and for each $n\in\nn$, if $\delta^{(n)}$ is a morphism $\car{c}\to\car{c}\tripow{n}$, then the composite $\delta^{(n+1)}=\delta\then\left(\delta^{(n)}\tri\car{c}\right)$ is a morphism

\[
\car{c}\To\delta\car{c}\tri\car{c}\To{\delta^{(n)}\:\tri\:\car{c}}\car{c}\tripow{n}\tri\car{c}\iso\car{c}\tripow{(n+1)}
\]

Hence the result follows by induction.

* We have $\delta^{(1)}=\delta\then(\delta^{(0)}\tri\car{c})=\delta\then(\epsilon\tri\car{c})=\id_\car{c}$ by the left erasure law from (<ref>).

* By the previous part, we have $\delta^{(2)}=\delta\then(\delta^{(1)}\tri\car{c})=\delta\then(\car{c}\tri\car{c})=\delta$.

[Not all polynomial comonoids are state systems]
At this point, a natural question to ask is whether everything we know about a state system $\car{s}$ is captured by the fact that state systems are polynomial comonoids.
In other words, are state systems the only polynomial comonoids there are?

The answer turns out to be no.
After all, there is one fact about state systems from <ref> that we did not encode in $\poly$: for a fixed state $s\in\car{s}(\1)$, the target function $\car{s}[s]\to\car{s}(\1)$ sending directions at $s$ to their target states is a bijection.

Nothing in our comonoid laws guarantees this bijectivity.
An arbitrary polynomial comonoid might send different directions at $s$ to the same target—given a second state $t$, there may be multiple ways to get from $s$ to $t$.
It might even send no directions at $s$ to a target $t$, making it impossible to get from $s$ to $t$.
(We'll give an explicit example of a comonoid that is not a state system in <ref>.)
State systems as we have defined them are just the polynomial comonoids that do not allow either of these variations, for which the bijective property holds.

We consider this a feature, not a bug.
After all, it is an abstraction to say that there is exactly one way to get from any one state in a system to another.
It is perfectly plausible that the inner workings of a state system do not permit traveling between some states and differentiate ways of traveling between others.
We won't formally introduce this idea into our theory of dependent dynamical systems,
but we will often think of polynomial comonoids as a sort of generalized state system throughout the rest of the book.

[A comonoid that is not a state system]
The polynomial $\yon^\2+\yon$ is not a state system: one of its direction-sets has one fewer element than its position-set.
But it can still be given a comonoid structure.
We describe that structure here, but we will go a little quickly, because we'll soon discover a much more familiar way to think about comonoids.

Define $\car{a}\coloneqq\{s\}\yon^{\{\id_s,a\}}+\{t\}\yon^{\{\id_t\}}\iso\yon^\2+\yon$.
Here is its tree picture:

\[
\begin{tikzpicture}[rounded corners]
\node (p1) [draw, "$\car{a}\coloneqq$" left] {
\begin{tikzpicture}[trees, sibling distance=5mm]
\node["\tiny $s$" below, red] (1) {$\bullet$}
child  {coordinate (is) \idchild}
child {coordinate (a)};
\node[right=.8 of 1,"\tiny $t$" below, blue] (2) {$\bullet$}
child  {coordinate (it) \idchild};
\node[below left=0 of is, font=\tiny] {$\id_s$};
\node[below left=.1 of it, font=\tiny] {$\id_t$};
\node[below right=.1 of a, font=\tiny] {$a$};
\end{tikzpicture}
\end{tikzpicture}
\]

Notice that we have drawn one direction out of each position—$\id_s$ and $\id_t$—with a double bar.
We let these be the directions that the eraser $\epsilon\colon\car{a}\to\yon$ picks out.
The double bar is meant to evoke an equals sign from the root position to the eventual target position, which is appropriate, as these two positions should be equal for every direction that the eraser selects.
We can draw the selections that $\epsilon$ makes like so:

\[
\begin{tikzpicture}[trees, bend right=60]
\node[red] (1) {$\bullet$}
child  {coordinate (11) \idchild}
child {coordinate (12)};
\node[right=1.5 of 1] (1y) {$\bullet$}
child {coordinate (1y1)};
\node[right=2 of 1y, blue] (2) {$\bullet$}
child  {coordinate (21) \idchild};
\node[right=1.5 of 2] (2y) {$\bullet$}
child {coordinate (2y1)};
\draw[|->, shorten <= 3pt, shorten >= 3pt] (1) -- (1y);
\draw[|->, shorten <= 3pt, shorten >= 3pt] (2) -- (2y);
\draw[densely dotted, postaction={decorate}] (1y1) to (11);
\draw[densely dotted, postaction={decorate}] (2y1) to (21);
\end{tikzpicture}
\]

Now we need a duplicator $\delta\colon\car{a}\to\car{a}\tri\car{a}$.
Before we define it, let's draw out $\car{a}\tri\car{a}$ to see what it looks like.
Remember that we need to glue corollas of $\car{a}$ to leaves of $\car{a}$ in every possible way:

\[
\begin{tikzpicture}[rounded corners]
\node (p1) [draw, "$\car{a}\tri\car{a}=$" left] {
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=5mm},
level 2/.style={sibling distance=2.5mm}]
\node[red] (1) {$\bullet$}
child  {
node [red] {$\bullet$}
child  {\idchild}
child {}
\idchild
child  {
node [red] {$\bullet$}
child  {\idchild}
child {}
\node[right=1 of 1, red] (2) {$\bullet$}
child  {
node [red]{$\bullet$}
child  {\idchild}
child {}
\idchild
child {node [blue] {$\bullet$}
child  {\idchild}
\node[right=1 of 2, red] (3) {$\bullet$}
child {node [blue] {$\bullet$}
child  {\idchild}
\idchild
child  {
node [red] {$\bullet$}
child {\idchild}
child {}
\node[right=1 of 3, red] (4) {$\bullet$}
child {node [blue] {$\bullet$}
child  {\idchild}
\idchild
child {node [blue] {$\bullet$}
child  {\idchild}
\node[right=.8 of 4, blue] (5) {$\bullet$}
child  {
node [red] {$\bullet$}
child  {\idchild}
child {}
\idchild
\node[right=.6 of 5, blue] (6) {$\bullet$}
child {node [blue] {$\bullet$}
child  {\idchild}
\idchild
\end{tikzpicture}
\end{tikzpicture}
\]

Each of these trees gives a way to match directions out of one position to positions they could lead to.
On positions, $\delta$ will decide which matchings to pick by sending the red $s$ to one of the four positions on the left and the blue $t$ to one of the two positions on the right.
We want the double-barred directions that the eraser picked out to have the same position on either end (in fact, the erasure laws guarantee this).
So the only choice to be made is whether we want the other direction $a$ at $s$ to point to $s$ or to $t$.
Let's pick $t$ for the time being, so that on positions, $\delta$ looks like this:

\[
\begin{tikzpicture}[trees, sibling distance=5mm,	bend right=60]
\node (1A) [red] {$\bullet$}
child  {coordinate (1A1) \idchild}
child {coordinate (1A2)};
\node (2A) [right=1.5 of 1A, red] {$\bullet$}
child  {
node [red] {$\bullet$}
child  {coordinate (2A1) \idchild}
child {coordinate (2A2)}
\idchild
child {node [blue] {$\bullet$}
child  {coordinate (2A3) \idchild}
\draw[|->, shorten <= 3pt, shorten >= 3pt] (1A) -- (2A);
% 	\draw[densely dotted, postaction={decorate}] (2A1) to (1A1);
% 	\draw[densely dotted, postaction={decorate}] (2A2) to (1A2);
% 	\draw[densely dotted, postaction={decorate}] (2A3) to (1A2);
\node[right=2 of 2A, blue] (1B) {$\bullet$}
child  {coordinate (1B1) \idchild};
\node[right=1.5 of 1B, blue] (2B) {$\bullet$}
child {node [blue] {$\bullet$}
child  {coordinate (2B1) \idchild}
\idchild
\draw[|->, shorten <= 3pt, shorten >= 3pt] (1B) -- (2B);
% 	\draw[densely dotted, postaction={decorate}] (2B1) to (1B1);
\end{tikzpicture}
\]

As in <ref>, we can interpret this as telling us how to “bend” the arrows of $\car{a}$ so that they point to other positions:

\begin{equation} \label{eqn.walking_arrow_bent_cor}
\begin{tikzpicture}[baseline=(b)]
\node[circle,minimum size=2cm] (b) {};
\foreach\x/\c in {1/red, 2/blue} {
\node[minimum size=0.1cm,draw,circle,\c,fill=\c] (2-\x) at (b.{360/2*\x}){};
\draw[double, -] (2-\x) to [in=360/2*\x-30,out=360/2*\x+30,loop] ();
\relax
\draw (2-1) edge[->] (2-2);
\end{tikzpicture}
\end{equation}

Meanwhile, on directions, $\delta$ should tell us how to run two directions together into one.
Fortunately, there's not much for us to do here—we know that if one of the two directions $\delta$ runs together is one of the double-barred directions that the eraser picked out, then $\delta$ should ignore that “do-nothing” direction and yield the other direction (again, the erasure laws ensure this).
Here's what that looks like:

\begin{equation}\label{eqn.my_comonoid_delta}
\begin{tikzpicture}[trees, sibling distance=5mm,	bend right=60]
\node (1A) [red] {$\bullet$}
child  {coordinate (1A1) \idchild}
child {coordinate (1A2)};
\node (2A) [right=1.5 of 1A, red] {$\bullet$}
child  {
node [red] {$\bullet$}
child  {coordinate (2A1) \idchild}
child {coordinate (2A2)}
\idchild
child {node [blue] {$\bullet$}
child  {coordinate (2A3) \idchild}
\draw[|->, shorten <= 3pt, shorten >= 3pt] (1A) -- (2A);
\draw[densely dotted, postaction={decorate}] (2A1) to (1A1);
\draw[densely dotted, postaction={decorate}] (2A2) to (1A2);
\draw[densely dotted, postaction={decorate}] (2A3) to (1A2);
\node[right=2 of 2A, blue] (1B) {$\bullet$}
child  {coordinate (1B1) \idchild};
\node[right=1.5 of 1B, blue] (2B) {$\bullet$}
child {node [blue] {$\bullet$}
child  {coordinate (2B1) \idchild}
\idchild
\draw[|->, shorten <= 3pt, shorten >= 3pt] (1B) -- (2B);
\draw[densely dotted, postaction={decorate}] (2B1) to (1B1);
\end{tikzpicture}
\end{equation}

And that's all we need to specify the triple $(\car{a},\epsilon,\delta)$.

Here are $\epsilon\colon\car{a}\to\yon$ and $\delta\colon\car{a}\to\car{a}\tri\car{a}$ again, in terms of polyboxes.

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (S) {$\id_s$\at$s$};

\draw (S_pos) to[climb'] node[right] {$\epsilon$} (S_dir);
\end{tikzpicture}
\node[right=1 of p1] (p2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (S) {$\id_t$\at$t$};

\draw (S_pos) to[climb'] node[right] {$\epsilon$} (S_dir);
\end{tikzpicture}
\end{tikzpicture}
\]

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (p) {$\id_s$\at$s$};
\node[poly, cod, right=of p.south, yshift=-1ex, "$\car{a}$" below] (q) {$\id_s$\at$s$};
\node[poly, cod, above=of q, "$\car{a}$" above] (r) {$\id_s$\at$s$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb, "$\delta$" left] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.3 of p1] (p2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (p) {$a$\at$s$};
\node[poly, cod, right= of p.south, yshift=-1ex, "$\car{a}$" below] (q) {$\id_s$\at$s$};
\node[poly, cod, above=of q, "$\car{a}$" above] (r) {$a$\at$s$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb, "$\delta$" left] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.3 of p2] (p3) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (p) {$a$\at$s$};
\node[poly, cod, right= of p.south, yshift=-1ex, "$\car{a}$" below] (q) {$a$\at$s$};
\node[poly, cod, above=of q, "$\car{a}$" above] (r) {$\id_t$\at$t$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb, "$\delta$" left] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.3 of p3] (p4) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{a}$" left] (p) {$\id_t$\at$t$};
\node[poly, cod, right= of p.south, yshift=-1ex, "$\car{a}$" below] (q) {$\id_t$\at$t$};
\node[poly, cod, above=of q, "$\car{a}$" above] (r) {$\id_t$\at$t$};
\draw (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb, "$\delta$" left] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\end{tikzpicture}
\]

Of course, we have yet to check that $(\car{a},\epsilon,\delta)$ really is a comonoid, i.e. that the diagrams in (<ref>) and (<ref>) commute.
We leave that for <ref>.

Verify that $(\car{a},\epsilon,\delta)$ as defined in <ref> obeys the erasure laws in (<ref>) and the coassociative law in (<ref>).

We will eventually see that comonoids in $\poly$ are categories; this gives us intuition for what is going on here. In fact the category corresponding to the comonoid in this exercise is the walking arrow, depicted in (<ref>). The erasure (counit) laws are verified by looking at the picture of $\delta$ in (<ref>) and noting that it sends the double (do-nothing) lines (the identities) back to the double lines.

Show that if $B$ is a set, then there exists a unique comonoid structure on the linear polynomial $B\yon$.

Given a set $B$, we wish to give a comonoid structure on $B\yon$ and show that it is unique.
There is only one way to define an eraser lens $\epsilon\colon B\yon\to\yon$: the on-position function is the unique map $!\colon B\to\1$, while every on-directions function $\1\to\1$ must be the identity.
Meanwhile $B\yon\tri B\yon\iso B^\2\yon$, so to specify a duplicator lens $\delta\colon B\yon\to B^\2\yon$, it suffices to specify an on-positions function $\delta_\1\colon B\to B^\2$, and every on-directions function will again be the identity.

All the comonoid laws should then hold trivially on directions, so it suffices to consider each law on positions.
The erasure laws imply that the composite functions

\[
B\To{\delta_\1}B\times B\To{B\:\times\:!}B\times\1\iso B,
\]

where the second map is just the canonical left projection, and

\[
B\To{\delta_\1}B\times B\To{!\:\times\:B}\1\times B\iso B,
\]

where the second nap is just the canonical right projection, are both the identity on $B$.
The only function $\delta_\1\colon B\to B\times B$ that satisfies this condition is the diagonal $a\mapsto(a,a)$.
It is easy to verify that the diagonal is coassociative, so this does define a unique comonoid structure on $B\yon$.
(It turns out that this is equivalent to the well-known result that there is a unique comonoid structure on every set in $(\smset,\1,\times)$.)

Once you know that state systems are comonoids in $\poly$, but not the only ones, the natural question to ask is “what are all the other comonoids in $\poly$?”
Or perhaps, as we led you through this case study of $\car{s}$, you have already suspected the truth: a polynomial comonoid—what with its directions leading from one position to another, directions that can be run together associatively among which there are directions at every position that do nothing—is just another name for a category.

§ POLYNOMIAL COMONOIDS ARE CATEGORIES

What Ahman and Uustalu showed was that polynomial comonoids can be identified with categories.
Every category in the usual sense is a comonoid in $\poly$, and every comonoid in $\poly$ is a category.
We find their revelation to be truly shocking, and it suggests some very different ways to think about categories.
But let's go over their result first.

There is a one-to-one isomorphism-preserving correspondence between polynomial comonoids and (small) categories.

Our goal is to spell out this correspondence so that we can justly proclaim:

Comonoids in $\poly$ are precisely categories!

§.§ Translating between polynomial comonoids and categories

First, we describe how to translate between the carrier $\car{c}$ of a comonoid $\com{C}\coloneqq(\car{c},\delta,\epsilon)$ and the objects and morphisms of the corresponding category $\cat{C}$.
The idea is pretty simple, and you may have already guessed it: positions are objects and directions are morphisms.

§.§.§ Positions as objects, directions as morphisms

More precisely, the positions of $\car{c}$ are the objects of $\cat{C}$:

\begin{equation} \label{eqn.pos_obj}
\car{c}(\1)=\Ob\cat{C}.
\end{equation}

Then for each such position or object $i$, the $\car{c}[i]$-directions are the morphisms of $\cat{C}$ with domain $i$:

\begin{equation} \label{eqn.dir_mor}
\car{c}[i]=\sum_{j\in\Ob\cat{C}}\cat{C}(i,j).
\end{equation}

The right hand side above is a little clumsier than the left; this is because while we are used to thinking of hom-sets of categories such as $\cat{C}(i,j)$, consisting of all morphisms in $\cat{C}$ with a fixed domain and codomain, we aren't used to thinking about the collection of all morphisms in $\cat{C}$ with a fixed domain and an arbitrary codomain quite as often.
[Except, perhaps, in the context of coslice categories.]
On the other hand, the carrier only encodes which morphisms have each object as its domain, i.e. which directions are at each position.
Codomains will be encoded in the data of the comonoid elsewhere.

This is the key difference in perspective between the polynomial comonoid perspective of categories, in contrast to our usual hom-set perspective: the polynomial perspective is in a sense domain-centric, as highlighted by the following definition.

Let $\cat{C}$ be a category.
For every object $i$ in $\cat{C}$, denote the morphisms in $\cat{C}$ with domain $i$ by $\cat{C}[i]$, so thatWe may also write $f\colon i\to\_$ to denote an arbitrary morphism $f\in\cat{C}[i]$, i.e. a morphism $f$ in $\cat{C}$ with domain $i$ and an unspecified codomain.

\[
\cat{C}[i]\coloneqq\sum_{j\in\Ob\cat{C}}\cat{C}(i,j).
\]

Then the polynomial carrier, or simply carrier, of $\cat{C}$ is the polynomial

\[
\sum_{i\in\Ob\cat{C}}\yon^{\cat{C}[i]}.
\]

So everything we have said so far about the correspondence from <ref> can be summarized by saying that it preserves carriers: the carrier of the category $\cat{C}$ is the carrier $\car{c}$ of the comonoid $\com{C}$, so that $\Ob\cat{C}=\car{c}(\1)$ and $\cat{C}[i]=\car{c}[i]$.

If we take the perspective that categories are equal if and only if their objects and morphisms are equal and obey the same laws, and similarly that polynomials are equal if and only if their position-sets and direction-sets are equal sets, then (<ref>) and (<ref>) really can be just strict equalities.
This is why we are comfortable naming a “one-to-one correspondence” in <ref> rather than just, say, some form of equivalence.
Since the positions and directions of our polynomials always form sets, however, the categories we obtain under this correspondence are also necessarily small: their objects form a set, as do all of their morphisms.
But we won't worry too much about size issues beyond this.

What is the carrier of each of the following categories (up to isomorphism)?

* The category

where we have drawn every morphism except for the identity morphisms.

* The category

where we have drawn every morphism except for the identity morphisms.

* The empty category.

*  A category with exactly $1$ object and a morphism $i$, for which every morphism can be written uniquely as the $n$-fold composite of $i$ for some $n\in\nn$.

*  The category

where there is a unique morphism $m\to n$ if $m\leq n$ (and no other morphisms).

* The category

where there is a unique morphism $m\from n$ if $m\leq n$ (and no other morphisms).

* The category white$A\Too{f}B$ has $2$ morphisms out of $A$, namely $\id_A$ and $f$; and $1$ morphism out of $B$, namely $\id_B$.
So its carrier is $\{A\}\yon^{\{\id_A,f\}}+\{B\}\yon^{\{\id_B\}}\iso\yon^\2+\yon$.

* The category white$B\To{g}A\From{h}C$ has $1$ morphism out of $A$, namely $\id_A$; $2$ morphisms out of $B$, namely $\id_B$ and $g$; and $2$ morphisms out of $C$, namely $\id_C$ and $h$.
So its carrier is $\{A\}\yon^{\{\id_A\}}+\{B\}\yon^{\{\id_B,g\}}+\{C\}\yon^{\{\id_C,h\}}\iso\2\yon^\2+\yon$.

* The empty category has no objects or morphisms, so its carrier is just $\0$.

* The category in question has $1$ object, and its set of morphisms is in bijection with $\nn$, so its carrier is isomorphic to $\yon^\nn$.
(This category is the monoid $(\nn,0,+)$ viewed as a $1$-object category; see <ref> for the general case.)

* The category in question has $\nn$ as its set of objects, and for each $m\in\nn$, the morphisms out of $m$ are determined by their codomains: there is exactly $1$ morphism $m\to n$ for every $n\in\nn$ satisfying $m\leq n$, and no other morphisms out of $m$.
So the carrier of the category is isomorphic to

\[
\sum_{m\in\nn}\yon^{\{n\in\nn\mid m\leq n\}}\iso\nn\yon^\nn,
\]

as $\{n\in\nn\mid m\leq n\}\iso\nn$ under the bijection $n\mapsto n-m$.
(This category is the poset $(\nn,\leq)$.)

* The category in question has $\nn$ as its set of objects, and for each $n\in\nn$, the morphisms out of $n$ are again determined by their codomains: there is exactly $1$ morphism $n\to m$ for every $m\in\nn$ satisfying $m\leq n$, and no other morphisms out of $n$.
So the carrier of the category is isomorphic to

\[
\sum_{n\in\nn}\yon^{\{m\in\nn\mid m\leq n\}}\iso\sum_{n\in\nn}\yon^{\ord{n+1}}\iso\yon^\1+\yon^\2+\yon^\3+\cdots.
\]

(This category is the poset $(\nn,\geq)$.)

But a category $\cat{C}$ is more than its carrier polynomial, just as a comonoid $\com{C}$ is more than its carrier $\car{c}$.
In particular, we have said nothing about the codomains of morphisms in $\cat{C}$, nor anything about identity morphisms, composition, or how the laws of a category are satisfied.
Similarly, we have said nothing about the eraser $\epsilon$ or the duplicator $\delta$ of $\com{C}$, nor anything about how the comonoid laws are satisfied.
It turns out that all of these constituents and laws correspond to one another, as summarized by the following table.
Here each item in the comonoid column—either a polynomial, a lens, or a lens equation—spans two rows, with the top row corresponding to positions and the bottom row corresponding to directions.

Comonoid     $\com{C}=(\car{c},\epsilon,\delta)$     Category     $\cat{C}$

2*carrier     $i\in\car{c}(\1)$     objects     $i\in\Ob\cat{C}$

$f\in\cat{c}[i]$     morphisms     $f\colon i\to\_$

2*eraser     $\epsilon_\1\colon\car{c}(\1)\to\1$     —     —

$\epsilon_i^\sharp\colon\1\to\car{c}[i]$     identities     $\id_i\colon i\to\_$

2*duplicator     $\delta_\1\colon\car{c}(\1)\to(\car{c}\tri\car{c})(\1)$     codomains*     $\cod\colon\cat{C}[i]\to\Ob\cat{C}$

$\delta_i^\sharp\colon(\car{c}\tri\car{c})[\delta_\1(i)]\to\car{c}[i]$     composition*     $\then$

2c|2*right erasure law     2c$\ast$

2c|     2cright identity law

2c|2*left erasure law     codomains of identities     $\cod\id_i=i$

2c|     2cleft identity law

2c|2*coassociative law     codomains of composites     $\cod(f\then g)=\cod g$

2c|     2cassociative law of composition

Note that the on-positions function of $\epsilon$, being a function into the terminal set, encodes no actual data.
The asterisk $\ast$ indicates that the right erasure law on positions works together with the duplicator to ensure that codomains and composites are properly specified.

We have already covered the correspondence between the first two rows, so let us consider each of the following rows in turn.
In some sense, we have already seen each piece of this correspondence in action for state systems in <ref>, so we'll go through it a little faster this time for the general case.

§.§.§ The eraser assigns identities

We know that the eraser $\epsilon\colon\car{c}\to\yon$ can be identified with a dependent function $(i\in\car{c}(\1))\to\com{c}[i]$, sending each position $i\in\com{c}(\1)$ to a $\com{c}[i]$-direction.
In terms of our category $\cat{C}$, the eraser sends each object $i\in\Ob\cat{C}$ to a morphism $i\to\_$.
But this is exactly what we need to specify identity morphisms—a morphism out of each object.
So the eraser of $\car{c}$ specifies the identity morphisms of the corresponding category $\cat{C}$.
We can interpret the polybox picture for $\epsilon$ like so:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (c) {$\id_i$\at$i$};
\draw (c_pos) to[climb'] node[right] {$\idy$} (c_dir);
\end{tikzpicture}
\]

Here we have given the label $\idy$ to the arrow sending objects to their identity morphisms.

Keep in mind that from the domain-centric polynomial perspective, we have not yet specified that the codomain of an identity morphism is equal to its domain; that comes later.

§.§.§ The right erasure law on positions: a bit of bookkeeping

Keeping our label $\idy$ for the arrow in $\epsilon$, the right erasure law $\delta\then(\car{c}\tri\epsilon)=\id_\car{c}$ from (<ref>) can be drawn in polyboxes like so:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (r) {\at$i$};
\node[poly, cod, right=2 of r.south, yshift=-2.5ex, "$\car{c}$" below] (p) {\at$i$};
\node[poly, above=.8 of p, "$\car{c}$" above] (p') {};

\draw (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[left=.1] {$\delta$} (p'_pos);
\draw (p'_pos) to[climb'] node[right] {$\idy$} (p'_dir);
\draw (p'_dir) to[last] node[above=.4] {} (r_dir);
\end{tikzpicture}
\node[right=1.8 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (c) {\at$i$};
\node[poly, cod, right=of c, "$\car{c}$" right] (c') {\at$i$};
\draw[double,-] (c_pos) -- (c'_pos);
\draw[double,-] (c'_dir) -- (c_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) (3) {=};
\end{tikzpicture}
\]

We have only filled in a few of the boxes, but that is enough to interpret what the right erasure law tells us on positions: that the bottom arrow of the duplicator must be the identity function on $\car{c}(\1)$.
Equipped with this knowledge, we can focus our attention on the other two arrows of $\delta$.

§.§.§ The duplicator assigns codomains and composites

In fact, in the polybox picture for $\delta\colon\car{c}\to\car{c}\tri\car{c}$, the middle arrow specifies codomains, and the top arrow specifies composition.
We therefore label these arrows as follows:[Compare these labels to the names “target” and “run” that we gave to the arrows of a state system's transition lens.]

\[
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{c}$" left] (yX) {};
\node[poly, cod, right=1.8 of yX.south, yshift=-2.5ex, "$\car{c}$" right] (p) {};
\node[poly, cod, above=.8 of p, "$\car{c}$" right] (p') {};

\draw[double, -] (yX_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above] {$\then$} (yX_dir);
\end{tikzpicture}
\]

To check that this makes sense, we fill in the boxes:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (yX) {$f\then g$\at$i$};
\node[poly, cod, right=2 of yX.south, yshift=-2.5ex, "$\car{c}$" right] (p) {$f$\at$i$};
\node[poly, cod, above=.8 of p, "$\car{c}$" right] (p') {$g$\at$\cod f$};

\draw[double, -] (yX_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above] {$\then$} (yX_dir);
\end{tikzpicture}
\]

Remember: each position box contains an object of $\cat{C}$, while each direction box contains a morphism of $\cat{C}$ emanating from the object below.
So $\delta$ takes an object $i\in\Ob\cat{C}$ and a morphism $f\colon i\to\_$ in $\cat{C}$ and assigns another object $\cod f\in\Ob\cat{C}$ to be the codomain of $f$.
It then takes another morphism $g\colon\cod f\to\_$ in $\cat{C}$ and assigns a morphism $f\then g\colon i\to\_$ to be the composite of $f$ and $g$.
In this way, every morphism gets a codomain, and every pair of morphisms that can be composed (i.e. the codomain of one matches the domain of the other) is assigned a composite.
As with the identity morphism, we don't know what the codomain of this composite morphism is yet; but we do know that the domain of $f\then g$ matches the domain of $f$, as it should.

§.§.§ The left erasure law on positions: codomains of identities

As with the right erasure law, we can partially fill in the polyboxes for the left erasure law $\delta\then(\epsilon\tri\car{c})=\id_\car{c}$ from (<ref>) to read what it says on positions:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (r) {\at$i$};
\node[poly, right=2 of r.south, yshift=-2.5ex, "$\car{c}$" below] (p) {$\id_i$\at$i$};
\node[poly, cod, above=.8 of p, "$\car{c}$" above] (p') {\at$\cod\id_i$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_pos) to[climb'] node[right] {$\idy$} (p_dir);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above] {$\then$} (r_dir);
\end{tikzpicture}
\node[right=1.8 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (c) {\at$i$};
\node[poly, cod, right=of c, "$\car{c}$" right] (c') {\at$i$};
\draw[double,-] (c_pos) -- (c'_pos);
\draw[double,-] (c'_dir) -- (c_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) (3) {=};
\end{tikzpicture}
\]

So the left erasure law on positions guarantees that $\cod\id_i=i$ for all $i\in\Ob\cat{C}$.
It makes sense that we would find this here: the eraser assigns identities, while the duplicator assigns codomains, so a statement about codomains of identities is a coherence condition between the eraser and the duplicator.

§.§.§ The erasure laws on directions are the identity laws

Let us finish filling in the polyboxes for the left and right erasure laws to see what they have to say on directions.
In the picture below, the left equality depicts the left erasure law (to conserve space, we'll substitute $i$ for $\cod\id_i$ on the left, which we now know we can do), while the right equality depicts the right erasure law:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (r) {$\id_i\then f$\at$i$};
\node[poly, right=2 of r.south, yshift=-2.5ex, "$\car{c}$" below] (p) {$\id_i$\at$i$};
\node[poly, cod, above=.8 of p, "$\car{c}$" above] (p') {$f$\at$i$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_pos) to[climb'] node[right] {$\idy$} (p_dir);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above] {$\then$} (r_dir);
\end{tikzpicture}
\node[right=.1 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (c) {$f$\at$i$};
\node[poly, cod, right=of c, "$\car{c}$" right] (c') {$f$\at$i$};
\draw[double,-] (c_pos) -- (c'_pos);
\draw[double,-] (c'_dir) -- (c_dir);
\end{tikzpicture}
\node[right=.25 of 2] (3) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{c}$" left] (r) {$f\then\id_{\cod f}$\at$i$};
\node[poly, cod, right=2.1 of r.south, yshift=-2.5ex, "$\car{c}$" below] (p) {$f$\at$i$};
\node[poly, above=.8 of p, xshift=1.5ex, "$\car{c}$" above] (p') {$\id_{\cod f}$\at$\cod f$};

\draw (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_pos) to[climb'] node[right] {$\idy$} (p'_dir);
\draw (p'_dir) to[last] node[above] {$\then$} (r_dir);
\end{tikzpicture}
\node at ($(1.east)!.2!(2.west)$) {=};
\node at ($(2.east)!.5!(3.west)$) {=};
\end{tikzpicture}
\]

We find that on directions, the erasure laws state that for every object $i\in\Ob\cat{C}$ and morphism $f\colon i\to\_$ in $\cat{C}$,

\[
\id_i\then f=f=f\then\id_{\cod f}.
\]

But these are precisely the identity laws of the category $\cat{C}$.

§.§.§ The coassociative law on positions: codomains of composites

It remains to consider the comonoid's coassociative law (<ref>), $\delta\then(\delta\tri\car{s})=\delta\then(\car{s}\tri\delta)$.
To read what it says on positions, we draw the polyboxes and fill them in, stopping just short of the uppermost direction box of the codomain:

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (m') {\at$i$};
\node[poly, right=1.8 of m'.south, yshift=-1ex, "$\car{s}$" below] (mm') {$f\then g$\at$i$};
\node[poly, above=of mm', "$\car{s}$" above] (C') {\at$\cod(f\then g)$};
\node[poly, cod, right=2.3 of mm'.south, yshift=-1ex, "$\car{s}$" right] (D') {$f$\at$i$};
\node[poly, cod, above=of D', "$\car{s}$" right] (mmm') {$g$\at$\cod f$};
\node[poly, cod, above=of mmm', "$\car{s}$" right] (CC') {\at$\cod(f\then g)$};
\draw[double, -] (m'_pos) to[first] (mm'_pos);
\draw (mm'_dir) to[climb] node[right] {$\cod$} (C'_pos);
\draw (C'_dir) to[last] node[above] {$\then$} (m'_dir);
\draw[double, -] (mm'_pos) to[first] (D'_pos);
\draw (D'_dir) to[climb] node[right] {$\cod$} (mmm'_pos);
\draw (mmm'_dir) to[last] node[above] {$\then$} (mm'_dir);
\draw[double, -] (C'_pos) to[first] (CC'_pos);
\draw[double, -] (CC'_dir) to[last] (C'_dir);
\end{tikzpicture}
\node (p2) [right=of p1] {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (m) {\at$i$};
\node[poly, right=1.8 of m.south, yshift=-1ex, "$\car{s}$" below] (D) {$f$\at$i$};
\node[poly, above=of D, "$\car{s}$" above] (mm) {\at$\cod f$};
\node[poly, cod, right=2.1 of D.south, yshift=-1ex, "$\car{s}$" right] (DD) {$f$\at$i$};
\node[poly, cod, above=of DD, "$\car{s}$" right] (mmm) {$g$\at$\cod f$};
\node[poly, cod, above=of mmm, "$\car{s}$" right] (C) {\at$\cod g$};
\draw[double, -] (m_pos) to[first] (D_pos);
\draw (D_dir) to[climb] node[right] {$\cod$} (mm_pos);
\draw (mm_dir) to[last] node[above] {$\then$} (m_dir);
\draw[double, -] (D_pos) to[first] (DD_pos);
\draw[double, -] (DD_dir) to[last] (D_dir);
\draw[double, -] (mm_pos) to[first] (mmm_pos);
\draw (mmm_dir) to[climb] node[right] {$\cod$} (C_pos);
\draw (C_dir) to[last] node[above] {$\then$} (mm_dir);
\end{tikzpicture}
\node at ($(p1.south)!.5!(p2.north)$) {$=$};
\end{tikzpicture}
\]

So on positions, the coassociative law states that given an object $i\in\Ob\cat C$ and morphisms $f\colon i\to\_$ and $g\colon\cod f\to\_$ in $\cat C$,

\[
\cod(f\then g)=\cod g.
\]

Hence composites are assigned the proper codomains.

§.§.§ The coassociative law on directions is the associative law of composition

Finally, let us fill in the remaining polyboxes for the coassociative law (we'll substitute $\cod g$ for $\cod(f\then g)$ on the left, which we now know we can do):

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (m') {$(f\then g)\then h$\at$i$};
\node[poly, right=1.8 of m'.south, yshift=-1ex, "$\car{s}$" below] (mm') {$f\then g$\at$i$};
\node[poly, above=of mm', "$\car{s}$" above] (C') {$h$\at$\cod g$};
\node[poly, cod, right=2 of mm'.south, yshift=-1ex, "$\car{s}$" right] (D') {$f$\at$i$};
\node[poly, cod, above=of D', "$\car{s}$" right] (mmm') {$g$\at$\cod f$};
\node[poly, cod, above=of mmm', "$\car{s}$" right] (CC') {$h$\at$\cod g$};
\draw[double, -] (m'_pos) to[first] (mm'_pos);
\draw (mm'_dir) to[climb] node[right] {$\cod$} (C'_pos);
\draw (C'_dir) to[last] node[above] {$\then$} (m'_dir);
\draw[double, -] (mm'_pos) to[first] (D'_pos);
\draw (D'_dir) to[climb] node[right] {$\cod$} (mmm'_pos);
\draw (mmm'_dir) to[last] node[above] {$\then$} (mm'_dir);
\draw[double, -] (C'_pos) to[first] (CC'_pos);
\draw[double, -] (CC'_dir) to[last] (C'_dir);
\end{tikzpicture}
\node (p2) [right=.8 of p1] {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{s}$" left] (m) {$f\then(g\then h)$\at$i$};
\node[poly, right=2.2 of m.south, yshift=-1ex, "$\car{s}$" below] (D) {$f$\at$i$};
\node[poly, above=of D, "$\car{s}$" above] (mm) {$g\then h$\at$\cod f$};
\node[poly, cod, right=2 of D.south, yshift=-1ex, "$\car{s}$" right] (DD) {$f$\at$i$};
\node[poly, cod, above=of DD, "$\car{s}$" right] (mmm) {$g$\at$\cod f$};
\node[poly, cod, above=of mmm, "$\car{s}$" right] (C) {$h$\at$\cod g$};
\draw[double, -] (m_pos) to[first] (D_pos);
\draw (D_dir) to[climb] node[right] {$\cod$} (mm_pos);
\draw (mm_dir) to[last] node[above] {$\then$} (m_dir);
\draw[double, -] (D_pos) to[first] (DD_pos);
\draw[double, -] (DD_dir) to[last] (D_dir);
\draw[double, -] (mm_pos) to[first] (mmm_pos);
\draw (mmm_dir) to[climb] node[right] {$\cod$} (C_pos);
\draw (C_dir) to[last] node[above] {$\then$} (mm_dir);
\end{tikzpicture}
\node at ($(p1.south)!.5!(p2.north)$) {$=$};
\end{tikzpicture}
\]

Thus, on directions, the coassociative law states that given an object $i\in\Ob\cat C$ and morphisms $f\colon i\to\_, g\colon\cod f\to\_,$ and $h\colon\cod g\to\_$ in $\cat C$,

\[
(f\then g)\then h = f\then(g\then h).
\]

But this is precisely the associative law of composition in a category.

We've seen that the data and equations of polynomial comonoids correspond exactly to the data and equations of categories.
This proves <ref>.

§.§.§ Generalized duplicators as unbiased composition

Before we move onto examples, one more note about the theory: notice that both sides of our coassociative law are given by $\delta^{(3)}\colon\car{c}\to\car{c}\tripow3$, as defined in <ref>.
On directions, $\delta^{(3)}$ tells us how to compose three morphisms $i\To{f}\_\To{g}\_\To{h}\_$ in $\cat{C}$ all at once to obtain $i\To{f\:\then\:g\:\then\:h}\_$, and (co)associativity ensures this is well-defined.

In general, $\delta^{(n)}\colon\car{c}\to\car{c}\tripow{n}$ on directions tells us how to compose $n$ morphisms in $\cat{C}$ for each $n\in\nn$.
After all, we have already seen that $\delta^{(2)}=\delta$ performs binary composition, that $\delta^{(1)}=\id_\car{c}$ performs “unary” composition (the “unary composite” of a single morphism $f$ is just $f$ itself), and that $\delta^{(0)}=\epsilon$ performs “nullary” composition (the “nullary composite” at any object is just its identity).
The directions of $\car{c}\tripow{n}$ at positions in the image of $\delta^{(n)}$ are exactly the sequences of composable morphisms of length $n$, and $\delta^{(n)}$ sends each sequence to the single direction that is its composite.

§.§ Examples of categories as comonoids

Now that we know that polynomial comonoids are just categories, let's review some simple examples of categories and see how they may be interpreted as comonoids.
As we go through these examples, pay attention to how the polynomial perspective causes us to view these familiar categories somewhat differently than usual.

§.§.§ Preorders

A preorder (or thin category) is a category in which every morphism $f\colon c\to d$ is the only morphism $c\to d$.
[Sometimes these are also called posets, short for partially ordered sets, but strictly speaking the only isomorphisms in a poset are its identities, while a preorder allows objects to be isomorphic without being equal.]
Composition in preorders is easy to describe, because the composite of $c\to d$ and $d\to e$ is always just the unique arrow $c\to e$.
As such, preorders are some of the simplest examples of categories to consider—we already saw several in <ref>—so let us interpret these as comonoids first.

Let us revisit <ref>, where we first wrote down a comonoid that was not a state system.
We defined $\car{a}\coloneqq\{s\}\yon^{\{\id_s,a\}}+\{t\}\yon^{\{\id_t\}}\iso\yon^\2+\yon$ and gave it a comonoid structure, with eraser $\epsilon\colon\car{a}\to\yon$ specifying directions $\id_s$ and $\id_t$ and duplicator $\delta\colon\car{a}\to\car{a}\tri\car{a}$ pointing the direction $a$ at $t$.

Looking at the picture we drew of the comonoid in (<ref>), it should come as no surprise that the corresponding category $\cat{A}$ is the walking arrow category, which is a preorder with two objects and one morphism between them:

Here we omit the identity morphisms from our picture, but we know that they exist.

The category $\cat{A}$ has two objects, the $\car{a}$-positions $s$ and $t$.
It has two morphisms with domain $s$, the $\car{a}[s]$-directions $\id_s$ and $a$; and one morphism with domain $t$, the $\car{a}[t]$-direction $\id_t$.
The morphisms $\id_s$ and $\id_t$ picked out by the erasure are the identity morphisms, and the duplicator assigns them codomains that are equal to their domains.
The duplicator also assigns $a$ the codomain $t$; and as $\cat{A}$ is then a preorder, composites are determined automatically.

Let $(\car{c},\epsilon,\delta)$ be the comonoid corresponding to the preorder depicted as follows (identity morphisms omitted):

* What is the carrier $\car{c}$?

* Characterize the eraser $\epsilon$.

* Characterize the duplicator $\delta$.

We are given a comonoid $(\car{c},\epsilon,\delta)$ corresponding to the preorder white$B\From{f}A\To{g}C$.

* There are three morphisms with domain $A$, namely $\id_A,f,$ and $g$; the only other morphisms are the identity morphisms on $B$ and $C$.
So the carrier is $\car{c}=\{A\}\yon^{\{\id_A,f,g\}}+\{B\}\yon^{\{\id_B\}}+\{C\}\yon^{\{\id_C\}}$.

* It suffices to specify the eraser $\epsilon\colon\car{c}\to\yon$ on directions: as always, $\epsilon_i^\sharp\colon\1\to\car{c}[i]$ picks out $\id_i$ for each $i\in\car{c}(\1)=\{A,B,C\}$.

* The duplicator $\delta\colon\car{c}\to\car{c}\tri\car{c}$ tells us the codomain of each morphism, as well as how every pair of composable morphisms compose (which in the case of a preorder can be deduced automatically).
So we can completely characterize the behavior of $\delta$ using polyboxes as follows:

\[
\begin{tikzpicture}[polybox, mapstos, node distance=2ex and 1.4cm, font=\tiny]
\node (a) {
\begin{tikzpicture}
\node[poly, dom] (p) {$\id_A$\at$A$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$\id_A$\at$A$};
\node[poly, cod, above=of q] (r) {$\id_A$\at$A$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.6 of a] (b) {
\begin{tikzpicture}
\node[poly, dom] (p) {$f$\at$A$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$\id_A$\at$A$};
\node[poly, cod, above=of q] (r) {$f$\at$A$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.6of b] (c) {
\begin{tikzpicture}
\node[poly, dom] (p) {$g$\at$A$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$\id_A$\at$A$};
\node[poly, cod, above=of q] (r) {$g$\at$A$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[right=.6 of c] (d) {
\begin{tikzpicture}
\node[poly, dom] (p) {$f$\at$A$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$f$\at$A$};
\node[poly, cod, above=of q] (r) {$\id_B$\at$B$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[below=.6 of a] (e) {
\begin{tikzpicture}
\node[poly, dom] (p) {$g$\at$A$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$g$\at$A$};
\node[poly, cod, above=of q] (r) {$\id_C$\at$C$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[below=.6 of b] (f) {
\begin{tikzpicture}
\node[poly, dom] (p) {$\id_B$\at$B$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$\id_B$\at$B$};
\node[poly, cod, above=of q] (r) {$\id_B$\at$B$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\node[below=.6 of c] (g) {
\begin{tikzpicture}
\node[poly, dom] (p) {$\id_C$\at$C$};
\node[poly, cod, right=of p.south, yshift=-1ex] (q) {$\id_C$\at$C$};
\node[poly, cod, above=of q] (r) {$\id_C$\at$C$};
\draw[double, -] (p_pos) to[first] (q_pos);
\draw (q_dir) to[climb] (r_pos);
\draw (r_dir) to[last] (p_dir);
\end{tikzpicture}
\end{tikzpicture}
\]

We showed in <ref> that for any set $B$, the linear polynomial $B\yon$ has a unique comonoid structure.
To what category does this comonoid correspond?

The linear polynomial $B\yon$ corresponds to a category whose objects form the set $B$ and whose only morphisms are identities: in other words, it is the discrete category on $B$.

* Find a comonoid structure for the polynomial $p\coloneqq{\yon}^{\ord{n}+\1}+\ord{n}\yon$ whose corresponding category is a preorder.
(It is enough to fully describe the category that it corresponds to.)

* Would you call your category “star-shaped”?

* The polynomial $p\coloneqq{\yon}^{\ord{n}+\1}+\ord{n}\yon$ has $n+1$ positions: $1$ with $n+1$ directions and the rest with $1$ direction each.
So any category carried by $p$ has $n+1$ objects, of which only $1$ has any nonidentity morphisms coming out of it: in fact, it has $n$ nonidentity morphisms coming out of it.
But if the category is to be a preorder, each of these $n$ nonidentity morphisms must have a distinct codomain.
As there are exactly $n$ other objects, this completely characterizes the category.
Equivalently, it is the discrete category on $\ord{n}$ adjoined with a unique initial object, so that the only nonidentity morphisms are the morphisms out of that initial object to each of the other objects exactly once.

* This category can be thought of as “star-shaped” if we picture the initial object in the center with morphisms leading out to the other $n$ objects like spokes.

[State systems as categories]
We know that every state system $\car{s}\iso S\yon^S$ with its do-nothing section $\epsilon\colon\car{s}\to\yon$ and its transition lens $\delta\colon\car{s}\to\car{s}\tri\car{s}$ is a comonoid, so what category $\cat{S}$ does $(\car{s},\epsilon,\delta)$ correspond to?

Recall from <ref> that state systems are exactly those comonoids whose codomain (i.e. “target”) functions $\cod\colon\car{s}[s]\to\car{s}(\1)$ for $s\in\car{s}(\1)$ are bijections.
That is, from every object $s\in\Ob\cat S=\car{s}(\1)$, there is exactly $1$ morphism to every object $t\in\Ob\cat S$.
So not only is $\cat S$ a preorder, it is the codiscrete preorder on $\car{s}(\1)$, where there is always a morphism between every pair of objects.

Let's redraw the polyboxes for the do-nothing section of $\car{s}$ from (<ref>) and the transition lens of $\car{s}$ from (<ref>), this time with our new arrow labels, as a sanity check:

\[
\begin{tikzpicture}
\node (erase) {

\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (S) {$\id_s$\at$s$};

\draw (S_pos) to[climb'] node[right] {$\idy$} (S_dir);
\end{tikzpicture}

\node[right=of erase] (dupl) {

\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (r) {$s_0\to s_2$\at$s_0$};
\node[poly, cod, right=2 of r.south, yshift=-2.5ex, "$\car{s}$" right] (p) {$s_0\to s_1$\at$s_0$};
\node[poly, cod, above=.8 of p, "$\car{s}$" right] (p') {$s_1\to s_2$\at$s_1$};

\draw[double, -] (r_pos) to[first] node[below] {} (p_pos);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above] {$\then$} (r_dir);
\end{tikzpicture}

\end{tikzpicture}
\]

Indeed, we had already been writing the directions of $\car{s}$ as arrows $s\to t$, knowing that each was uniquely specified by its source $s$ and its target $t$ in $\car{s}(\1)$.
And in <ref>, we had already noted that $\id_s$ was just the arrow $s\to s$.
So state systems have been categories with exactly one morphism between every pair of objects all along.

Other names for this category include the indiscrete preorder and the codiscrete or indiscrete category.
These names highlight the fact that every object of this category is isomorphic to every other object: in fact, every arrow $s\to t$ is an isomorphism with inverse $t\to s$, for these compose as $\id_s\colon s\to s$ in one direction and $\id_t\colon t\to t$ in the other.
Thus this category is also a groupoid, and it may be called the codiscrete, indiscrete, or contractible groupoid…but we will call it the state category on $S$, where $S$ is the set of positions of $\car{s}$ or objects of $\cat S$.

Here are the state categories on $\3$ and on $\1\5$, with all maps (even identities) drawn:

\[
\begin{tikzpicture}
\def\n{3}% how many nodes
\def\size{2cm}
\node[circle,minimum size=\size] (b) {};
\foreach\x in{1,...,\n}{
\node[minimum size=0.75cm,draw,circle] (n-\x) at (b.{360/\n*\x}){\x};
\foreach\x in{1,...,\n}{
\foreach\y in{1,...,\n}{
\ifnum\x=\y\draw[->] (n-\x) to [in=360/\n*\x-15,out=360/\n*\x+15,loop] ();\relax\else
\draw (n-\x) edge[->,bend right=10] (n-\y);
\fi
\def\n{15}% how many nodes
\def\size{4cm}
\node[circle,minimum size=\size, right=4 of b] (b) {};
\foreach\x in{1,...,\n}{
\node[minimum size=0.75cm,draw,circle] (n-\x) at (b.{360/\n*\x}){\x};
\foreach\x in{1,...,\n}{
\foreach\y in{1,...,\n}{
\ifnum\x=\y\draw[->] (n-\x) to [in=360/\n*\x-15,out=360/\n*\x+15,loop] ();\relax\else
\draw (n-\x) edge[->,bend right=3] (n-\y);
\fi
% Source: Asterix: https://tex.stackexchange.com/questions/390647/understanding-complete-graph-example-in-tikz
\end{tikzpicture}
\]

The picture on the left should look familiar: it's what we drew in <ref> when took the corolla picture for $\3\yon^\3$ and bent the arrows to point at their targets according to its transition lens.
Notice that the graphs we obtain in this way are always complete.

Let $S$ be a set. Is there any comonoid structure on $S\yon^S$ other than that of the state category?

In the case of $S\coloneqq\0$, the only comonoid structure on $S\yon^S\iso\0$ is given by the empty category, the only category with no objects; and in the case of $S\coloneqq\1$, the only comonoid structure on $S\yon^S\iso\yon$ is given by the category with $1$ object and no nonidentity morphisms, again the only such category.
So in those cases, the comonoid structure on $S\yon^S$ is unique.

Now assume $|S|\geq2$.
The state category is always connected, but we can always find a comonoid structure on $S\yon^S$ given by a category that is not connected—and thus not isomorphic to the state category—as follows.
Consider a category whose object set is $S$ that has no morphisms between distinct objects, so that it is certainly not connected.
Then to specify the category, it suffices to specify a monoid associated with each object that will give the morphisms whose domain and codomain are equal to that object.
But there is always a monoid structure on a given set $S$.