Here is $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$ drawn in polyboxes, where we continue to denote the stage-$n$ pretree of a $p$-tree by $\pi^{(n)}T$:

\begin{equation} \label{eqn.eps_n_polybox}
\begin{tikzpicture}
\node (f) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" below] (p) {$v$\at$T$};
\node[left=0pt of p_pos] {$\tr_p$};
\node[left=0pt of p_dir] {$\vtx(-)$};

\node[poly, cod, right=of p, "$p\tripow{n}$" below] (q) {$v$\at$\pi^{(n)}T$};
\node[right=0pt of q_pos] {$p\tripow{n}(\1)$};
\node[right=0pt of q_dir] {$\vtx_n(-)$};

\draw (p_pos) -- node[below] {} (q_pos);
\draw (q_dir) -- node[above] {} (p_dir);
\end{tikzpicture}
\end{tikzpicture}
\end{equation}

On the right hand side, $v$ is a height-$n$ leaf of $\pi^{(n)}T$; on the left, $v$ is identified with the corresponding height-$n$ vertex of $T$.

This isn't the only way we can write this lens in polyboxes, however; polyboxes have special notation for lenses to composites, allowing us to write, say, the $n=4$ case like so:

\begin{equation} \label{eqn.eps_1_1_1_1_polybox}
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (p) {$a_1\leadsto a_2\leadsto a_3\leadsto a_4$\at$T$};
\foreach \i/\j in {1/0,2/1,3/2,4/3}
\node[poly, cod, "$p$" right] (q\i) at (4,1.3*\i-3.25) {$a_\i$\at$i_\j$};
\draw (p_pos) to[first] node[below] {} (q1_pos.west);
\foreach \i/\j in {1/2,2/3,3/4}
\draw
node[left] {}
\draw (q4_dir) to[last] node[above left] {} (p_dir);
\end{tikzpicture}
\end{equation}

Here we are unpacking the construction of the first $4$ levels of $T$, according to our nested instructions for building $p$-trees.
The $p$-position $i_0$ is the label on the root of $T$, while the $p[i_0]$-direction $a_1$ specifies one of the edges coming out of it—leading to a height-$1$ vertex of $T$ labeled $i_1$, and so on.

The contents of the position-boxes and the arrows going up on the codomain side carry all the data of the bottom $4$ levels of $T$: namely the label $i_0$ of the root, the label $i_1$ of the vertex at the end of every direction $a_1$ out of the root, and so on until $i_3$.
All this specifies a unique $p\tripow4$-position, a $p\tripow4$-pretree, which is the same as the $p\tripow4$-pretree $T$.
Indeed, we can think of $\pi^{(4)}T$ as a shorthand for the gadget comprised of the $4$ polyboxes on the right hand side of (<ref>) when their blue boxes are yet to be filled.
So the position and direction depicted on the codomain side of (<ref>) is equivalent to the position and direction depicted on the codomain side of (<ref>).
This generalizes to all values of $n$. The direction $a_4$ emanating from $i_3$, together with all the data below it, corresponds to the rooted path we've denoted $a_1\leadsto a_2\leadsto a_3\leadsto a_4$ in $T$.

There are even more ways to express $\epsilon^{(4)}_p\colon\car{t}_p\to p\tripow4$ in polyboxes, however.
After all, $p\tripow4\iso p\tripow2\tri p\tripow2$.
So we ought to be able to draw $\epsilon^{(4)}_p$ as follows:

\begin{equation} \label{eqn.eps_2_2_polybox_empty}
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$\car{t}_p$" left] (r) {};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow2$" right] (q) {};
\node[poly, cod, above=of q, "$p\tripow2$" right] (q') {};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\end{equation}

Let's think about how we should fill these boxes.
We can still put a $p$-tree $T$ in the lower left position box.
From the commutativity of (<ref>), we know the on-positions function $\pi^{(4)}$ of $\epsilon^{(4)}_p$ factors through the on-positions function $\pi^{(2)}$ of $\epsilon^{(2)}_p$, which tells us that $p\tripow2$-pretree that should go in the lower right position box should be $\pi^{(2)}T$: the $p\tripow2$-pretree of $T$.

Another way to think about this is that the polyboxes for the lower $p\tripow2$ on the right side of (<ref>) are equivalent to the polyboxes for the $2$ lower copies of $p$ on the right side of (<ref>)—just like how the polyboxes for $p\tripow{n}$ in (<ref>) are equivalent to the polyboxes for all $n=4$ copies of $p$ in (<ref>).
There, the position could be represented with a single $p\tripow{n}$-pretree $\pi^{(n)}T$, and the direction $(a_1,\ldots,a_n)$ is one of its length-$n$ rooted paths.
So here, too, we can package the $2$ lower copies of $p$ into a single pair of polyboxes for $p\tripow2$, if we let $u$ be the height-$2$ vertex of $T$ at the end of the rooted path $(a_1,a_2)$:

\begin{equation} \label{eqn.eps_2_2_polybox_partly}
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {\at$T$};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow2$" right] (q) {$u$\at$\pi^{(2)}T$};
\node[poly, cod, above=of q, "$p\tripow2$" right] (q') {};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\end{equation}

But then the polyboxes for the $2$ upper copies of $p$ from (<ref>) should also collapse down to a single pair of polyboxes for $p\tripow2$, with a $p\tripow2$-pretree as its position and a height-$2$ leaf of that pretree as its direction.
Indeed, once we have followed the directions $(a_1,a_2)$ up to the height-$2$ vertex $u$, the subtree of $T$ rooted at $u$ is itself a $p$-tree: it has a label $i_2$ on its root, out of which we can follow the direction $a_3$ to reach a height-$1$ vertex labeled $i_3$, then follow the direction $a_4$ to reach a height-$2$ vertex that we call $w$.
Of course, the vertex labeled $i_3$ is actually a height-$3$ vertex of the whole tree $T$; likewise $w$ corresponds to a height-$4$ vertex of $T$.
However, from the perspective of the upper copy of $p\tripow2$ in (<ref>), we are starting over from $u$ and moving up the subtree of $T$ rooted at $u$—or, more precisely, the $p\tripow2$-pretree of the subtree rooted at $u$.
So the polyboxes end up looking like this:

\begin{equation} \label{eqn.eps_2_2_polybox}
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {$u\leadsto w$\at$T$};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow2$" right] (q) {$u$\at$\pi^{(2)}T$};
\node[poly, cod, above=of q, "$p\tripow2$" right] (q') {$w$\at$\pi^{(2)}T(u)$};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\end{equation}

Here $T(u)$ denotes the $p$-tree equal to the subtree of $T$ rooted at its vertex $u$, and $w$ is one of $T(u)$'s height-$2$ vertices.
When viewed as the subtree of $T$ rooted at its the height-$2$ vertex $u$, the $p$-tree $T(u)$ has its height-$2$ vertex $w$ identified with a height-$4$ vertex of $T$, a descendent of $u$ that we denote by $u\leadsto w$.
Alternatively, $u$ corresponds to the rooted path $(a_1,a_2)$ of $T$, while $w$ corresponds to the rooted path $(a_3,a_4)$ of $T(u)$, so $u\leadsto w$ corresponds to the concatenated rooted path $(a_1,a_2,a_3,a_4)$ of $T$.
As concatenation is associative, $\leadsto$ is associative as well.

Both the notation $T(u)$, for what we will call the $p$-subtree of the $p$-tree $T$ rooted at $u\in\vtx(T)$, and the notation $u\leadsto w$, for the vertex in $\vtx(T)$ that $w\in\vtx(T(u))$ coincides with when $T(u)$ is identified with the subtree of $p$ rooted at $u$, will turn out to be temporary—we will soon justify why we can express these concepts in much more familiar terms.
As a reminder, due to the definition of a $p$-tree $T$, a $p$-subtree of $T$ is still itself a $p$-tree, whereas the $p\tripow{n}$-pretree of $T$ is not a $p$-tree unless the height of $T$ is strictly less than $n$.
As a sneak preview, they will be crucial to defining the categorical structure of the cofree comonoid on $p$.

Here are three more ways to depict $\epsilon^{(4)}_p$, viewing its codomain in turn as $p\tripow3\tri p\tripow1$, as $p\tripow1\tri p\tripow2\tri p\tripow1$, or as $p\tripow1\tri p\tripow1\tri p\tripow1\tri p\tripow1$:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {$r\leadsto t$\at$T$};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow3$" right] (q) {$r$\at$\pi^{(3)}T$};
\node[poly, cod, above=of q, "$p\tripow1$" right] (q') {$t$\at$\pi^{(1)}T(r)$};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\node[right=1.5 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (S) {$x\leadsto s\leadsto t$\at$T$};
\node[poly, cod, right=of S, "$p\tripow2$" right] (S2) {$s$\at$\pi^{(2)}T(x)$};
\node[poly, cod, below=of S2, "$p\tripow1$" right] (S1) {$x$\at$\pi^{(1)}T$};
\node[poly, cod, above=of S2, "$p\tripow1$" right] (S3) {$t$\at$\pi^{(1)}T(x\leadsto s)$};
\draw (S_pos) to[first] (S1_pos);
\draw (S1_dir) to[climb] (S2_pos);
\draw (S2_dir) to[climb] (S3_pos);
\draw (S3_dir) to[last] (S_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$=\qquad\car{t}_p$" left] (p) {$x\leadsto y\leadsto z\leadsto t$\at$T$};
\node[poly, cod, "$p\tripow1$" right] (q1) at (4,1.5*1-3.25) {$x$\at$\pi^{(1)}T$};
\node[poly, cod, "$p\tripow1$" right] (q2) at (4,1.5*2-3.25) {$y$\at$\pi^{(1)}T(x)$};
\node[poly, cod, "$p\tripow1$" right] (q3) at (4,1.5*3-3.25) {$z$\at$\pi^{(1)}T(x\leadsto y)$};
\node[poly, cod, "$p\tripow1$" right] (q4) at (4,1.5*4-3.25) {$t$\at$\pi^{(1)}T(x\leadsto y\leadsto z)$};

\draw (p_pos) to[first] node[below] {} (q1_pos.west);
\foreach \i/\j in {1/2,2/3,3/4}
\draw
node[left] {}
\draw (q4_dir) to[last] node[above left] {} (p_dir);
\end{tikzpicture}
\]

Here $r=x\leadsto s$ and $s=y\leadsto z$.
Notice that the last depiction is just another way to write (<ref>), with each $p\tripow1$-pretree in place of the $p$-position that labels its root and height-$1$ vertices in place of their corresponding directions, which are just length-$1$ rooted paths.

Finally, all this could be generalized to other values of $n$.
Here are different ways to draw polyboxes for $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$, viewing its codomain as $p\tripow\ell\tri p\tripow{m}$ with $n=\ell+m$ or $p\tripow{i}\tri p\tripow{j}\tri p\tripow{k}$ with $n=i+j+k$:

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {$u\leadsto w$\at$T$};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow\ell$" right] (q) {$u$\at$\pi^{(\ell)}T$};
\node[poly, cod, above=of q, "$p\tripow{m}$" right] (q') {$w$\at$\pi^{(m)}T(u)$};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\node[right=1.5 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (S) {$x\leadsto s\leadsto t$\at$T$};
\node[poly, cod, right=of S, "$p\tripow{j}$" right] (S2) {$s$\at$\pi^{(j)}T(x)$};
\node[poly, cod, below=of S2, "$p\tripow{i}$" right] (S1) {$x$\at$\pi^{(i)}T$};
\node[poly, cod, above=of S2, "$p\tripow{k}$" right] (S3) {$t$\at$\pi^{(k)}T(x\leadsto s)$};
\draw (S_pos) to[first] (S1_pos);
\draw (S1_dir) to[climb] (S2_pos);
\draw (S2_dir) to[climb] (S3_pos);
\draw (S3_dir) to[last] (S_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

§.§ Cofree comonoids as categories

We have now characterized the carrier $\car{t}_p$ of the comonoid $\cofree{p}$ that will turn out to be cofree on $p$; but we have yet to describe the comonoid structure of $\cofree{p}$ that $\car{t}_p$ carries.
This structure will allow us to interpret $\cofree{p}$ as a category, whose objects will be $p$-trees and whose morphisms will be the vertices of each $p$-tree.
We could go ahead and describe this category right now, but as category theorists, let us show that the eraser and duplicator of $\cofree{p}$, as well as the comonoid laws that they satisfy, arise naturally from our construction of $\car{t}_p$ as the limit of (<ref>).

§.§.§ The eraser of the cofree comonoid

The eraser for a comonoid $\cofree{p}$ carried by $\car{t}_p$ should be a lens of the form $\car{t}_p\to\yon$.
Conveniently, since $\yon$ appears in (<ref>), its limit $\car{t}_p$ is already equipped with a canonical lens $\epsilon_p\colon\car{t}_p\to\yon$, as seen in (<ref>).
This lens will turn out to be the eraser of the cofree comonoid on $p$.

The eraser picks out a direction at each position of the carrier to be the identity morphism on that object.
As each $\car{t}_p$-position is a tree $T\in\tr_p$, and each $\car{t}_p[T]$-direction is a vertex of $T$, the eraser $\epsilon_p$ should pick out a single vertex of every $p$-tree.
Even without looking at (<ref>), you may already have your suspicions as to which vertex this will turn out to be, as there is, after all, only one sensible way to choose a canonical vertex that every $p$-tree is guaranteed to have: choose its root.
Indeed, <ref> tells us that $\epsilon_p\colon\car{t}_p\to\yon$ sends each $p$-tree $T\in\tr_p$ to its stage-$0$ pretree on positions, stripping away everything except for the single unlabeled root of $T$; then on-directions, $\epsilon_p$ picks out the unique height-$0$ vertex of $T$ in $\vtx_0(T)\ss\vtx(T)$, which is just its root.

So in the category $\cofree{p}$, where morphisms out of objects are vertices of trees, the identity morphism on a tree is its root—in fact, we will henceforth denote the root of a $p$-tree by $\id_T$ (so that $\vtx_0(T)=\{\id_T\}$).
Equivalently, we can identify $\id_T$ with the unique length-$0$ rooted path of $T$: the empty rooted path, which starts and ends at the root.
The rest of the categorical structure of $\cofree{p}$ will be determined by its duplicator.

§.§.§ The duplicator of the cofree comonoid

The duplicator for a comonoid $\cofree{p}$ carried by $\car{t}_p$ should be a lens $\delta_p\colon\car{t}_p\to\car{t}_p\tri\car{t}_p$.
But before we can specify such a lens, we need to figure out what kind of polynomial $\car{t}_p\tri\car{t}_p$ is.

Here is where our work from <ref> comes in handy: since the diagram in (<ref>) is connected, its limit $\car{t}_p$ is a connected limit, and we showed in <ref> that $\tri$ preserves connected limits.
Therefore $\car{t}_p\tri\car{t}_p$ is itself the limit of some diagram, and a morphism to $\car{t}_p\tri\car{t}_p$ is just a cone over that diagram.

Which diagram is it?
First, we can use the fact that $\tri$ preserves connected limits on the left to expand $\car{t}_p\tri\car{t}_p$ as the limit of the following diagram, where we have applied the functor $-\tri\car{t}_p$ to the diagram from (<ref>):

\[
\begin{tikzcd}
\yon\tri\car{t}_p \ar[d] &
p\tri\car{t}_p \ar[d] &
p\tripow2\tri\car{t}_p \ar[d] &
p\tripow3\tri\car{t}_p \ar[d] &
\cdots\\
\1\tri\car{t}_p &
p\tri\1\tri\car{t}_p \ar[l] &
p\tripow2\tri\1\tri\car{t}_p \ar[l] &
p\tripow3\tri\1\tri\car{t}_p \ar[l] &
\cdots.\ar[l]
\end{tikzcd}
\]

But we have $p\tripow{n}\tri\1\tri\car{t}_p\iso p\tripow{n}\tri\1$, so we can simplify this diagram like so:

\begin{equation} \label{eqn.cofree_tri2_lim_expand_left}
\begin{tikzcd}
\yon\tri\car{t}_p \ar[d] &
p\tri\car{t}_p \ar[d] &
p\tripow2\tri\car{t}_p \ar[d] &
[10pt] p\tripow3\tri\car{t}_p \ar[d] &
\cdots\\
\1 &
p\tri\1 \ar[l] &
p\tripow2\tri\1 \ar[l] &
p\tripow3\tri\1 \ar[l] &
\cdots.\ar[l]
\end{tikzcd}
\end{equation}

(This works because according to <ref>, $\tri$ actually preserves all limits on the left—including the terminal object $\1$.)
So $\car{t}_p\tri\car{t}_p$ is the limit of (<ref>).

Then we use the fact that $\tri$ preserves connected limits on the right to expand each $p\tripow\ell\tri\car{t}_p$ in (<ref>) as the limit of the following:

\begin{equation} \label{eqn.cofree_tri2_lim_expand_right}
\begin{tikzcd}
p\tripow\ell\tri\yon \ar[d] &
p\tripow\ell\tri p \ar[d] &
p\tripow\ell\tri p\tripow2 \ar[d] & p\tripow\ell\tri p\tripow3 \ar[d] &
\cdots\\
p\tripow\ell\tri\1 &
p\tripow\ell\tri p\tri\1 \ar[l] &
p\tripow\ell\tri p\tripow2\tri\1 \ar[l] &
p\tripow\ell\tri p\tripow3\tri\1 \ar[l] &
\cdots.\ar[l]
\end{tikzcd}
\end{equation}

So the limit of (<ref>) is the limit of a larger diagram, where we have “plugged in” a copy of (<ref>) in place of each $p\tripow\ell\tri\car{t}_p$ that appears.

It's worth being a little careful, though, when we draw this diagram: each $p\tripow\ell\tri\car{t}_p$ in (<ref>) appears with a lens to $p\tripow\ell\tri\1$, and we need to work out what arrow should go in its place.
The lens in question is given by applying $p\tripow\ell\tri-$ to the unique lens $\car{t}_p\to\1$.
But $\1$ actually shows up in the lower left corner of (<ref>), so the unique lens $\car{t}_p\to\1$ is just the projection from the limit of (<ref>) to that $\1$.
Then once we apply the connected limit-preserving functor $p\tripow\ell\tri-$ to (<ref>), yielding (<ref>), we obtain the lens $p\tripow\ell\tri\car{t}_p\to p\tripow\ell\tri\1$ we desire as the projection from the limit of (<ref>) to the $p\tripow\ell\tri\1$ in the lower left corner.
So if we want to replace each $p\tripow\ell\tri\car{t}_p$ in (<ref>) with a copy of (<ref>), without changing the limit of the whole diagram, we should replace the arrow $p\tripow\ell\tri\car{t}_p\to p\tripow\ell\tri\1$ with an identity arrow from the $p\tripow\ell\tri\1$ in the lower left corner of (<ref>) to the $p\tripow\ell\tri\1$ in (<ref>).
Of course, we can then collapse these identity arrows down without changing the limit, so the diagram we are left with should look like this:

\begin{equation} \label{eqn.cofree_tri2_diagram}
\begin{tikzcd}[row sep=small, column sep=tiny]
p\tripow3 \ar[rd] && p\tripow3\tri p \ar[rd] && p\tripow3\tri p\tripow2 \ar[rd] && \cdots \\
& p\tripow3\tri\1 \ar[dd] && p\tripow3\tri p\tri1 \ar[dd] && p\tripow3\tri p\tripow2\tri\1 \ar[dd] && \cdots \\
p\tripow2 \ar[rd] && p\tripow2\tri p \ar[rd] && p\tripow2\tri p\tripow2 \ar[rd] && \cdots \\
& p\tripow2\tri\1 \ar[dd] && p\tripow2\tri p\tri1 \ar[dd] && p\tripow2\tri p\tripow2\tri\1 \ar[dd] && \cdots \\
p \ar[rd] && p\tri p \ar[rd] && p\tri p\tripow2 \ar[rd] && \cdots \\
& p\tri\1 \ar[dd] && p\tri p\tri1 \ar[dd] && p\tri p\tripow2\tri\1 \ar[dd] && \cdots \\
\yon \ar[rd] && p \ar[rd] && p\tripow2 \ar[rd] && \cdots \\
& \1 && p\tri\1 \ar[ll] && p\tripow2\tri\1 \ar[ll] && \cdots.\ar[ll]
\end{tikzcd}
\end{equation}

Here the bottom row of (<ref>) is still the bottom row of (<ref>), but in the place of each $p\tripow\ell\tri\car{t}_p$ in the top row, we have grafted in a copy of (<ref>).
Yet the limit of the diagram is preserved: the limit of (<ref>) is still $\car{t}_p\tri\car{t}_p$.
In summary, for purely formal reasons, <ref> ensure that since the limit of (<ref>) is $\car{t}_p$, the limit of (<ref>) is $\car{t}_p\tri\car{t}_p$.

While (<ref>) has become rather unwieldy to draw, it is easy to characterize: it is a diagram with a copy each of

\[
p\tripow\ell\tri p\tripow{m} \qqand p\tripow\ell\tri p\tripow{m}\tri\1
\]

for every $\ell,m\in\nn$, with arrows

\begin{equation} \label{eqn.cofree_tri2_diagram_arr_diag}
p\tripow\ell\tri p\tripow{m}\to p\tripow\ell\tri p\tripow{m}\tri\1
\end{equation}

between them; along with arrows

\begin{equation} \label{eqn.cofree_tri2_diagram_arr_vert}
p\tripow\ell\tri p\tripow{(m+1)}\tri\1\to p\tripow\ell\tri p\tripow{m}\tri\1,
\end{equation}

drawn vertically in (<ref>); and

\begin{equation} \label{eqn.cofree_tri2_diagram_arr_horiz}
p\tripow{\ell+1}\tri p\tripow0\tri\1\iso p\tripow{\ell+1}\tri\1\to p\tripow\ell\tri\1\iso p\tripow\ell\tri p\tripow0\tri\1,
\end{equation}

drawn horizontally in (<ref>) along the bottom row.
Of course, we could write each $p\tripow\ell\tri p\tripow{m}$ as $p\tripow{(\ell+m)}$, but the notation $p\tripow\ell\tri p\tripow{m}$ helps us distinguish it as the object appearing $\ell$ rows above the bottom and $m$ columns to the right in (<ref>), in contrast with any other $p\tripow{\ell'}\tri p\tripow{m'}$ with $(\ell,m)\neq(\ell',m')$, even if $\ell+m=\ell'+m'$ guarantees that there are isomorphisms between these objects.

Nevertheless, it is these isomorphisms that induce a canonical lens $\car{t}_p\to\car{t}_p\tri\car{t}_p$, by giving a map from the diagram (<ref>) to the diagram (<ref>) as follows.
For all $\ell,m,n\in\nn$ with $n=\ell+m$, we have a canonical isomorphism $p\tripow{n}\To\iso p\tripow\ell\tri p\tripow{m}$ sending the $p\tripow{n}$ that appears in (<ref>) to the $p\tripow\ell\tri p\tripow{m}$ that appears in (<ref>), and similarly sending $p\tripow{n}\tri\1$ in (<ref>) to $p\tripow\ell\tri p\tripow{m}\tri\1$ in (<ref>).
Then all the arrows that appear in (<ref>)—i.e. all the arrows in (<ref>), (<ref>), and (<ref>)—can be identified with arrows that appear in (<ref>), so everything commutes.
We therefore induce a lens from the limit $\car{t}_p$ of (<ref>) to the limit $\car{t}_p\tri\car{t}_p$ of (<ref>), which we call $\delta_p\colon\car{t}_p\to\car{t}_p\tri\car{t}_p$.
This turns out to be the duplicator of $\cofree{p}$.

How does $\delta_p$ behave in terms of $p$-trees?
First, we characterize $\car{t}_p\tri\car{t}_p$ and its projections to each $p\tripow\ell\tri p\tripow{m}$ in (<ref>).
Concretely, we know that a $\car{t}_p\tri\car{t}_p$-position is just a $p$-tree $T\in\tr_p$ along with a $p$-tree $U(v)\in\tr_p$ associated with every vertex $v\in\vtx(T)$.
Then a direction at that position is a choice of vertex $v\in\vtx(T)$ and another vertex $w\in\vtx(U(v))$ of the $p$-tree $U(v)$ associated with $v$.
Each projection from $\car{t}_p\tri\car{t}_p$ to $p\tripow\ell\tri p\tripow{m}$ in (<ref>) is then the composition product of the projections $\epsilon^{(\ell)}_p\colon\car{t}_p\to p\tripow\ell$ and $\epsilon^{(m)}_p\colon\car{t}_p\to p\tripow{m}$, which by <ref> we can draw in polyboxes like so:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" below] (p) {$v$\at$T$};
\node[left=0pt of p_pos] {$\tr_p$};
\node[left=0pt of p_dir] {$\vtx(-)$};
\node[poly, dom, above=.8 of p, "$\car{t}_p$" above] (p') {$w$\at$U_v$};
\node[left=0pt of p'_pos] {$\tr_p$};
\node[left=0pt of p'_dir] {$\vtx(-)$};

\node[poly, cod, right=of p, "$p\tripow\ell$" below] (q) {$v$\at$\pi^{(\ell)}T$};
\node[right=0pt of q_pos] {$p\tripow\ell(\1)$};
\node[right=0pt of q_dir] {$\vtx_\ell(-)$};
\node[poly, cod, above=.8 of q, "$p\tripow{m}$" above] (q') {$w$\at$\pi^{(m)}U_v$};
\node[right=0pt of q'_pos] {$p\tripow{m}(\1)$};
\node[right=0pt of q'_dir] {$\vtx_m(-)$};

\draw (p_pos) -- node[below] {} (q_pos);
\draw (q_dir) -- node[above] {} (p_dir);
\draw (p'_pos) -- node[below] {} (q'_pos);
\draw (q'_dir) -- node[above] {} (p'_dir);
\end{tikzpicture}
\]

On positions, $\epsilon^{(\ell)}_p\tri\epsilon^{(m)}_p$ sends the $p$-tree $T$ to its stage-$\ell$ pretree $\pi^{(\ell)}T$, and it sends each $p$-tree $U_v$ associated to a height-$\ell$ vertex $v\in\vtx_\ell(T)$ to its stage-$m$ pretree $\pi^{(m)}U_v$, to be $p\tripow{m}$-pretree associated with the height-$\ell$ leaf $v$ of $\pi^{(m)}T$.
Equivalently, this specifies a $p\tripow{(\ell+m)}$-pretree on the right: its bottom $\ell$ levels coincide with the bottom $\ell$ levels of $T$, and its top $m$ levels coincide with the bottom $m$ levels of the $U_v$'s for $v\in\vtx_\ell(T)$.
Then on directions, $\epsilon^{(\ell)}_p\tri\epsilon^{(m)}_p$ is the canonical inclusion of vertices $\vtx_\ell(T)\inj\vtx(T)$ sending $v\mapsto v$, followed by the canonical inclusion of vertices $\vtx_m(U_v)\inj\vtx(U_v)$.
These lenses comprise the universal cone over (<ref>).

Meanwhile, the other cone we formed over (<ref>) is comprised of lenses of the form $\epsilon^{(\ell+m)}_p\colon\car{t}_p\to p\tripow{(\ell+m)}\iso p\tripow\ell\tri p\tripow{m}$, each of which should factor through $\car{t}_p\tri\car{t}_p$, as depicted in the following commutative diagram:

\begin{equation} \label{eqn.delta_p_tri_epsilons}
\begin{tikzcd}[row sep=large]
\car{t}_p \ar[r,dashed,"\delta_p"] \ar[dr,"\epsilon^{(\ell+m)}_p"'] & \car{t}_p\tri\car{t}_p \ar[d,"\epsilon^{(\ell)}_p\:\tri\:\epsilon^{(m)}_p"] \\
& p\tripow{\ell}\tri p\tripow{m}.
\end{tikzcd}
\end{equation}

Indeed, by the universal property of $\car{t}_p\tri\car{t}_p$, our $\delta_p$ is the unique lens for which the above diagram commutes for all $\ell,m\in\nn$.
We will use the equation given by the commutativity of (<ref>) repeatedly in what follows, whenever we work with $\delta_p$.

Expressing (<ref>) as an equation of polyboxes, using our usual labels for the arrows of the duplicator $\delta_p$ on the left and our depiction of the projection $\epsilon^{(\ell+m)}_p\colon\car{t}_p\to p\tripow\ell\tri p\tripow{m}$ from <ref> on the right, we have

\[
\begin{tikzpicture}
\node (1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {$v\then w$\at$T$};
\node[poly, right=1.8 of r.south, yshift=-2.5ex, "$\car{t}_p$" below] (p) {$v$\at$T$};
\node[poly, above=.8 of p, "$\car{t}_p$" above] (p') {$w$\at$\cod v$};
\node[poly, cod, right=of p, "$p\tripow\ell$" right] (q) {$v$\at$\pi^{(\ell)}T$};
\node[poly, cod, above=.75 of q, "$p\tripow{m}$" right] (q') {$w$\at$\pi^{(m)}(\cod v)$};

\draw (p_pos) -- node[below] {} (q_pos);
\draw (q_dir) -- node[above] {} (p_dir);
\draw (p'_pos) -- node[below] {} (q'_pos);
\draw (q'_dir) -- node[above] {} (p'_dir);
\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}
\node[right=1.8 of 1] (2) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{t}_p$" left] (r) {$v\leadsto w$\at$T$};
\node[poly, cod, right=1.8 of r.south, yshift=-1ex, "$p\tripow\ell$" right] (q) {$v$\at$\pi^{(\ell)}T$};
\node[poly, cod, above=of q, "$p\tripow{m}$" right] (q') {$w$\at$\pi^{(m)}T(v)$};

\draw (r_pos) to[first] node[below] {} (q_pos);
\draw (q_dir) to[climb] node[right] {} (q'_pos);
\draw (q'_dir) to[last] node[above] {} (r_dir);
\end{tikzpicture}
\node at ($(1.east)!.5!(2.west)$) {=};
\end{tikzpicture}
\]

Recall from <ref> that $T(v)$ denotes the $p$-tree equal to the subtree of $T$ rooted at $v\in\vtx(T)$, while $v\leadsto w\in\vtx(T)$ for $w\in\vtx(T(v))$ is the descendent of $v$ that coincides with $w$ when $T(v)$ is identified with the subtree of $T$ rooted at $v$.
Equivalently, we can identify $v\in\vtx(T)$ with the rooted path in $T$ that ends at the vertex $v$ and $w\in\vtx(T(v))$ with the rooted path of $T(v)$ that ends at the vertex $w$, so $v\leadsto w$ becomes the rooted path in $T$ obtained by concatenating $v$ and $w$.
Then for this equality to hold over all $\ell,m\in\nn$, we want $\cod v\coloneqq T(v)$ and $v\then w\coloneqq v\leadsto w$; in fact, $\cod v$ and $v\then w$ will henceforth be our preferred notation for $T(v)$ and $v\leadsto w$.

§.§.§ Verifying the comonoid laws

Putting together our constructions of the carrier, the eraser, and the duplicator of the $\cofree{p}$ yields the following result.

As defined above, $\left(\car{t}_p,\epsilon_p,\delta_p\right)$ is a polynomial comonoid corresponding to a category $\cofree{p}$ characterized as follows.

* An object in $\cofree{p}$ is a $p$-tree in $T\in\tr_p$.

* A morphism emanating from $T$ is a rooted path in $T$; its codomain is the $p$-subtree rooted at the end of the path.

* The identity morphism on $T$ is its empty empty rooted path:

* Composition is given by concatenating rooted paths: given a rooted path $v$ in $T$ and a rooted path $w$ in $\cod v$, the $p$-subtree rooted at the end of $v$, we identify $w$ with the corresponding path in $T$ that starts where $v$ ends, then concatenate the two paths in $T$ to obtain the composite morphism $v\then w$, another rooted path in $T$.

We have already shown how to construct the given carrier, eraser, and duplicator purely diagrammatically, and we have given them concrete interpretations in terms of $p$-trees, their vertices, and their $p$-subtrees.
So it remains to verify that the category laws hold for $\cofree{p}$, or equivalently that the comonoid laws hold for $\left(\car{t}_p,\epsilon_p,\delta_p\right)$.
Again, our argument will be purely formal, although it is not too hard to see that our concrete characterization above in terms of $p$-trees satisfies the laws for a category.

First, we verify the left erasure law: that

\[
\begin{tikzcd}
\yon\tri\car{t}_p & \car{t}_p \ar[l,equals] \ar[d, "\delta_p"] \\
& \car{t}_p\tri\car{t}_p \ar[ul, "\epsilon_p\:\tri\:\car{t}_p"]
\end{tikzcd}
\]

We know the lens $\epsilon_p\tri\car{t}_p\colon\car{t}_p\tri\car{t}_p\to\yon\tri\car{t}_p$ is characterized by its components $\epsilon_p\tri\epsilon^{(n)}_p\colon\car{t}_p\tri\car{t}_p\to p\tripow0\tri p\tripow{n}$, a projection out of the limit $\car{t}_p\tri\car{t}_p$, for all $n\in\nn$.
Then by our construction of $\delta_p$, each composite $\delta_p\then\left(\epsilon_p\tri\epsilon^{(n)}_p\right)\colon\car{t}_p\to p\tripow0\tri p\tripow{n}$ is the component of $\delta_p$ equal to $\epsilon^{(n)}_p=\epsilon^{(0+n)}_p\colon\car{t}_p\to p\tripow0\tri p\tripow{n}\iso p\tripow{n}$ (this is just the commutativity of (<ref>) in the case of $(\ell,m)=(0,n)$).
Together, these characterize the composite lens $\delta_p\then\left(\epsilon_p\tri\car{t}_p\right)\colon\car{t}_p\to\yon\tri\car{t}_p\iso\car{t}_p$ as the lens whose components are the projections $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$ from the limit.
It follows from the universal property of $\car{t}_p$ that $\delta_p\then\left(\epsilon_p\tri\car{t}_p\right)$ can only be the identity lens on $\car{t}_p$.
Hence the left erasure law holds.

The right erasure law, that

\[
\begin{tikzcd}
\car{t}_p \ar[r,equals] \ar[d, "\delta_p"'] & \car{t}_p\tri\yon \\
\car{t}_p\tri\car{t}_p \ar[ur, "\car{t}_p\:\tri\:\epsilon_p"']
\end{tikzcd}
\]

commutes, follows similarly: the composite $\delta_p\then\left(\car{t}_p\tri\epsilon_p\right)$ is characterized by its components over $n\in\nn$ of the form $\delta_p\then\left(\epsilon^{(n)}_p\tri\epsilon_p\right)\colon\car{t}_p\to p\tripow{n}\tri p\tripow0$, which we know by (<ref>) is equal to $\epsilon^{(n+0)}_p=\epsilon^{(n)}_p$, the projection out of the limit $\car{t}_p$.
It follows from the universal property of this limit that $\delta_p\then\left(\car{t}_p\tri\epsilon_p\right)$ must be the identity lens on $\car{t}_p$.

Finally, we check the coassociative law: that

\[
\begin{tikzcd}[column sep=large]
\car{t}_p\ar[r, "\delta_p"]\ar[d, "\delta_p"']&
\car{t}_p\tri\car{t}_p\ar[d, "\car{t}_p\:\tri\:\delta_p"]\\
\car{t}_p\tri\car{t}_p\ar[r, "\delta_p\:\tri\:\car{t}_p"']&
\car{t}_p\tri\car{t}_p\tri\car{t}_p,
\end{tikzcd}
\]

Because $\tri$ preserves connected limits, we can write $\car{t}_p\tri\car{t}_p\tri\car{t}_p$ as a limit the way we did with $\car{t}_p\tri\car{t}_p$: it is the limit of diagram consisting of arrows

\[
p\tripow{i}\tri p\tripow{j}\tri p\tripow{k}\to p\tripow{i}\tri p\tripow{j}\tri p\tripow{k}\tri\1
\]

for each $i,j,k\in\nn$, with additional arrows between the position-sets.
So a lens to $\car{t}_p\tri\car{t}_p\tri\car{t}_p$, such as those in the square above, is uniquely determined by its components to $p\tripow{i}\tri p\tripow{j}\tri p\tripow{k}$ for all $i,j,k\in\nn$, obtained by composing it with the projections $\epsilon^{(i)}_p\tri\epsilon^{(j)}_p\tri\epsilon^{(k)}_p$ out of the limit.
Then by (<ref>),

\begin{align*}
\delta_p\then\left(\car{t}_p\tri\delta_p\right)\then\left(\epsilon^{(i)}_p\tri\epsilon^{(j)}_p\tri\epsilon^{(k)}_p\right) &=
\delta_p\then\left(\epsilon^{(i)}_p\tri\left(\delta_p\then\left(\epsilon^{(j)}_p\tri\epsilon^{(k)}_p\right)\right)\right) \\ &=
\delta_p\then\left(\epsilon^{(i)}_p\tri\epsilon^{(j+k)}_p\right) \tag*{\eqref{eqn.delta_p_tri_epsilons}} \\ &=
\epsilon^{(i+j+k)}_p \tag*{\eqref{eqn.delta_p_tri_epsilons}} \\ &=
\delta_p\then\left(\epsilon^{(i+j)}_p\tri\epsilon^{(k)}_p\right) \tag*{\eqref{eqn.delta_p_tri_epsilons}} \\ &=
\delta_p\then\left(\left(\delta_p\then\left(\epsilon^{(i)}_p\tri\epsilon^{(j)}_p\right)\right)\tri\epsilon^{(k)}_p\right) \tag*{\eqref{eqn.delta_p_tri_epsilons}} \\ &=
\delta_p\then\left(\delta_p\tri\car{t}_p\right)\then\left(\epsilon^{(i)}_p\tri\epsilon^{(j)}_p\tri\epsilon^{(k)}_p\right).
\end{align*}

for all $i,j,k\in\nn$.
So by the universal property of $\car{t}_p\tri\car{t}_p\tri\car{t}_p$, coassociativity holds.

We call the category $\cofree{p}$ corresponding to the comonoid $\left(\car{t}_p,\epsilon_p,\delta_p\right)$ the category of $p$-trees, the category of trees on $p$, or the $p$-tree category.

[The category of $p$-trees: states and transitions for (co)free]
Let's step back and think about how $p$-tree categories relate to the original polynomial $p$ from the perspective of the states and transitions of dynamical systems.
Before we build any trees or categories out of it, a polynomial $p$ is just a family of sets of directions indexed over a set of positions.
The directions emerge from positions, but don't point to anywhere in particular.
If we want to interpret the positions of $p$ as states and the directions of $p$ as composable transitions, first we would need to point the directions to other positions by assigning them codomains.
There are many ways to do this, but we would like to do so “freely,” without having to make any choices along the way that would bias us one way or another, so as to give a canonical way to interpret $p$ as a category.

So to avoid making choices, rather than fixing a codomain for each direction, we allow every possible direction to point to every possible position once.
But a single direction of any one position cannot point to multiple positions, which is when we need to make several copies of each position: at least one copy for every possible combination of codomains that can be assigned to its directions.
This is how we get from $p$ to $p\tripow2$: the $p\tripow2$-pretrees represent all the ways we could assign codomains to the directions in $p$.
Essentially, we have freely refined our positions into more specific states to account for everywhere their directions could lead.
Each $p\tripow2$-pretree still remembers which $p\tripow1$-pretree it grew from, giving us our canonical trimming operation $p\tripow2(\1)\to p\tripow1(\1)$.

Yet even that is not enough: sure, we've assigned codomains to the directions of $p$ in every possible way, but now that we're building a category, we want our directions to be composable transitions.
So each pair of composable directions of $p$—each length-$2$ rooted path of the $p\tripow2$-pretrees—is now a possible transition as well, another morphism in our category.
To keep everything canonical, we still want to avoid making any actual choices; we can't simply say that two directions of $p$ compose to a third direction of $p$ that we already have.
Each pair of composable directions must be an entirely new morphism—and every new morphism needs a codomain.

You can tell where this is going.
To avoid actually choosing codomains for the new morphisms, we need to refine our $p\tripow2$-pretrees by making copies of them to account for every possibility, building $p\tripow3$-pretrees as a result.
Then their length-$3$ rooted paths are new morphisms, too, and they need new codomains, and so forth, ad infinitum.
Indeed, this process cannot terminate in a finite number of steps, but that's okay—we can take the limit, yielding the ultimate free refinement of positions into states and free composites of directions as transitions.

This is where (<ref>) comes from; it captures the infinite process of turning sequences of directions into morphisms by giving them codomains in every possible way, then dealing with the longer sequences of directions that emerge as a result.
Note that we also need to account for the fact that every object needs an identity; to avoid making a choice, we don't set it to be any direction or composite of multiple directions of $p$, reserving it instead for the empty sequence of directions that every pretree has.
Then the limit $\car{t}_p$ of (<ref>) is all we need: the $p$-trees are states representing every possible way that sequences of directions emerging from a $p$-position can lead to other $p$-positions, and the rooted paths of each $p$-tree are transitions accounting for every finite sequence of composable directions from the corresponding state.

Since composites were freely generated, directions and thus entire rooted paths compose by concatenation—making the empty rooted path the correct identity.
And the codomain is whatever the direction at the end of a rooted path has been freely assigned to point to—not just the $p$-position there but the whole $p$-subtree, an entire state representing all the sequences of directions one could take and the positions to which they lead, starting from the end of the path just followed.
This gives the comonoid structure on $\car{t}_p$, completing the cofree construction of the category of $p$-trees $\cofree{p}$.

Soon we will prove that $\cofree{p}$ really is the cofree category on $p$, but first we give some examples to make all this concrete.

§.§.§ Examples of $p$-tree categories

In what follows, we will freely switch between the morphisms-as-vertices and the morphisms-as-rooted-paths perspectives of $p$-tree categories given in <ref> whenever convenient.

[The category of $\1$-trees]
Let's start by taking $p\coloneqq\1$.
In <ref> <ref>, we showed that there is a unique $\1$-tree: a tree with only $1$ vertex, its root.
So $\car{t}_\1\iso\yon$ is the carrier of the category of $\1$-trees $\cofree\1$.

Up to isomorphism, there is only one category carried by $\yon$: the terminal category with $1$ object and no morphisms aside from the $1$ identity.
When we think of this as the category of $\1$-trees, we can characterize it as follows.

* The $1$ object is the tree with $1$ vertex: call the tree $\bullet$, because that's what it looks like.

* The $1$ morphism $\bullet\to\_$ is the $1$ vertex of $\bullet$, its root.
After all, there are no directions of $\1$ to freely compose, so the only morphism generated is the identity.
Since the $\1$-subtree of $\bullet$ rooted as its root is just the entire $\1$-tree $\bullet$, the codomain of this morphism is still $\bullet$, which makes sense—it's the only object we have.

* The identity morphism $\id_\bullet\colon\bullet\to\bullet$ is the root of $\bullet$.
This is the same morphism we just mentioned.
Equivalently, it is the empty rooted path.

* The composite morphism $\id_\bullet\then\id_\bullet=\id_\bullet\then\id_{\cod(\id_\bullet)}\colon\bullet\to\_$ is obtained by concatenating the empty rooted path $\id_\bullet$ of $\bullet$ with the empty rooted path $\id_{\cod(\id_\bullet)}$ of $\cod(\id_\bullet)$, which is again just the empty rooted path of $\bullet$.
Hence $\id_\bullet\then\id_{\cod\id_\bullet}=\id_\bullet$, as expected—it's the only morphism we have.

This is certainly too trivial an example to say much about, but it demonstrates how we can interpret the category carried by $\yon$ as the category of $p$-trees for $p\coloneqq\1$.
Moreover, it helps us see concretely why taking the identity to be the root gives it the right codomain and compositional behavior.

[The category of trees on a constant]
Let $B$ be a set, viewed as a constant polynomial.

* What is the polynomial $\car{t}_B$?

* Characterize the $B$-tree category $\cofree{B}$.

* We compute $\car{t}_B$ as follows.
To select a $B$-tree, we must select a position from $B$.
Then we are done, because there are no directions.
So every $B$-tree consists of $1$ vertex labeled with an element of $B$.
Hence the set of $B$-trees $\car{t}_B(\1)=\tr_B$ is in bijection with $B$ itself, yielding $\car{t}_B\iso B\yon$.
(We could have also applied <ref> <ref> in the case of $A=\0$, yielding $\car{t}_{B\yon^\0}\iso B^{\lst(\0)}\yon^{\lst(\0)}\iso B\yon$, as $\lst(\0)\iso\1+\0^\1+\0^\2+\cdots\iso\1$—the empty sequence is the only sequence with elements in $\0$.)

* We characterize the $B$-tree category $\cofree{B}$ as follows.
We saw in <ref> and <ref> that (up to isomorphism) there is a unique comonoid structure on $B\yon$, corresponding to the discrete category on $B$.
So $\cofree{B}$ must be isomorphic to the discrete category on $B$.
In the language of $B$-trees, the objects of $\cofree{B}$ are trees with exactly $1$ vertex, labeled with an element of $B$.
Each tree has an identity morphism, its root; but there are no vertices aside from the root, so there are no morphisms aside from the identities.
In particular, the only $B$-subtree of any one $B$-tree is the entire $B$-tree itself, so there are no morphisms from one $B$-tree to a different $B$-tree.
So the category of $B$-trees can indeed be identified with the discrete category on $B$.

[The category of $\yon$-trees]
Now consider $p\coloneqq\yon$.
In <ref> <ref>, we showed that there is a unique $\yon$-tree: a single ray extending from the root in which every vertex has exactly $1$ child, so that there is exactly $1$ height-$n$ vertex—and $1$ length-$n$ rooted path—for every $n\in\nn$.
Then $\car{t}_\yon\iso\yon^\nn$ is the carrier of the category of $\yon$-trees $\cofree\yon$.
In fact, we can identify the set of rooted paths of this $\yon$-tree with $\nn$, so that $n\in\nn$ is the $\yon$-tree's unique length-$n$ rooted path.

We know from <ref> that comonoids with representable carriers correspond to $1$-object categories, which can be identified with monoids.
In particular, a comonoid structure on $\yon^\nn$ corresponds to a monoid structure on $\nn$.
There is more than one monoid structure on $\nn$, though, so which one corresponds to the category $\cofree\yon$?

We can characterize $\cofree\yon$ in terms of $\yon$-trees as follows.

* The $1$ object is the unique $\yon$-tree, a single ray: call it $\uparrow$.
Here is a picture of this ray, to help you visualize its vertices, rooted paths, and subtrees:

\begin{gather*}
\vdots\\
\begin{tikzpicture}[trees]
\node {$\bullet$}
child {node {$\bullet$}
child {node {$\bullet$}
child {node {$\bullet$}
child {node {$\vphantom\bullet$}}
\end{tikzpicture}
\end{gather*}

* The morphisms are the rooted paths of $\uparrow$; they comprise the set $\nn$, where each $n\in\nn$ is the unique rooted path of $\uparrow$ of length $n$.
Each rooted path represents the free composite of $n$ copies of the sole direction of $\yon$.
Since $\uparrow$ is an infinite ray, the $\yon$-subtree of $\uparrow$ rooted at any of its vertices is still just a copy of $\uparrow$.
So the codomain of each morphism is still $\uparrow$, which makes sense—it's the only object we have.

* The identity morphism $\id_\uparrow\colon{\uparrow}\to{\uparrow}$ is the empty rooted path, which has length $0$; so $\id_\uparrow=0$.
In the corresponding monoid structure on $\nn$, the element $0\in\nn$ must then be the unit.

* The composite morphism $m\then n\colon{\uparrow}\to{\uparrow}$ for $m,n\in\nn$ is obtained by concatenating $m$, i.e. the length-$m$ rooted path of $\uparrow$, with $n$, i.e. the length-$n$ rooted path of $\uparrow$, translating the latter path so that it begins where the former path ends.
The result is then the rooted path of $\uparrow$ of length $m+n$; so $m\then n=m+n$.
In the corresponding monoid structure on $\nn$, the binary operation must then be given by addition.

Hence $\cofree{\yon}$ is the monoid $(\nn,0,+)$ viewed as a $1$-object category.

[$B\yon$-trees are $B$-streams]
Let $B$ be a set, and consider $p\coloneqq B\yon$.
Generalizing <ref> <ref> for $B$ instead of $\2$, or applying <ref> <ref> for the case of $A\coloneqq\1$, we can deduce that a $B\yon$-tree consists of a single ray for which every vertex is given a label from $B$.
So the vertices of a $B\yon$-tree are in bijection with $\nn$, and $B\yon$-trees are in bijection with functions $\nn\to B$ assigning each vertex a label.
Hence $\car{t}_{B\yon}\iso B^\nn\yon^\nn$ is the carrier of the category of $B\yon$-trees $\cofree{B\yon}$.
As in <ref>, we identify the set of rooted paths of a given $B\yon$-tree with $\nn$, so that $n\in\nn$ is the $B\yon$-tree's unique length-$n$ rooted path.

In fact, we have already seen the category $\cofree{B\yon}$ once before: it is the category of $B$-streams from <ref>.

* Recall that a $B$-stream is an element of $B^\nn$ interpreted as a countable sequence of elements $b_n\in B$ for $n\in\nn$, written like so:

\[
\ol{b}\coloneqq(b_0\to b_1\to b_2\to b_3\to\cdots).
\]

This is just a $B\yon$-tree lying on its side!
Each arrow is a copy of the sole direction at each position of $B\yon$, pointing to one of the positions in $B$ for that direction to lead to next.

* Given a $B$-stream $\ol{b}\in B^\nn$ above, recall that a morphism out of $\ol{b}$ is a natural number $n\in\nn$, and its codomain is the substream of $B$ starting at $b_n$:

\[
\cod(\ol{b}\To{n}\_)=(b_n\to b_{n+1}\to b_{n+2}\to b_{n+3}\to\cdots).
\]

This coincides with how we view morphisms as rooted paths and codomains as subtrees rooted at the end of those paths in the category of $B\yon$-trees.

* Whether we view $\ol{b}$ as a $B$-stream or a $B\yon$-tree, its identity morphism $\id_{\ol{b}}\colon\ol{b}\to\ol{b}$ corresponds to $0\in\nn$; from the latter perspective, it is the length-$0$ path from the root to itself.

* Whether we view $\ol{b}$ as a $B$-stream or a $B\yon$-tree, composition is given by addition; from the latter perspective, concatenating a length-$m$ rooted path with a length-$n$ path yields a length-$(m+n)$ rooted path.

[The category of $\nn$-labeled binary trees]
Consider $p\coloneqq\nn\yon^\2$.
By <ref> <ref>, or <ref> <ref> in the case of $L\coloneqq\nn$ and $\ord{n}\coloneqq\2$, an $\nn\yon^\2$-tree is an infinite binary tree with vertices labeled by elements of $\nn$.
Here's how such an $\nn\yon^\2$-tree might start:

\[
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm},
level 3/.style={sibling distance=2.5mm}]
\node {$17$}
child {node {$3$}
child {node {$0$}
child {node {$3$}
child {node {$1$}
child {node {$92$}
child {node {$6$}
\end{tikzpicture}
\]

We can characterize the category $\cofree{\nn\yon^\2}$ as follows.

* The objects are $\nn$-labeled binary trees from the set $\nn^{\lst(\2)}$.

* A morphism out of an $\nn$-labeled binary tree is a binary sequence: a finite list of directions in $\2$, whose elements could be interpreted as “left” and “right,” thus uniquely specifying a rooted path in a binary tree.
They comprise the set $\lst(\2)$.
The codomain of each rooted path is the $\nn$-labeled binary subtree rooted at the end of the path.

* The identity morphism on a given $\nn$-labeled binary tree is its empty rooted path.

* The composite of two binary sequences is obtained by concatenation.

[The category of $B$-labeled $A$-ary trees]
Characterize the $B\yon^A$-tree category $\cofree{B\yon^A}$.

We characterize $\cofree{B\yon^A}$, following <ref>.

* The objects are $B\yon^A$-trees.
By <ref> <ref>, or <ref> <ref> with $L\coloneqq B$ and $\ord{n}$ replaced with an arbitrary set $A$, a $B\yon^A$-tree is a (infinite, assuming $|A|,|B|>0$) tree whose every vertex is labeled by an element of $B$ and whose children are in bijection with $A$.
We can call these $B$-labeled $A$-ary trees; they are in bijection with the set $B^{\lst(A)}$.

* A morphism out of a $B$-labeled $A$-ary tree is a finite list of directions in $A$, or a rooted path in an $A$-ary tree.
They comprise the set $\lst(A)$.
The codomain of each rooted path is the $B$-labeled $A$-ary subtree rooted at the end of the path.

* The identity morphism on a given $B$-labeled $A$-ary tree is its empty rooted path.

* The composite of two lists in $A$ is obtained by concatenation.

Characterize the $\left(\yon+\1\right)$-tree category $\cofree{\yon+\1}$.

We characterize $\cofree{\yon+\1}$ as follows.

* The objects are $(\yon+\1)$-trees.
By <ref> <ref>, a $(\yon+\1)$-tree is either a single length-$n$ path for some $n\in\nn$, which we denote by $[n]$, or a ray, which we denote by $[\infty]$.
So the set of objects is $\tr_{\yon+\1}=\{[n]\mid n\in\nn\cup\{\infty\}\}\iso\nn\cup\{\infty\}$.

* A finite $(\yon+\1)$-tree $[n]$ for $n\in\nn$ has $n+1$ rooted paths: $1$ each of length $0$ through $n$, inclusive.
So a morphism out of $[n]$ can be identified with an element of the set $\{0,\ldots,n\}$.

Meanwhile, the infinite $(\yon+\1)$-tree $[\infty]$, a ray, has exactly $1$ rooted path of every length $\ell\in\nn$.
So a morphism out of $[\infty]$ can be identified with an element of the set $\nn$.
Every $(\yon+\1)$-subtree of the ray is still a ray, so the codomain of each of these morphisms is still $[\infty]$.

* The identity morphism on a given $B$-labeled $A$-ary tree is its empty rooted path.

* The composite of two lists in $A$ is obtained by concatenation.

Let $p\coloneqq \{a,b,c,\ldots,z,\text{\textvisiblespace}\}\yon+\{\bullet\}$.

* Describe the objects of the cofree category $\cofree{p}$, and draw one.

* For a given such object, describe the set of emanating morphisms.

* Describe how to take the codomain of a morphism.

* An object in $\cofree{p}$ is a stream of letters $a,b,\ldots,z$ and spaces $\text{\textvisiblespace}$, that may go on forever or may end with a gigantic period, “$\bullet$”. So an example is the infinite stream $aaaaa\cdots$. Another example is $hello\text{\textvisiblespace}world\bullet$.

* The object $aaaaa\cdots$ has $\nn$ as its set of emanating morphisms. The object $hello\text{\textvisiblespace}world\bullet$ has $\{0,\ldots,11\}$ as its set of emanating morphisms.

* The codomain of any morphism out of $aaaaa\cdots$ is again $aaaaa\cdots$. The codomain of any morphism $0\leq i\leq 11$ out of $hello\text{\textvisiblespace}world\bullet$ is the string one obtains by removing the first $i$ letters of $hello\text{\textvisiblespace}world\bullet$.

Let $p\coloneqq\{\bul[red],\bul[blue]\}\yon^\2+\{\bul[dgreen]\}\yon+\{\bul[dyellow]\}$ as in <ref>.

* Choose an object $t\in \tr_p$, i.e. a tree in $p$, and draw a finite approximation of it (say four layers).

* What is the identity morphism at $t$?

* Choose a nonidentity morphism $f$ emanating from $t$ and draw it.

* What is the codomain of $f$? Draw a finite approximation of it.

* Choose a morphism emanating from the codomain of $f$ and draw it.

* What is the composite of your two morphisms? Draw it on $t$.

\[
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm},
level 3/.style={sibling distance=2.5mm}]
\node {$\bul[red]$}
child {node {$\bul[blue]$}
child {node {$\bul[dgreen]$}
child {node {$\bul[red]$}
child {node {$\bul[dyellow]$}
child {node {$\bul[dgreen]$}
child {node {$\bul[blue]$}
child {node {$\bul[dyellow]$}
child {node {$\bul[blue]$}
\end{tikzpicture}
\]

* The identity morphism at $t$ is the trivial path starting at the root node.

* We indicate a morphism $f$ using thick arrows:

\[
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm},
level 3/.style={sibling distance=2.5mm}]
\node {$\bul[red]$}
child[thin] {node {$\bul[blue]$}
child {node {$\bul[dgreen]$}
child {node {$\bul[red]$}
child {node {$\bul[dyellow]$}
child[very thick] {node {$\bul[dgreen]$}
child {node {$\bul[blue]$}
child[thin] {node {$\bul[dyellow]$}
child[thin] {node {$\bul[blue]$}
\end{tikzpicture}
\]

* The codomain of $f$ is the tree rooted at the target of the path, namely

\[
\begin{tikzpicture}[trees,sibling distance=2.5mm]
\node {$\bul[blue]$}
child[thin] {node {$\bul[dyellow]$}
child[thin] {node {$\bul[blue]$}
\end{tikzpicture}
\]

* Here's a morphism emanating from the codomain of $f$:

\[
\begin{tikzpicture}[trees,sibling distance=2.5mm]
\node {$\bul[blue]$}
child[very thick] {node {$\bul[dyellow]$}
child[thin] {node {$\bul[blue]$}
\end{tikzpicture}
\]

* The composite morphism on the original tree is:

\[
\begin{tikzpicture}[trees,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm},
level 3/.style={sibling distance=2.5mm}]
\node {$\bul[red]$}
child[thin] {node {$\bul[blue]$}
child {node {$\bul[dgreen]$}
child {node {$\bul[red]$}
child {node {$\bul[dyellow]$}
child[very thick] {node {$\bul[dgreen]$}
child {node {$\bul[blue]$}
child[very thick] {node {$\bul[dyellow]$}
child[thin] {node {$\bul[blue]$}
\end{tikzpicture}
\]

Let $p$ be a polynomial, let $Q\coloneqq\{q\in\qq\mid q\geq 0\}$ and consider the monoid $\yon^Q$ of nonnegative rational numbers under addition. Is it true that any cofunctor $\varphi\colon\cofree{p}\cof\yon^\qq$ is constant, i.e. that it factors as

\[
\cofree{p}\cof\yon\cof\yon^\qq?
\]

Take $p\coloneqq\2\yon$, and consider the object $x\in\cofree{p}(\1)$ given by the stream

\[
\]

(with spaces only for readability); note that every morphism emanating from $x$ has a different codomain. We need to give $\varphi^\sharp_i(q)$ for every $i\in\cofree{p}(\1)$ and $q\geq 0$. Define

\[
\varphi^\sharp_i(q)\coloneqq
\begin{cases}
i&\tn{ if }i\neq x \tn{ or } q=0\\
x'&\tn{ if }i=x\tn{ and } q>0
\end{cases}
\]

where $x'\coloneqq(12\,112\,1112\,11112\,111112\ldots)$. There are three cofunctor conditions to check, namely identity, codomains, and composition. The codomain condition is vacuous since $\yon^Q$ has one object, and the identity condition holds by construction, because we always have $\varphi^\sharp_i(0)=i$. Now take $q_1,q_2\in Q$; we need to check that

\[\varphi^\sharp_{\cod\varphi^\sharp_i(q_1)}(q_2)=^?\varphi^\sharp_i(q_1+q_2)\]

holds. If $i\neq x$ or $q_1=q_2=0$, then it holds because both sides equal $i$. If $i=x$ and either $q_1>0$ or $q_2>0$, it is easy to check that both sides equal $x'$, so again it holds.

§.§ Exhibiting the forgetful-cofree adjunction

We are now ready to give a diagrammatic proof of the main result of this section: as promised, the category $\cofree{p}$ we constructed is the cofree comonoid on $p$.

The forgetful functor $U\colon \smcat^\sharp\to\poly$ has a right adjoint $\cofree{-}\colon\poly\to\smcat^\sharp$, giving rise to an adjunction

\[
\adj{\smcat^\sharp}{U}{\cofree{-}}{\poly},
\]

such that for each $p\in\poly$, the carrier $\car{t}_p\coloneqq U\cofree{p}$ of the category $\cofree{p}$ is given by the limit of the diagram (<ref>), repeated here:

\[
\begin{tikzcd}
\yon \ar[d] &
p \ar[d] &
p\tripow2 \ar[d] &
[10pt] p\tripow3 \ar[d] &
\cdots\\
\1 &
p\tri\1 \ar[l, "!"'] &
p\tripow2\tri\1 \ar[l, "p\:\tri\:!"'] &
p\tripow3\tri\1 \ar[l, "p\tripow2\:\tri\:!"'] &
\cdots.\ar[l]
\end{tikzcd}
\]

That is, for any category $\cat{C}\in\smcat^\sharp$ with carrier $\car{c}\coloneqq U\cat{C}$, there is a natural isomorphism

\[
\poly(\car{c},p)\iso\smcat^\sharp(\cat{C},\cofree{p}).
\]

To show that $\cofree{-}$ is the right adjoint of $U$, it is enough to show that for every lens $\varphi\colon\car{c}\to p$, there exists a unique cofunctor $F\colon\cat{C}\cof\cofree{p}$ for which

\begin{equation} \label{eqn.cofree_universal_lens_counit}
\begin{tikzcd}
\car{c} \ar[d,dashed,"F"'] \ar[dr,"\varphi"] \\
\car{t}_p \ar[r,"\epsilon^{(1)}_p"'] & p
\end{tikzcd}
\end{equation}

Here the projection $\epsilon^{(1)}_p\colon U\cofree{p}\iso\car{t}_p\to p$ serves as the counit of the adjunction, and we identify the cofunctor $F$ with its underlying lens $UF\colon\car{c}\to\car{t}_p$.

First, we construct $F$ from $\varphi$ as follows.
If we let $\epsilon$ and $\delta$ be the eraser and duplicator of $\cat{C}$, the diagram

\begin{equation} \label{eqn.phi_seed}
\begin{tikzcd}[column sep=large]
\car{c} \ar[d, "\epsilon"'] \ar[r, "\delta"] \ar[dr, "\varphi"'] &
\car{c}\tri\car{c} \ar[d, "\epsilon\:\tri\:\varphi"] \\
\yon \ar[d] & p \ar[d] \\
\1 & p\tri\1 \ar[l]
\end{tikzcd}
\end{equation}

commutes: the pentagon in the lower left commutes trivially, while the triangle in the upper right commutes by the left erasure law of $\cat{C}$, as

\begin{align*}
\delta\then\left(\epsilon\tri\varphi\right)&=
\delta\then\left(\epsilon\tri\car{c}\right)\then\varphi \\ &=
\id_\car{c}\then\varphi \tag{Left erasure law} \\ &=
\varphi.
\end{align*}

Then by induction, the larger diagram

\begin{equation} \label{eqn.phi_expand}
\begin{tikzcd}[column sep=large]
\car{c} \ar[d,"\epsilon"'] \ar[r,"\delta"] \ar[dr,"\varphi"'] & \car{c}\tri\car{c} \ar[d,"\epsilon\:\tri\:\varphi"] \ar[r,"\delta\:\tri\:\car{c}"] & \car{c}\tripow3 \ar[d, "\epsilon\:\tri\:\varphi\tripow2"] \ar[r,"\delta\:\tri\:\car{c}\tripow2"] & \car{c}\tripow4 \ar[d,"\epsilon\:\tri\:\varphi\tripow{3}"] \ar[r] & \cdots \\
\yon \ar[d] & p \ar[d] & p\tripow2 \ar[d] & p\tripow3 \ar[d] & \cdots \\
\1 & p\tri\1 \ar[l] & p\tripow2\tri\1 \ar[l] & p\tripow3\tri\1 \ar[l] & \cdots \ar[l]
\end{tikzcd}
\end{equation}

commutes as well: its leftmost rectangle is (<ref>), and taking the composition product of each rectangle in (<ref>) with the commutative rectangle

\[
\begin{tikzcd}[column sep=large]
\car{c} \ar[d, "\varphi"'] \ar[r, equals] & \car{c} \ar[d, "\varphi"] \\
p \ar[d, equals] & p \ar[d, equals] \\
p & p \ar[l, equals]
\end{tikzcd}
\]

yields the rectangle to its right.
As $\car{t}_p$ is the limit of the bottom two rows of (<ref>), it follows that there is an induced lens $F\colon\car{c}\to\car{t}_p$ that, when composed with each projection $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$, yields the lens depicted in (<ref>) from $\car{c}$ to $p\tripow{n}$.
This lens is the composite of the lens $\car{c}\to\car{c}\tripow{(n+1)}$ in the top row, which by <ref> is the canonical lens $\delta^{(n+1)}$ associated with the comonoid $\cat{C}$, composed with the lens $\epsilon\tri\varphi\tripow{n}\colon\car{c}\tripow{(n+1)}\to p\tripow{n}$.

Next, we prove uniqueness: that a cofunctor $\cat{C}\cof\cofree{p}$ with underlying lens $f\colon\car{c}\to\car{t}_p$ is completely determined by the value of $f\then\epsilon^{(1)}_p$.
It suffices to show that we can recover the $n^\text{th}$ component of $g$ from its first component.

§.§ The many (inter)faces of the cofree comonoid

The forgetful-cofree adjunction of <ref> tells us that given a category $\cat{C}\in\smcat^\sharp$ with carrier $\car{c}\coloneqq U\cat{C}$ and a polynomial $p\in\poly$, there is a natural isomorphism

\[
\poly(\car{c},p)\iso\smcat^\sharp(\cat{C},\cofree{p}).
\]

So every lens $\varphi\colon\car{c}\to p$ has a corresponding cofunctor $F\colon\cat{C}\cof\cofree{p}$ that we call its mate.

We can view $\varphi$ as a dynamical system with an interface $p$ and a generalized state system $\car{c}$, carrying an arbitrary category $\cat{C}$ of states and transitions.
Then the lens $\text{Run}_n(\varphi)\colon\car{c}\to p\tripow{n}$ for $n\in\nn$, defined as the composite

\[
\car{c}\To{\delta^{(n)}}\car{c}\tripow{n}\To{\varphi\tripow{n}}p\tripow{n},
\]

models $n$ runs through the system $\varphi$.

Meanwhile, as the limit of the diagram (<ref>) with the row of polynomials of the form $p\tripow{n}$ across the top, the carrier $\car{t}_p$ of the cofree comonoid on $p$ comes equipped with a lens $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$ for each $n\in\nn$.
Since the cofunctor $F\colon\cat{C}\cof\cofree{p}$ has an underlying lens between carriers $f\coloneqq UF\colon\car{c}\to\car{t}_p$, we can obtain another lens $\car{c}\to\tripow{n}$ as the composite

\[
\car{c}\To{f}\car{t}_p\To{\epsilon^{(n)}_p}p\tripow{n}.
\]

It follows from our forgetful-cofree adjunction that these two composites are equal.

With the definitions above, the following diagram commutes:

\[
\begin{tikzcd}
\car{c} \ar[r,"f"] \ar[d, "\delta^{(n)}"'] & \car{t}_p \ar[d, "\epsilon^{(n)}_p"] \\
\car{c}\tripow{n} \ar[r, "\varphi\tripow{n}"'] & p\tripow{n}.
\end{tikzcd}
\]

Now we have a better sense of what we mean when we say that $F\colon\cat{C}\cof\cofree{p}$ captures all the information that the lenses $\text{Run}_n(\varphi)\colon\car{c}\to p\tripow{n}$ encode: the category $\cofree{p}$ is carried by a polynomial $\car{t}_p$ equipped with lenses $\epsilon^{(n)}_p\colon\car{t}_p\to p\tripow{n}$, each of which exposes a part of the category as the $n$-fold interface $p\tripow{n}$.
All together, $\car{t}_p$ acts as a giant interface that captures the $n$-fold behavior of $p\tripow{n}$ for every $n\in\nn$.
But to see all this explicitly, let's consider some examples.

Let $S\coloneqq\{\bul[dgreen],\bul[dyellow],\bul[red]\}$ and $p\coloneqq\yon^\2+\1$, and consider the dynamical system $\varphi\colon S\yon^S\to p$ modeling the halting deterministic state automaton from <ref>, depicted here again for your convenience:

\[
\begin{tikzcd}[column sep=small]
\bul[blue]\ar[rr, bend left, orange]\ar[loop left, dgreen]&&
\bul[dyellow]\ar[dl, bend left, orange]\ar[ll, dgreen, bend left]\\&
\bul[red]
\end{tikzcd}
\]

Under the forgetful-cofree adjunction, the lens $\varphi$ coincides with a cofunctor $F\colon S\yon^S\cof\cofree{p}$ from the state category on $S$ to the category of $p$-trees.
The cofunctor sends each state in $S=\{\bul[dgreen],\bul[dyellow],\bul[red]\}$ to a $p$-tree; these $p$-trees are drawn below (the first two are infinite).
Then the vertices of each $p$-tree are sent back to a morphism in the state category; the color of each vertex indicates the codomain of the morphism to which that vertex is sent.

\[
\begin{tikzpicture}[trees, scale=1.5,
level 1/.style={sibling distance=20mm},
level 2/.style={sibling distance=10mm},
level 3/.style={sibling distance=5mm},
level 4/.style={sibling distance=2.5mm},
level 5/.style={sibling distance=1.25mm}]
\node[blue] (a) {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange]  {node[red] {$\bullet$}}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange]  {node[red] {$\bullet$}}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[red] {$\bullet$}}
child[orange] {node[red] {$\bullet$}
\end{tikzpicture}
\hspace{.5in}
\begin{tikzpicture}[trees, scale=1.5,
level 1/.style={sibling distance=20mm},
level 2/.style={sibling distance=10mm},
level 3/.style={sibling distance=5mm},
level 4/.style={sibling distance=2.5mm},
level 5/.style={sibling distance=1.25mm}]
\node[dyellow] (a) {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange]  {node[red] {$\bullet$}}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {node[blue] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange] {node[dyellow] {$\bullet$}
child[dgreen] {}
child[orange] {}
child[orange]  {node[red] {$\bullet$}}
child[orange] {node[red] {$\bullet$}
\end{tikzpicture}
\hspace{.5in}
\begin{tikzpicture}
\node[red] {$\bullet$};
\end{tikzpicture}
\]

Each $p$-tree above, with its vertices colored, thus encodes all the ways to navigate the automaton.
In particular, the maximal rooted paths of these trees (i.e. those that terminate at a leaf) trace out all the ways in which the automaton can halt, and therefore all the words that the automaton accepts.
Notice, too, that every $p$-subtree of any one of these $p$-trees is another one of these three $p$-trees—do you see why?

In general, given a lens $\varphi\colon S\yon^S\to\yon^A+\1$ modeling a halting deterministic state automaton and an initial state $s_0\in S$, the $(\yon^A+\1)$-tree to which the corresponding cofunctor $F\colon S\yon^S\cof\cofree{\yon^A+\1}$ sends $s_0$ encodes the set of words accepted by the automaton with that initial state in its maximal rooted paths.

[Languages recognized by deterministic state automata]
Recall from <ref> that a deterministic state automaton with a set of states $S$ and a set of input symbols $A$ can be identified with a lens $\yon\to S\yon^S$, indicating the initial state $s_0\in S$, and a lens $\varphi\colon S\yon^S\to\2\yon^A$, indicating the subset of accept states $F\coloneqq\varphi_1^{-1}(2)\ss S$ and the update function $u\colon S\times A\to S$ via $u(s,a)=\varphi^\sharp_s(a)$.

Under the forgetful-cofree adjunction, the lens $\varphi$ coincides with a cofunctor $F\colon S\yon^S\cof\cofree{\2\yon^A}$.
By <ref>, $\cofree{\2\yon^A}$ is the category of $\2$-labeled $A$-ary trees.
So $F(s_0)$ is an element of $\tr_{\2\yon^A}\iso\2^{\lst(A)}$: an $A$-ary tree where each rooted path corresponds to a list of elements of $A$ and bears one of the elements of $\2$, indicating whether the course through the automaton corresponding to that rooted path ends at an accept state or not.
Equivalently, an element of $\2^{\lst(A)}$ is a subset of $\lst(A)$; in the case of $F(s_0)$, it is the subset containing exactly the words in $\lst(A)$ accepted by the automaton.
So on objects, $F$ sends each possible start state $s_0\in S$ of the automaton to the subset of words that the automaton would then accept!
Backward on morphisms, $F^\sharp_{s_0}$ sends every possible word to the state the automaton would reach if it followed that word starting from $s_0$.

[Input sequences to output sequences]
We interpret our dynamical systems as converting sequences of input to sequences of output.
The forgetful-cofree adjunction allows us to express this conversion formally in the language of $\poly$.
For convenience, we'll focus on the example of an $(A,B)$-Moore machine $\varphi\colon S\yon^S\to B\yon^A$, although of course we can generalize this beyond monomial interfaces.

The lens $\varphi$ corresponds to a cofunctor $F\colon S\yon^S\cof\cofree{B\yon^A}$.
By <ref>, $\cofree{B\yon^A}$ is the category of $B$-labeled $A$-ary trees; in paticular, its carrier is $\car{t}_{B\yon^A}\iso B^{\lst(A)}\yon^{\lst(A)}$.

Then for every initial state $s_0\in S$, the $B$-labeled $A$-ary tree $F(s_0)$ can be interpreted as a decision tree of all the possible sequences of inputs that the system may receive.
The label in $B$ corresponding to the vertex (or rooted path) specified by each sequence in $\lst(A)$ tells us the final output that the system returns when that sequence is fed in as input.
Put another way, $F(s_0)\in B^{\lst(A)}$ can be interpreted as a function $\lst(A)\to B$.
So if the input sequence is $(a_1,\ldots,a_n)\in A^n\ss\lst(A)$, then the corresponding output sequence $(b_0,\ldots,b_n)\in B^{n+1}$ is given (non-recursively!) by

\[
b_i\coloneqq F(s_0)(a_1,\ldots,a_i).
\]

Finally, $F^\sharp_{s_0}(a_1,\ldots,a_i)\in S$ then corresponds to the system's state after that sequence of inputs is given.

§.§ Morphisms between cofree comonoids

Given a lens $\varphi \colon p \to q$, the cofree functor gives us a comonoid morphism $\cofree{\varphi}\colon\cofree{p}\to\cofree{q}$ as follows.

An object $t \in \tr_p$ is a tree; the tree $u \coloneqq \cofree{\varphi} (t) \in \tr_q $ is constructed recursively as follows. If the root of $t$ is $i \in p(\1)$ then the root of $u$ is $j \coloneqq \varphi_1 (i)$. To each branch $b \in q[j]$, we need to assign a new tree, and we use the one situated at $\varphi_i ^ \sharp (b)$.

Let $p \coloneqq \{\bul[dgreen]\}\yon ^\2 + \{\bul[red]\}$ and $q \coloneqq \{\bul[dgreen],\bul[dyellow]\} \yon + \{\bul[red],\bul[black]\}$.

* Choose a lens $\varphi\colon p\to q$, and write it out.

* Choose a tree $T\in\tr_p$ with at least height $3$.

* What is $\cofree{\varphi}(T)$?

Recall that $p \coloneqq \{\bul[dgreen]\}\yon ^\2 + \{\bul[red]\}$ and $q \coloneqq \{\bul[dgreen],\bul[dyellow]\} \yon + \{\bul[red],\bul[black]\}$.

* Have $\varphi\colon p\to q$ send forward $\bul[dgreen]\mapsto\bul[dgreen]$, with the unique element of $q[\bul[dgreen]]$ sent back to the left branch of $p[\bul[dgreen]]$, and send forward $\bul[red]\mapsto\bul[red]$.

* Here is a sample $T\in\tr_p$.

\[
\begin{tikzpicture}[trees, scale=1.5,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm}]
\node[dgreen] (a) {$\bullet$}
child {node[dgreen] {$\bullet$}
child {node[red] {$\bullet$}
child{node[dgreen] {$\bullet$}
child {node[red] {$\bullet$}
\end{tikzpicture}
\]

* Here is $\cofree{\varphi}(T)$:

\[
\begin{tikzpicture}[trees, scale=1.5,
level 1/.style={sibling distance=10mm},
level 2/.style={sibling distance=5mm}]
\node[dgreen] (a) {$\bullet$}
child {node[dgreen] {$\bullet$}
child {node[red] {$\bullet$}
\end{tikzpicture}
\]

Let $p$ be a polynomial.

* Show there is an induced cofunctor $\cofree{p} \to \cofree{p\tripow{n}}$ for all $n\in\nn$.

* When $n\geq1$, is the induced cofunctor is an isomorphism?

* By the adjunction from <ref>, cofunctors $\cofree{p} \to \cofree{p\tripow{n}}$ are in bijection with lenses $\car{t}_{p}\to p\tripow{n}$, where $\car{t}_{p}=U\cofree{p}$ is the carrier.

From <ref> we have a lens $\delta^{(n)}\colon\cofree{p}\to\cofree{p}\tripow{n}$, and we also have the counit of the cofree adjunction which we'll temporarily call $r\colon\cofree{p}\to p$. Then the desired lens is $(\delta^{(n)}\then r\tripow{n})\colon\car{t}_{p}\to p\tripow{n}$.

* When $n=1$ the induced cofunctor is an isomorphism, but for $n\geq 2$ it is not. However, we should start by saying that the function on objects $\tr_p\to\tr_{p\tripow{n}}$ is a bijection. It sends a $p$-tree to the $p\tripow{n}$ tree that simply compresses every height-$n$ segment into a single vertex, labeled by that height-$n$ segment. To go back, just decompress the segments. But this is not a bijection on maps, because every rooted path on $\tr_{p\tripow{n}}$ would correspond to a rooted path on $\tr_p$ whose length is a multiple of $n$. When $n=2$ and $p=\yon+1$, some rooted paths in $\tr_p$ have odd lengths.

§.§ Some categorical properties of cofree comonoids

For every polynomial $p$, the cofree category $\cofree{p}$ is free on a graph. That is, there is a graph $G_p$ whose associated free category in the usual sense (the category of vertices and paths in $G_p$) is isomorphic to $\cofree{p}$.

For vertices, we let $V_p$ denote the set of $p$-trees,

\[V_p\coloneqq\tr_p(\1).\]

For arrows we use the counit lens $\pi\colon\tr_p\to p$ from <ref> to define

\[
\]

In other words $A_p$ is the set $\{d\in p[\pi_1(t)]\,\mid\,t\in\tr_p\}$ of directions in $p$ that emanate from the root corolla of each $p$-tree. The source of $(t,d)$ is $t$ and the target is $\cod(\pi^\sharp_t(d))$. It is clear that every morphism in $\cofree{t}$ is the composite of a finite sequence of such morphisms, completing the proof.

Let $p$ be a polynomial and $\cofree{p}$ the cofree comonoid. Every morphism in $\cat{C}_p$ is both monic and epic.

The free category on a graph always has this property, so the result follows from <ref>.

The additive monoid $\yon^\nn$ of natural numbers has a $\times$-monoid structure in $\smcat^\sharp$.

The right adjoint $p\mapsto\cofree{p}$ preserves products, so $\yon^{\List(\ord{n})}\cong\cofree{\yon^{\ord{n}}}$ is the $n$-fold product of $\yon^\nn$ in $\smcat^\sharp$. We thus want to find cofunctors $e\colon \yon\to\yon^\nn$ and $m\colon\yon^{\List(\2)}\to\yon^\nn$ that satisfy the axioms of a monoid.

The unique lens $\yon\to\yon^\nn$ is a cofunctor (it is the mate of the identity $\yon\to\yon$). We take $m$ to be the mate of the lens $\yon^{\List(\2)}\to\yon$ given by the list $[1,2]$. One can check by hand that these definitions make $(\yon^\nn,e,m)$ a monoid in $(\smcat^\sharp,\yon,\times)$.

Recall from <ref> that an arrow field of a category $\cat{C}$ is a cofunctor $\cat{C}\cof\yon^\nn$.

For any category $\cat{C}$, the set $\smcat^\sharp(\cat{C},\yon^\nn)$ of arrow fields has the structure of a monoid. Moreover, this construction is functorial

\[\smcat^\sharp(-,\yon^\nn)\colon\smcat^\sharp\to\Cat{Mon}\op\]

We saw that $\yon^\nn$ is a monoid object in <ref>.

A cofunctor $\cat{C}\cof\yon^\nn$ is a policy in $\cat{C}$: it assigns an outgoing morphism to each object of $\cat{C}$. Any two such trajectories can be multiplied: we simply do one and then the other; this is the monoid operation. The policy assigning the identity to each object is the unit of the monoid.

We use the notation $\cat{C}\mapsto\vec{\cat{C}}$ for the monoid of arrow fields.

The arrow fields functor

\[\smcat^\sharp\to\Cat{Mon}\op\]

is right adjoint to the inclusion $\Cat{Mon}\op\to\smcat^\sharp$ from <ref>.

Let $\cat{C}$ be a category and $(M,e,*)$ a monoid. A cofunctor $F\colon\cat{C}\cof\yon^M$ has no data on objects; it is just a way to assign to each $c\in \cat{C}$ and $m\in M$ a morphism $F^\sharp_c(m)\colon c\to c'$ for some $c'\coloneqq\cod(F^\sharp_c(m))$. This assignment must send identities to identities and composites to composites: given $m'\in M$ we have $F^\sharp_c(m\then m')=F^\sharp_c(m)\then F^\sharp_{c'}(m')$. This is exactly the data of a monoid morphism $M\to \vec{\cat{C}}$: it assigns to each $m\in M$ an arrow field $\cat{C}$, preserving unit and multiplication.

There is a commutative square of left adjoints

\[
\begin{tikzcd}
\Cat{Mon}\op\ar[r, "U"]\ar[d, "\yon^-"']&
\smset\op\ar[d, "\yon^-"]\\
\smcat^\sharp\ar[r, "U"']&
\poly
\end{tikzcd}
\]

where the functors denoted $U$ are forgetful functors.

Using the fully faithful functor $\yon^-\colon\Cat{Mon}\op\fromto\smcat^\sharp$ from <ref>, it is easy to check that the above diagram commutes.

The free-forgetful adjunction $\smset\fromto\Cat{Mon}$ gives an opposite adjunction $\smset\op\fromto\Cat{Mon}\op$, where $U$ is now left adjoint. We saw that $\yon^-\colon\smset\op\to\poly$ is a left adjoint in <ref>, that $U\colon\smcat^\sharp\to\poly$ is a left adjoint in <ref>, and that $\yon^-\colon\Cat{Mon}\to\smcat^\sharp$ is a left adjoint in <ref>.

§ MORE CATEGORICAL PROPERTIES OF $\SMCAT^\SHARP$

Many of the properties of $\poly$ we covered in <ref> have analogues in $\smcat^\sharp$; we review these here.

§.§ Other special comonoids and adjunctions

We begin by highlighting a few other adjunctions involving $\smcat^\sharp$, as well as the special comonoids in $\smcat^\sharp$ they provide.

The functor $\yon^-$ from <ref> factors through an isomorphism of categories

\[
\smcat^\sharp_{\text{rep}}\iso\Cat{Mon}\op,
\]

where $\Cat{Mon}$ is the category of monoids and monoid homomorphisms and  $\smcat^\sharp_{\text{rep}}$ is the full subcategory of $\smcat^\sharp$ consisting of categories with representable carriers $\yon^M$ for some $M\in\smset$.

Let $\cat{C}$ be a category. It has only one object iff its carrier $\car{c}$ has only one position, i.e. $\car{c}\cong\yon^M$ for some $M\in\smset$, namely where $M$ is the set of morphisms in $\cat{C}$. It remains to show that cofunctors between monoids are dual—opposite—to morphisms between monoids.

A cofunctor $f\colon\yon^M\to\yon^N$ involves a single function $f^\sharp\colon N\to M$ that must satisfy a law coming from unitality and one coming from composition, as in <ref>. The result can now be checked by hand, or seen formally as follows. Each object in the two diagrams of (<ref>) is representable by <ref>. The Yoneda embedding $\smset\op\to\poly$ is fully faithful, so these two diagrams are equivalent to the unit and composition diagrams for monoid homomorphisms.

Let $\smcat^\sharp_{\text{lin}}$ be the full subcategory of $\smcat^\sharp$ consisting of categories with linear carriers $S\yon$ for some $S\in\smset$.
Show that there is an isomorphism of categories

\[
\smcat^\sharp_{\text{lin}}\iso\smset.=
\]

A category $S\yon$ with linear carrier is a discrete category on $S$, so we need to show that a cofunctor between the discrete category on $S$ and the discrete category on $T$ is the same thing as a function $S\to T$. But this is clear: a cofunctor $S\yon\to T\yon$ is a function $S\to T$ on objects and a function backwards on morphisms, and the latter is unique because each object in $S\yon$ has a unique outgoing morphism.

The inclusion $\smcat^\sharp_{\text{lin}}\to\smcat^\sharp$ has a left adjoint sending each $(\car{c},\epsilon,\delta)\in\smcat^\sharp$ to the unique comonoid carried by $(\car{c}\tri\1)\yon$ in $\smcat^\sharp_{\text{lin}}$.

We need to show that for any comonoid $(\car{c},\epsilon,\delta)$ and set $A$, we have a natural isomorphism

\[
\smcat^\sharp(\car{c},A\yon).
\cong^?
\smcat^\sharp((\car{c}\tri\1)\yon,A\yon)
\]

But every morphism in $A\yon$ is an identity, so the result follows from the fact that every cofunctor must pass identities back to identities.

§.§ Vertical-cartesian factorization of cofunctors

A cofunctor is called cartesian if the underlying lens $f\colon\car{c}\to\car{d}$ is cartesian (i.e. for each position $i\in\car{c}(\1)$, the map $f^\sharp_i\colon\car{d}[f_1(i)]\to\car{c}[i]$ is an isomorphism).

Every cofunctor $f\colon\cat{C}\cof\cat{D}$ factors as a vertical morphism followed by a cartesian morphism

\[
\cat{C}\overset{\text{vert}}{\cof}\cat{C}'\overset{\text{cart}}{\cof}\com{D}.
\]

A cofunctor $\cat{C}\cof\cat{D}$ is a lens $\car{c}\to\car{d}$ satisfying some properties, and any lens $f\colon\car{c}\to\car{d}$ can be factored as a vertical morphism followed by a cartesian morphism

\[
\car{c}\To{g}\car{c'}\To{h}\car{d}.
\]

For simplicity, assume $g_1\colon\car{c}(\1)\to\car{c'}(\1)$ is identity (rather than merely isomorphism) on positions and similarly that for each $i\in\car{c}$ the map $h^\sharp_i\colon\car{c'}[i]\to\car{d}[h_1(i)]$ is identity (rather than merely isomorphism) on directions.

It suffices to show that the intermediate object $\car{c'}$ can be endowed with the structure of a category such that $g$ and $h$ are cofunctors. Given an object $i\in\car{c'}(\1)$, assign its identity to be the identity on $h_1(i)=f(i)$; then both $g$ and $h$ preserve identities because $f$ does. Given an emanating morphism $m\in\car{c'}[i]=\car{d}[f(i)]$, assign its codomain to be $\cod(m)\coloneqq\cod(f^\sharp_i(m))$, and given an emanating morphism $m'\in\car{c'}[\cod(m)]$, assign the composite $m\then m'$ in $\car{c'}$ to be $m\then m'$ in $\car{d}$. In <ref> we will check that with these definitions, $\car{c'}$ is a category and both $g$ and $h$ are cofunctors.

We will complete the proof of <ref>, using the same notation.

* Show that composition is associative and unital in $\car{c'}$.

* Show that $g$ preserves codomains.

* Show that $g$ preserves compositions.

* Show that $h$ preserves codomains.

* Show that $h$ preserves compositions.

* Given an object $i\in\car{c'}(1)=\car{c}(1)$, the set of emanating morphisms is $\car{c'}[i]\coloneqq\car{d}[fi]$, and they compose according to the structure of $\car{d}$. Since morphisms in $\car{d}$ compose associatively and unitaly, so do morphisms in $\car{c'}$.

* Given $i\in\car{c}(1)$ and $m\in \car{c'}[i]=\car{d}[fi]$, we have $g(\cod(g^\sharp_i(m)))=\cod(g^\sharp_i(m))=\cod(f^\sharp_i(m))=\cod(m)$ by definition.

* For any $i\in\car{c'}(1)$, the lens $g^\sharp_i$ preserves compositions of morphisms in $\car{c'}[i]=\car{d}[fi]$ because it agrees with $f^\sharp_i$, which preserves compositions.

* Given $i\in\car{c'}(1)$ and $m\in\car{d}[hi]$, we have $h(\cod(h^\sharp_i(m)))=f(\cod(f^\sharp_i(m)))=m$.

* The map $h^\sharp_i$ was chosen to be the identity for each $i$, so it certainly preserves compositions.

The wide
[A subcategory $\Cat{D}$ of a category $\Cat{C}$ is wide if every object of $\Cat{C}$ is in $\Cat{D}$.]
subcategory of cartesian cofunctors in $\smcat^\sharp$ is isomorphic to the wide subcategory of discrete opfibrations in $\smcat$.

Suppose that $\cat{C}$ and $\cat{D}$ are categories. Both a functor and a cofunctor between them involve a map on objects, say $f\colon\Ob\cat{C}\to\Ob\cat{D}$. For any object $c\in\Ob\cat{C}$, a functor gives a function, say $f_\sharp\colon\cat{C}[c]\to\cat{D}[f(c)]$ whereas a cofunctor gives a function $f^\sharp\colon\cat{D}[f(c)]\to\cat{C}[c]$. The cofunctor is cartesian iff $f^\sharp$ is an iso, and the functor is a discrete opfibration iff $f_\sharp$ is an iso. We thus transform our functor into a cofunctor (or vice versa) by taking the inverse function on morphisms. It is easy to check that this inverse appropriately preserves identities, codomains, and compositions.

The wide subcategory of vertical maps in $\smcat^\sharp$ is isomorphic to the opposite of the wide subcategory bijective-on-objects maps in $\smcat$:

\[
\smcat^\sharp_{\text{vert}}\cong(\smcat_{\text{boo}})\op.
\]

Let $\cat{C}$ and $\cat{D}$ be categories. Given a vertical cofunctor $F\colon\cat{C}\cof\cat{D}$, we have a bijection $F_1\colon\Ob\cat{C}\to\Ob\cat{D}$; let $G_1$ be its inverse. We define a functor $G\colon\cat{D}\to\cat{C}$ on objects by $G_1$ and, for any $f\colon d\to d'$ in $\cat{D}$ we define $G(f)\coloneqq F^\sharp_{G_1(d)}$. It has the correct codomain: $\cod(G(f))=G_1(F_1(\cod(G(f)))=G_1(\cod f)$. And it sends identities and compositions to identities and compositions by the laws of cofunctors.

The construction of a vertical cofunctor from a bijective-on-objects functor is analogous, and it is easy to check that the two constructions are inverses.

Let $S$ be a set and consider the state category $\cat{S}\coloneqq(S\yon^S,\epsilon,\delta)$. Use <ref> to show that categories $\cat{C}$ equipped with a vertical cofunctor $\cat{S}\cof\cat{C}$ can be identified with categories whose set of objects has been identified with $S$.

The category corresponding to $S\yon^S$ is the contractible groupoid $K_s$ on $S$. A vertical cofunctor $K_S\cof\cat{C}$ includes a bijection on objects, so we can assume that $\Ob(\cat{C})=S$. But the rest of the cofunctor assigns to each map $s_1\to s_2$ in $\cat{C}$ some choice of morphism $s_1\to s_2$ in $K_S$, and there is exactly one. Thus the cofunctor includes no additional data.

Consider the categories $\cat{C}\coloneqq\fbox{$\bullet\tto\bullet$}$ and $\cat{D}\coloneqq\fbox{$\bullet\to\bullet$}$. There is a unique bijective-on-objects (boo) functor $F\colon\cat{C}\to\cat{D}$ and two boo functors $G_1,G_2\colon\cat{D}\to\cat{C}$. These have corresponding cofunctors going the other way.

* Write down the morphism $\car{d}\to\car{c}$ of carriers corresponding to $F$.

* Write down the morphism $\car{c}\to\car{d}$ of carriers corresponding to either $G_1$ or $G_2$.

Let's take the two nonidentity arrows in $\cat{C}$ to be labeled $s,t$ and the unique nonidentity arrow in $\cat{D}$ to be labeled $f$. Then the carrier of $\cat{C}$ is $\car{c}\coloneqq\yon^{\{\id_1,s,t\}}+\yon^{\{\id_2\}}$ and that of $\cat{D}$ is $\car{d}\coloneqq\yon^{\{\id_1,f\}}+\yon^{\{\id_2\}}$.

* The boo functor $F\colon\cat{C}\to\cat{D}$ can be identified with a vertical cofunctor $\car{d}\to\car{c}$ that sends back $\id_1\mapsto\id_1$ and $s\mapsto f$ and $t\mapsto f$ and $\id_2\mapsto\id_2$.

* For $G_1\colon\cat{D}\to\cat{C}$, which we take to send $f\mapsto s$, the corresponding vertical cofunctor $\car{c}\to\car{d}$ sends back $\id_1\mapsto\id_1$ and $f\mapsto s$ and $\id_2\mapsto\id_2$.

We record the following proposition here.

If $\varphi\colon p\to q$ is a cartesian lens, then $\cofree{\varphi}\colon\cofree{p}\to\cofree{q}$ is a cartesian cofunctor: that is, for each $t\in\tr_p$, the on-morphisms function

\[
\left(\cofree{\varphi}\right)^\sharp_t\colon\cofree{q}[\cofree{\varphi}t]\To{\iso}\cofree{p}[t]
\]

is a bijection.

Given $\varphi\colon p\to q$ cartesian, each tree $T\in\tr_p$ is sent to a tree in $\tr_q$ with the same branching profile. A morphism emanating from it is just a finite rooted path, and the set of these is completely determined by the branching profile. Thus we have the desired bijection.

§.§ Limits and colimits of comonoids

We saw in <ref> that $\poly$ has all small limits and colimits.
It turns out that $\smcat^\sharp$ has all small limits and colimits as well.
We start by discussing colimits in $\smcat^\sharp$, as they are somewhat easier to get a handle on.

§.§.§ Colimits in $\smcat^\sharp$

It is a consequence of the forgetful-cofree adjunction from <ref> that $\smcat^\sharp$ inherits all the colimits from $\poly$.
As these results are somewhat technical, relying on a property of functors known as comonadicity, we defer their proofs to references.

The forgetful functor $\smcat^\sharp\to\poly$ is comonadic.

The fact that a forgetful functor $\smcat^\sharp\iso\Cat{Comon}(\poly)\to\poly$ is comonadic if it has a right adjoint follows from Beck's monadicity theorem via a straightforward generalization of an argument given by Paré in <cit.>, as pointed out by Porst in <cit.>.
So the result follows from <ref>.

The category $\smcat^\sharp$ has all small colimits.
They are created by the forgetful functor $\smcat^\sharp\to\poly$.

A comonadic functor creates all colimits that exist in its codomain (see <cit.>), and by <ref>, the category $\poly$ has all small colimits.

[Coproducts in $\smcat^\sharp$]
Probably the most familiar kind of colimit in $\smcat^\sharp$ is the coproduct, as <ref> tells us that it agrees with the usual coproduct from $\smcat$.
Here's why.

For concreteness, let $I$ be a set and $(\cat{C}_i)_{i\in I}$ be categories with carriers $(\car{c}_i)_{i\in I}$.
Then the coproduct of $(\cat{C}_i)_{i\in I}$ in $\smcat$ is the category $\sum_{i\in I}\cat{C}_i$, whose objects are given by the disjoint union of the objects in each summand, so that

\[
\Ob\left(\sum_{i\in I}\cat{C}_i\right)\iso\sum_{i\in I}\Ob\cat{C}_i=\sum_{i\in I}\car{c}_i(\1)\iso\left(\sum_{i\in I}\car{c}_i\right)(\1),
\]

and whose morphisms out of each $c\in\Ob\cat{C}_j\ss\Ob\sum_{i\in I}\cat{C}_i$ are just the morphisms out of $c$ in the summand $\cat{C}_j$, so

\[
\left(\sum_{i\in I}\cat{C}_i\right)[c]\iso\cat{C}_j[c]=\car{c}_j[c]\iso\left(\sum_{i\in I}\car{c}_i\right)[c]
\]

Hence $\sum_{i\in I}\cat{C}_i$ is carried by the coproduct of polynomials $\sum_{i\in I}\car{c}_i$.

It remains to show that $\sum_{i\in I}\cat{C}_i$ is also the coproduct of $(\cat{C}_i)_{i\in I}$ in $\smcat^\sharp$.
We already know from <ref> that it has the right carrier: the coproduct of carriers $\sum_{i\in I}\car{c}_i$. It also has the right morphisms, for any object $(i,x)$ with $x\in\car{c}_i(1)$, the set of emanating morphisms is—and should be—$\car{c}_i[x]$.

* Show that $\0$ has a unique comonoid structure.

* Explain why $\0$ with its comonoid structure is initial in $\smcat^\sharp$ in two ways: by explicitly showing it has the required universal property, or by invoking <ref>.

* We actually already showed that $\0$ has a unique comonoid structure, corresponding to the empty category (which we will also denote by $\0$), in <ref>, for the case of $S\coloneqq\0$.

* We show that $\0$ has the universal property of the initial object in $\smcat^\sharp$ as follows.
For any category $\cat{D}$, there is a unique cofunctor $\0\cof\cat{D}$: it vacuously sends each object in $\0$ to an object in $\cat{D}$, and since there are no objects in $\0$, it does nothing to morphisms.

Alternatively, we know by <ref> that $\smcat^\sharp$ has an initial object, and that the forgetful functor $\smcat^\sharp\to\poly$ sends it to the initial object in $\poly$, which is $\0$ (by <ref> and the following discussion).
So the initial object in $\smcat^\sharp$ must be the unique comonoid carried by $\0$.

Given a comonoid $(\car{c},\epsilon,\delta)\in\smcat^\sharp$, show that there is an induced comonoid structure on the polynomial $\2\car{c}$.

The coproduct of $\car{c}$ with itself is again a comonoid (as a category it is the disjoint union of $\car{c}$ with itself) and it has the right carrier polynomial, since the carrier functor $U\colon\smcat^\sharp\to\poly$ is a left adjoint.

§.§.§ Limits in $\smcat^\sharp$

As in the case of colimits, there is a rather technical result showing that the forgetful-cofree adjunction implies the existence of all small limits of comonoids, which we summarize here.

The category $\smcat^\sharp$ has all small limits.

By <ref>, the forgetful functor $U\colon\smcat^\sharp\to\poly$ has a right adjoint, and by <ref>, $\poly$ itself has all small limits.
Furthermore equalizers in $\poly$ are connected limits, so by <ref>, they are preserved by $\tri$ on either side.
Then the result follows from <cit.>.

§.§ Parallel product comonoids

The usual product of categories is not the categorical product in $\smcat^\sharp$.
It is, however, a monoidal product on $\smcat^\sharp$, coinciding with the parallel product $\otimes$ on $\poly$.

The parallel product $(\yon,\otimes)$ on $\poly$ extends to a monoidal structure $(\yon,\otimes)$ on $\smcat^\sharp$, such that the forgetful functor
is strong monoidal with respect to $\otimes$.
The parallel product of two categories is their product in $\smcat$.

Let $\cat{C},\cat{D}\in\smcat^\sharp$ be categories corresponding to comonoids $(\car{c},\epsilon_{\car c},\delta_{\car c})$ and $(\car{d},\epsilon_{\car d},\delta_{\car d})$.

The carrier of $\cat{C}\otimes\cat{D}$ is defined to be $\car{c}\otimes\car{d}$. A position in it is a pair $(c,d)$ of objects, one from $\cat{C}$ and one from $\cat{D}$; a direction there is a pair $(f,g)$ of a morphism emanating from $c$ and one emanating from $d$.

We define $\epsilon_{\cat{C}\otimes\cat{D}}\colon\car{c}\otimes\car{d}\to\yon$ as

\[
\car{c}\otimes\car{d}\To{\epsilon_{\car{C}}\otimes\epsilon_{\car{D}}}\yon\otimes\yon\cong\yon.
\]

This says that the identity at $(c,d)$ is the pair of identities.

We define $\delta_{\cat{C}\otimes\cat{D}}\colon(\car{c}\otimes\car{d})\to(\car{c}\otimes\car{d})\tri(\car{c}\otimes\car{d})$ using the duoidal property:

\[
\car{c}\otimes\car{d}\To{\delta_{\car{c}}\otimes\delta_{\car{d}}}(\car{c}\tri\car{c})\otimes(\car{d}\tri\car{d})\to(\car{c}\otimes\car{d})\tri(\car{c}\otimes\car{d}).
\]

One can check that this says that codomains and composition are defined coordinate-wise, and that $(\car{c}\otimes\car{d},\epsilon_{\car{c}\otimes\car{d}},\delta_{\car{c}\otimes\car{d}})$ forms a comonoid. One can also check that this is functorial in $\cat{C},\cat{D}\in\smcat^\sharp$. See <ref>.

We complete the proof of <ref>.

* Show that $(\car{c}\otimes\car{d},\epsilon_{\car{c}\otimes\car{d}},\delta_{\car{c}\otimes\car{d}})$, as described in <ref>, forms a comonoid.

* Check that the construction $(\cat{C},\cat{D})\mapsto\cat{C}\otimes\cat{D}$ is functorial in $\cat{C},\cat{D}\in\smcat^\sharp$.

* The highbrow way to check that $\car{c}\otimes\car{d}$ forms a comonoid is to say that

\[\otimes\colon(\poly,\yon,\tri)\times(\poly,\yon,\tri)\too(\poly,\yon,\tri)\]

is a colax monoidal functor, so it sends comonoids to comonoids. A lowbrow way to check it is to see that the category corresponding to $\car{c}\otimes\car{d}$ is just the usual cartesian product $\cat{C}\times\cat{D}$ in $\smcat$. This is a category, hence a comonoid in $\poly$.

* Because $\otimes$ is symmetric, it suffices to show that for any cofunctor $\varphi\colon\cat{C}\cof\cat{C}'$, there is an induced cofunctor $\varphi\otimes\cat{D}\colon\cat{C}\otimes\cat{D}\cof\cat{C}'\otimes\cat{D}$.

The cofree construction works nicely with this monoidal product.

The cofree functor $p\mapsto\cofree{p}$ is lax monoidal; in particular there is a lens $\yon\to\car{t}_\yon$, and for any $p,q\in\poly$ there is a natural lens

\[
\car{t}_p\otimes\car{t}_q\to\car{t}_{p\otimes q}.
\]

satisfying the usual conditions.

By <ref>, the left adjoint $U\colon\smcat^\sharp\to\poly$ is strong monoidal. A consequence of Kelly's doctrinal adjunction theorem <cit.> says that the right adjoint of an oplax monoidal functor is lax monoidal.

* What polynomial is $\car{t}_\yon$?

* What is the lens $\yon\to\car{t}_\yon$ from <ref>?

* Explain in words how to think about the lens $\car{t}_p\otimes\car{t}_q\to\car{t}_{p\otimes q}$ from <ref>, for arbitrary $p,q\in\poly$.

* The carrier of $\cofree{\yon}$ is $\car{t}_\yon\coloneqq\yon^\nn$.

* The lens $\yon\to\car{t}\yon$ is the unique lens.

* Given a $p$-tree $T$ and a $q$-tree $U$, we get a $(p\otimes q)$-tree by having its root be labeled by the pair of root labels for $T$ and $U$, and for each child there—the set of which is the set of pairs consisting of a child in $T$ and a child in $U$—recursively using the above formula to combine these two children.

§ COMODULES OVER POLYNOMIAL COMONOIDS

Just as we can define a category of comonoids within any monoidal category, we can further define a notion of comodules over such comonoids.
And much like how polynomial comonoids are categories, these comodules can also be described in categorical terms we are already familiar with.
There is much more to say about comodules over polynomial comonoids than we have room for here—we will merely give a glimpse of the theory and applications.

§.§ Left and right comodules

When the monoidal category is not symmetric, left comodules and right comodules may differ significantly, so we define them separately (but notice that the diagrams for one are analogous to the diagrams for the other).

In a monoidal category $(\Cat{C},\yon,\tri)$, let $\cat{C}=(\car{c},\epsilon,\delta)$ be a comonoid.
A left $\cat{C}$-comodule is

* an object $m\in\Cat{C}$, called the carrier, equipped with

* a morphism $\car{c}\tri m\From{\lambda}m$ called the left coaction,

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

\begin{equation} \label{eqn.left_comod_laws}
\begin{tikzcd}[ampersand replacement=\&]
\car{c}\tri m\ar[d, "\epsilon\:\tri\:m"']\&
m\ar[l, "\lambda"']\ar[dl, equal, bend left]\\
\end{tikzcd}
\hspace{.6in}
\begin{tikzcd}[ampersand replacement=\&]
\car{c}\tri m\ar[d, "\delta\:\tri\:m"']\&
m\ar[l, "\lambda"']\ar[d, "\lambda"]\\
\car{c}\tri\car{c}\tri m\&
\car{c}\tri m\ar[l, "\car{c}\:\tri\:\lambda"]
\end{tikzcd}
\end{equation}

When referring to a left $\cat{C}$-comodule, we may omit its coaction if it can be inferred from context (or simply unspecified), identifying the comodule with its carrier.

A morphism of left $\cat{C}$-comodules $m$ and $n$ is a morphism $\alpha\colon m\to n$ such that the following diagram commutes:

\[
\begin{tikzcd}
\car{c}\tri m \ar[d, "\car{c}\:\tri\:\alpha"'] &
m \ar[l] \ar[d, "\alpha"] \\
\car{c}\tri n &
n \ar[l]
\end{tikzcd}
\]

Here the top and bottom morphisms are the left coactions of $m$ and $n$.

Show that the category of $\cat{C}$-coalgebras from <ref> is exactly the category of constant left $\cat{C}$-comodules—i.e. the full subcategory of the category of left $\cat{C}$-comodules spanned by those left $\cat{C}$-comodules whose carriers are constant polynomials.

In <ref>, if the carrier of the left $\cat{C}$-comodule is always chosen to be a constant polynomial, i.e. a set, then we recover <ref>.
Hence constant left $\cat{C}$-comodules are precisely left $\cat{C}$-coalgebras; their notions of morphisms coincide as well, so the categories they form are isomorphic.

In a monoidal category $(\Cat{C},\yon,\tri)$, let $\cat{D}=(\car{d},\epsilon,\delta)$ be a comonoid.
A right $\cat{D}$-comodule is

* an object $m\in\Cat{C}$, called the carrier, equipped with

* a morphism $m\To{\rho}m\tri\car{d}$ called the right coaction,

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

\begin{equation} \label{eqn.right_comod_laws}
\begin{tikzcd}[ampersand replacement=\&]
m\ar[r, "\rho"]\ar[dr, equal, bend right]\&
m\tri\car{d}\ar[d, "m\:\tri\:\epsilon"]\\\&
\end{tikzcd}
\hspace{.6in}
\begin{tikzcd}[ampersand replacement=\&]
m\ar[r, "\rho"]\ar[d, "\rho"']\&
m\tri\car{d}\ar[d, "m\:\tri\:\delta"]\\
m\tri\car{d}\ar[r, "\rho\:\tri\:\car{d}"']\&
\end{tikzcd}
\end{equation}

When referring to a right $\cat{D}$-comodule, we may omit its coaction if it can be inferred from context (or unspecified), identifying the comodule with its carrier.

A morphism of right $\cat{D}$-comodules $m$ and $n$ is a morphism $\alpha\colon m\to n$ such that the following diagram commutes:

\[
\begin{tikzcd}
m \ar[r] \ar[d, "\alpha"'] &
m\tri\car{d} \ar[d, "\alpha\:\tri\:\car{d}"] \\
n \ar[r] &
\end{tikzcd}
\]

Here the top and bottom morphisms are the right coactions of $m$ and $n$.

* Draw the equations of (<ref>) using polyboxes.

* Draw the equations of (<ref>) using polyboxes.

* Here is the first equation in terms of polyboxes:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$m$" left] (l) {$x$\at$a\vphantom{a}$};
\node[poly, cod, "$m$" right, right=of l] (r) {$x$\at$a$};
\draw[double,-] (l_pos) -- (r_pos);
\draw[double,-] (r_dir) -- (l_dir);
\node[poly, dom, right=2.5 of r, "$m$" left] (p) {$\lambda^\sharp_a(\id_{|a|},x)$\at$a$};
\node[poly, right=2.2cm of p.south, yshift=-1.25ex] (r') {$\id_{|a|}$\at$|a|$};
\node[poly, cod, above=of r', "$m$" right] (q) {$x$\at$a.\id_{|a|}$};
\draw (p_pos) to[first] (r'_pos);
\draw (r'_dir) to[climb] node[left] {$\lambda$} (q_pos);
\draw (q_dir) to[last] (p_dir);
\draw (r'_pos) to[climb'] node[right] {$\epsilon_\car{c}$} (r'_dir);
\node at ($(r.east)!.5!(p.west)$) {$=$};
\end{tikzpicture}
\]

The equation says that for any $a\in m(1)$ we have $a=a.\id_{|a|}\coloneqq\lambda(a,\id_{|a|})$ and that for any $x\in m[a]$ we have $x=x'\coloneqq\lambda^\sharp_a(\id_{|a|},x)$.

Here is the second equation in terms of polyboxes:

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

These say that $\cod(f)=|a.f|$, that $a.(f\then f')=(a.f).f'$, and that $\lambda^\sharp_a((f\then f'),x)=\lambda^\sharp_a(f,\lambda^\sharp_{a.f}(f',x))$.

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$m$" left] (l) {$x$\at$a\vphantom{a}$};
\node[poly, cod, "$m$" right, right=of l] (r) {$x$\at$a$};
\draw[double,-] (l_pos) -- (r_pos);
\draw[double,-] (r_dir) -- (l_dir);
\node[poly, dom, right=2.5 of r, "$m$" left] (p) {$\rho^\sharp_a(x,\id_{|a'.x|})$\at$a$};
\node[poly, cod, right=2.5cm of p.south, yshift=-1.25ex, "$m$" right] (r') {$x$\at$a'$};
\node[poly, above=of r'] (q) {$\id_{|a'.x|}$\at$|a'.x|$};
\draw (p_pos) to[first] (r'_pos);
\draw (r'_dir) to[climb] node[left] {$\rho$} (q_pos);
\draw (q_dir) to[last] (p_dir);
\draw (q_pos) to[climb'] node[right] {$\epsilon_\car{d}$} (q_dir);
\node at ($(r.east)!.5!(p.west)$) {$=$};
\end{tikzpicture}
\]

The equation says that for any $a\in m(1)$ we have $a=a'\coloneqq\rho_1(i)$ and that for any $f\in m[a]$ we have $x=\rho^\sharp_a(x,\id_{|a'.x|})$.

Here is the second equation in terms of polyboxes:

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$m$" left] (m') {$\rho^\sharp_a(\rho_a^\sharp(x,g),g')$\at$a$};
\node[poly, right=2.7 of m'.south, yshift=-1ex, "$m$" below] (mm') {$\rho^\sharp_i(x,g)$\at$a$};
\node[poly, above=of mm', "$\car{d}$" above] (C') {$g'$\at$|a.\rho^\sharp_a(x,g)|$};
\node[poly, cod, right=2 of mm'.south, yshift=-1ex, "$m$" right] (D') {$x$\at$a$};
\node[poly, cod, above=of D', "$\car{d}$" right] (mmm') {$g$\at$|a.x|$};
\node[poly, cod, above=of mmm', "$\car{d}$" right] (CC') {$g'$\at$|a.\rho^\sharp_a(x,g)|$};
\draw[double,-] (m'_pos) to[first] (mm'_pos);
\draw (mm'_dir) to[climb] node[left] {$\rho$}  (C'_pos);
\draw (C'_dir) to[last]  (m'_dir);
\draw[double,-] (mm'_pos) to[first] (D'_pos);
\draw (D'_dir) to[climb] node[left] {$\rho$} (mmm'_pos);
\draw (mmm'_dir) to[last] (mm'_dir);
\draw[double,-] (C'_pos) to[first] (CC'_pos);
\draw[double,-] (CC'_dir) to[last] (C'_dir);
\end{tikzpicture}
\node (p2) [below=1 of p1] {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$m$" left] (m) {$\rho^\sharp_a(x,(g\then g'))$\at$a$};
\node[poly, right=2.5 of m.south, yshift=-1ex, "$m$" below] (D) {$x$\at$a$};
\node[poly, above=of D, "$\car{d}$" above] (mm) {$g\then g'$\at$|a.x|$};
\node[poly, cod, right=2 of D.south, yshift=-1ex, "$m$" right] (DD) {$x$\at$a$};
\node[poly, cod, above=of DD, "$\car{d}$" right] (mmm) {$g$\at$|a.x|$};
\node[poly, cod, above=of mmm, "$\car{d}$" right] (C) {$g'$\at$\cod g$};
\draw[double,-] (m_pos) to[first] (D_pos);
\draw (D_dir) to[climb]  node[left] {$\rho$} (mm_pos);
\draw (mm_dir) to[last] (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[left] {$\delta$} (C_pos);
\draw (C_dir) to[last] (mm_dir);
\end{tikzpicture}
\node at ($(p1.south)!.5!(p2.north)$) {$=$};
\end{tikzpicture}
\]

These equations say that $\cod(g)=|a.\rho^\sharp_a(x,g)|$ and that $\rho_a^\sharp(\rho_a^\sharp(x,g),g')=\rho^\sharp_a(x,(g\then g'))$.

Recall from <ref> that $\yon$ has a unique category structure.

* Show that the category of left $\yon$-comodules is isomorphic to $\poly$.

* Show that the category of right $\yon$-comodules is isomorphic to $\poly$. If it is similar, just say “similar”; if not, explain.

The comonoid structure on $\yon$ has $\epsilon\colon\yon\to\yon$ and $\delta\colon\yon\to\yon\tri\yon=\yon$ the unique lenses.

* We first show that for any polynomial $m$, there is a unique $\yon$-comodule structure on $m$. By (<ref>), a $\yon$-comodule structure is a lens $\lambda\colon m\to\yon\tri m=m$ such that $\lambda\then(!\tri m)=\id_m$, but $!\tri m=\id_m$, so $\lambda=\id_m$ is forced. A morphism $(m,\id)\to(n,\id_n)$ of $\yon$-comodules is also easily seen to be just a lens $m\to n$.

* Similar.

We can characterize left comodules as something far more familiar.

Let $\cat{C}$ be a category.
The category of left $\cat{C}$-comodules is equivalent to the category of functors $\cat{C}\to\poly$.

Let $\car{c}$ be the carrier of $\cat{C}$. Given a left $\cat{C}$-comodule $m\to \car{c}\tri m$, we saw in <ref> that there is an induced function $|-|\colon m(1)\to\car{c}(\1)$, so to each object $i\in\Ob(\cat{C})$ we can associate a set $P^m_i\coloneqq\{a\in m(\1)\mid |a|=i\}$. We also have for each $a\in P_i\ss m(\1)$ a set $m[a]$, and so we can consider the polynomial

\[
p^m_i\coloneqq\sum_{a\in P^m_i}\yon^{m[a]}.
\]

The polynomial $p^m_i\in\poly$ is easily seen to be functorial in the comodule $m$. Moreover, given a morphism $f\colon i\to i'$ in $\cat{C}$, we have for each $a\in p^m_i(1)$ an element $a.f\in m(1)$, with $|a.f|=i'$, i.e. $a.f\in  P^m_{i'}=p^m_{i'}(\1)$. Similarly for each $x\in m[a.f]=p^m_{i'}[a.f]$ we have $\lambda_a^\sharp(f,x)\in m[a]=p^m_i[a]$, and thus we have a lens $p^m_i\to p^m_{i'}$. In this way we have obtained we obtain a functor $p^m_-\colon\cat{C}\to\poly$, and this functor is itself functorial in $m$.

We leave the proof that this construction has an inverse to the reader.

Similarly, a right comodule is not an altogether foreign concept.

Let $\cat{D}$ be a category.
A right $\cat{D}$-comodule $m$ can be identified (up to isomorphism) with a functor $\cat{D}\to\smset^{m(\1)}$.

Let $\car{d}$ be the carrier of $\cat{D}$. Given a right $\cat{D}$-comodule $m\to m\tri\car{d}$ we need a functor $F\colon\cat{D}\times m(1)\to\smset$. We again rely heavily on <ref>.
Given $j\in\cat{D}$ and $a\in m(1)$, define

\[F(j,d)\coloneqq\{x\in m[a]\mid|a.f|=j\}.\]

Given $g\colon j\to j'$ we get $\rho_a^\sharp(x,g)\in m[a]$ with $|a.\rho_a^\sharp(x,g)|=j'$, and thus $g$ induces a function $F(g,d)\colon F(j,d)\to F(j',d)$. Again by laws from <ref> these are functorial in $g$, completing the proof sketch.

Let $\com{C}=(\car{c},\epsilon,\delta)$ be a comonoid in $\poly$. For any set $G$, the polynomial $\yon^G\tri\car{c}$ has a natural right $\com{C}$-comodule structure.

We use the lens $(\yon^G\tri\delta)\colon(\yon^G\tri\car{c})\to(\yon^G\tri\car{c}\tri\car{c})$. It satisfies the unitality and associativity laws because $\car{c}$ does.

We can think of elements of $G$ as “generators”. Then if $i'\colon G\to\car{c}\tri\1$ assigns to every generator an object of a category $\cat{C}$, then we should be able to find the free $\cat{C}$-set that $i'$ generates.

Functions $i'\colon G\to\car{c}\tri\1$ are in bijection with positions $i\in\yon^G\tri\car{c}\tri\1$. Let $m\coloneqq i^*(\yon^G\tri\car{c})$ and let $\rho_i$ be the induced right $\com{C}$-comodule structure.
Then $\rho_i$ corresponds to the free $\cat{C}$-set generated by $i'$.

The polynomial $m$ has the following form:

\[
m\cong\yon^{\sum_{g\in G}\car{c}[i'(g)]}
\]

In particular $\rho_i$ is a representable right $\com{C}$-comodule, and we can identify it with a $\cat{C}$-set by <ref>. The elements of this $\cat{C}$-set are pairs $(g, f)$, where $g\in G$ is a generator and $f\colon i'(g)\to\cod(f)$ is a morphism in $\cat{C}$ emanating from $i'(g)$. It is easy to see that the comodule structure induced by <ref> is indeed the free one.

Let $\cat{C}$ be a category and $i\in\cat{C}$ an object.

* Consider $i$ as a lens $\yon\to\car{c}$.
Show that the vertical-cartesian factorization of this lens is $\yon \to \yon^{\car{c}[i]} \To{\varphi} \car{c}$.

* Use <ref> to show that $\yon^{\car{c}[i]} \tri \car{c} \to \car{c} \tri \car{c}$ is cartesian.

* Show that there is a commutative square

\[
\begin{tikzcd}
\yon^{\car{c}[i]} \ar[r, "\delta^i"] \ar[d, "\varphi"'] & \yon^{\car{c}[i]} \tri \car{c} \ar[d, "\text{cart}"] \\
\car{c} \ar[r, "\delta"'] & \car{c} \tri \car{c} \ar[ul, phantom, very near end, "\lrcorner"]
\end{tikzcd}
\]

* Show that this square is a pullback, as indicated.

* Show that $\delta^i$ makes $\yon^{\car{c}[i]}$ a right $\com{C}$-comodule.

The lens $\delta^i$ can be seen as the restriction of $\delta \colon \car{c} \to \car{c} \tri \car{c}$ to a single starting position.

We can extend this to a functor $\cat{C} \to \bimod{\yon}{\cat{C}}$ that sends the object $i$ to $\yon^{\car{c}[i]}$. Given a morphism $f \colon i \to i'$ in $\cat{C}$, we get a function $\car{c}[i'] \to \car{c}[i]$ given by composition with $f$, and hence a lens $\yon^{\car{c}[f]} \colon \yon^{\car{c}[i]} \to \yon^{\car{c}[i']}$.

* Show that $\yon^{\car{c}[f]}$ is a right $\com{C}$-comodules morphism.

* Show that the construction $\yon^{\car{c}[f]}$ is functorial in $f$.

Let $\car{c}$ be a comonoid. For any set $I$ and right $\car{c}$-comodules $(m_i)_{i\in I}$, the coproduct $m\coloneqq \sum_{i\in I}m_i$ has a natural right-comodule structure. Moreover, each representable summand in the carrier $m$ of a right $\car{c}$-comodule is itself a right-$\car{c}$ comodule and $m$ is their sum.

This follows from the fact in <ref> that $-\tri\car{c}$ commutes with coproduct, i.e. $\left(\sum_{i\in I}m_i\right)\tri\car{c}\cong\sum_{i\in I}(m_i\tri\car{c})$.

If $m\in\poly$ is equipped with both a right $\com{C}$-comodule and a right $\com{D}$-comodule structure, we can naturally equip $m$ with a $(\com{C}\times\com{D})$-comodule structure.

It suffices by <ref> to assume that $m=\yon^M$ is representable. But a right $\com{C}$-comodule with carrier $\yon^M$ can be identified with a cofunctor $M\yon^M\to\com{C}$.

Thus if $\yon^M$ is both a right-$\com{C}$ comodule and a right-$\com{D}$ comodule, then we have comonoid morphisms $\com{C}\from M\yon^M\to\com{D}$. This induces a unique comonoid morphism $M\yon^M\to(\com{C}\times\com{D})$ to the product, and we identify it with a right-$(\com{C}\times\com{D})$ comodule on $\yon^M$.

§.§ Bicomodules

We take special note of any object that is both a left comodule and a right comodule in compatible ways.

In a monoidal category $(\Cat{C},\yon,\tri)$, let $\cat{C}$ and $\cat{D}$ be comonoids with carriers $\car{c}$ and $\car{d}$.
A $(\cat{C},\cat{D})$-bicomodule is

* an object $m\in\Cat{C}$ that is both

* a left $\cat{C}$-comodule, with left coaction $\car{c}\tri m\From{\lambda}m$, and

* a right $\cat{D}$-comodule, with right coaction $m\To{\rho}m\tri\car{d}$,

such that the following diagram, known as the coherence law, commutes:

\begin{equation} \label{eqn.bimod_coherence}
\begin{tikzcd}[sep=small]
& m \ar[dl, "\lambda"'] \ar[dr, "\rho"] & \\
\car{c}\tri m \ar[dr, "\car{c}\:\tri\:\rho"'] & &
m\tri\car{d} \ar[dl, "\lambda\:\tri\:\car{d}"] \\
& \car{c}\tri m\tri\car{d}.
\end{tikzcd}
\end{equation}

We may denote such a bicomodule by $\cat{C}\bimodfrom[m]\cat{D}$ when its left and right coactions have yet to be specified or may be inferred from context—or even by $\car{c}\bimodfrom[m]\car{d}$ when the comonoid structures on $\car{c}$ and $\car{d}$ can be inferred from context as well.
[The notation $\car{c}\bimodfrom\car{d}$ has a mnemonic advantage, as each $\tri$ goes in the correct direction: $\car{c}\tri m\from m$ and $m\to m\tri\car{d}$.
But it also looks like an arrow going backward from $\car{d}$ to $\car{c}$, which will turn out to have a semantic advantage as well.

A morphism of $(\cat{C},\cat{D})$-bicomodules is one that is a morphism of left $\cat{C}$-comodules and a morphism of right $\cat{D}$-comodules.

We draw the commutativity of (<ref>) using polyboxes.

\begin{equation}\label{eqn.bimod_coherence_polybox}
\begin{tikzpicture}[baseline=(current bounding box.center)]
\node (p1) {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$m$" left] (m) {};
\node[poly, right= of m.south, yshift=-1ex, "\tiny$\car{c}$" below] (D) {};
\node[poly, above=of D, "\tiny$m$" above] (mm) {};
\node[poly, cod, right= of D.south, yshift=-1ex, "$\car{c}$" right] (DD) {};
\node[poly, cod, above=of DD, "$m$" right] (mmm) {};
\node[poly, cod, above=of mmm, "$\car{d}$" right] (C) {};
\draw (m_pos) to[first] (D_pos);
\draw (D_dir) to[climb] (mm_pos);
\draw (mm_dir) to[last] (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] (C_pos);
\draw (C_dir) to[last] (mm_dir);
\end{tikzpicture}
\node (p2) [right=of p1] {
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$m$" left] (m') {};
\node[poly, right= of m'.south, yshift=-1ex, "\tiny$m$" below] (mm') {};
\node[poly, above=of mm', "\tiny$\car{d}$" above] (C') {};
\node[poly, cod, right= of mm'.south, yshift=-1ex, "$\car{c}$" right] (D') {};
\node[poly, cod, above=of D', "$m$" right] (mmm') {};
\node[poly, cod, above=of mmm, "$\car{d}$" right] (CC') {};
\draw[double,-] (m'_pos) to[first] (mm'_pos);
\draw (mm'_dir) to[climb] (C'_pos);
\draw (C'_dir) to[last] (m'_dir);
\draw (mm'_pos) to[first] (D'_pos);
\draw (D'_dir) to[climb] (mmm'_pos);
\draw (mmm'_dir) to[last] (mm'_dir);
\draw[double,-] (C'_pos) to[first] (CC'_pos);
\draw[double,-] (CC'_dir) to[last] (C'_dir);
\end{tikzpicture}
\node at ($(p1.east)!.5!(p2.west)$) {$=$};
\end{tikzpicture}
\end{equation}

This polybox equation implies that we can unambiguously write

\[
\begin{tikzpicture}[polybox, tos]
\node[poly, dom, "$m$" left] (m) {};
\node[poly, cod, right=of m, "$m$" right] (mm) {};
\node[poly, cod, above=of mm, "$\car{d}$" right] (C) {};
\node[poly, cod, below=of mm, "$\car{c}$" right] (D) {};
\draw (m_pos) to[out=0, in=180] (D_pos);
\draw (D_dir) to[climb] (mm_pos);
\draw (mm_dir) to[climb] (C_pos);
\draw (C_dir) to[last] (m_dir);
\end{tikzpicture}
\]

for any bicomodule $\car{c}\bimodfrom[m]\car{d}$.

Let $\cat{C}=(\car{c},\epsilon,\delta)$ be a category. Recall from <ref> that $\yon$ has a unique category structure.

* Show that a left $\cat{C}$-module is the same thing as a $(\cat{C},\yon)$-bimodule.

* Show that a right $\cat{C}$-module is the same thing as a $(\yon,\cat{C})$-bimodule.

* Show that every polynomial $p\in\poly$ has a unique $(\yon,\yon)$-bimodule structure.

* Show that there is an isomorphism of categories $\poly\cong\bimod{\yon}{\yon}$.

* By <ref>, it suffices to check that the diagram (<ref>) commutes vacuously when $\car{d}=\yon$.

* By <ref>, it suffices to check that the diagram (<ref>) commutes vacuously when $\car{c}=\yon$.

* This follows from <ref>.

* This follows from <ref>.

§.§ More equivalences

We have seen that a cofunctor from a state category to a category $\cat{C}$ carries the same data as a $\cat{C}$-coalgebra, which is in turn equivalent to a discrete opfibration over $\cat{C}$ or a copresheaf on $\cat{C}$.
We then showed that cartesian cofunctors to $\cat{C}$ is an equivalent notion as well.
We are now ready to show that several kinds of comodules are also equivalent to all of these concepts.

Given a polynomial comonoid $\cat{C}=(\car{c},\epsilon,\delta)$, the following comprise equivalent categories:

* functors $\cat{C}\to\smset$;

* discrete opfibrations over $\cat{C}$;

* cartesian cofunctors to $\com{C}$;

* $\com{C}$-coalgebras (sets with a coaction by $\com{C}$);

* constant left $\com{C}$-comodules;

* $(\com{C},\0)$-bicomodules;

* linear left $\com{C}$-comodules; and

* representable right $\com{C}$-comodules (opposite).

In fact, all but the first comprise isomorphic categories; and up to isomorphism, any one of these can be identified with a cofunctor from a state category to $\cat{C}$.

$1\simeq 2\cong 3$: This was shown in <ref>.

$3\cong 4$: Given a cartesian cofunctor $(\pi_1,\pi^\sharp)\colon\cat{S}\cof\cat{C}$, let $S\coloneqq\Ob(\cat{S})$ and define a $\car{c}$-coalgebra structure $\alpha\colon S\to\car{c}\tri S$ on an object $s\in\Ob(\cat{S})$ and an emanating morphism $f\colon\pi_1(s)\to c'$ in $\cat{C}$ by

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$S$" left] (yX) {$\varnothing$\at$s$};
\node[poly, cod, right=1.8 of yX.south, yshift=-1ex, "$\car{c}$" right] (p) {$f$\at$\pi_1(s)$};
\node[poly, above=of p, "$S$" right] (p') {$\varnothing$\at$\cod\pi^\sharp_s(f)$};
\draw (yX_pos) to[first] node[below] {$\alpha_1$}(p_pos);
\draw (p_dir) to[climb] node[right] {$\alpha_2$} (p'_pos);
\draw (p'_dir) to[last] node[above left] {$!$} (yX_dir);
\end{tikzpicture}
\]

We check that this is indeed a coalgebra using properties of cofunctors. For identities in $\com{C}$, we have

\begin{align*}
\alpha_2(s,\id_{\pi_1(s)})&=
\cod\pi^\sharp_s(\id_{\pi_1(s)})\\&=
\cod\id_{s}=s
\end{align*}

and for compositions in $\com{C}$ we have

\begin{align*}
\alpha_2(s, f\then g)&=
\cod\left(\pi_s^\sharp(f\then g)\right)\\&=
\cod\left(\pi_s^\sharp(f)\then\pi^\sharp_{\cod\pi^\sharp_s(f)}g\right)\\&=
\cod\left(\pi^\sharp_{\cod\pi^\sharp_s(f)}g\right)\\&=
\alpha_2(\alpha_2(s,f),g).
\end{align*}

Going backward, if we're given a coalgebra $\alpha\colon S\to\car{c}\tri S$, we obtain a function $\alpha_1\colon S\to\car{c}\tri\1$ and we define $\car{s}\coloneqq \alpha_1^*\car{c}$ and the cartesian lens $\varphi\coloneqq(\alpha_1,\id)\colon\car{s}\to\car{c}$ to be the base change from <ref>. We need to show $\car{s}$ has a comonoid structure $(\car{s},\epsilon,\delta)$ and that $\varphi$ is a cofunctor. We simply define the eraser $\epsilon\colon\car{s}\to\yon$ using $\alpha_1$ and the eraser on $\car{c}$:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" below] (c) {$\id_{\alpha_1(s)}$\at$s\vphantom{s_1}$};
\node[poly, cod, right=of c, "$\car{c}$" below] (c') {$\id_{\alpha_1{s}}$\at$\alpha_1(s)$};
\draw (c_pos) -- node[below] {$\alpha_1$} (c'_pos);
\draw[double,-] (c'_dir) -- (c_dir);
\draw (c'_pos) to[climb'] node[right] {$\epsilon_\car{c}$} (c'_dir);
\end{tikzpicture}
\]

We give the duplicator $\delta\colon\car{s}\to\car{s}\tri\car{s}$ using $\alpha_2$ for the codomain, and using the composite $\then$ from $\car{c}$:

\[
\begin{tikzpicture}[polybox, mapstos]
\node[poly, dom, "$\car{s}$" left] (yX) {$f\then g$\at$s$};
\node[poly, cod, right=2.5 of yX.south, yshift=-1ex, "$\car{s}$" right] (p) {$f$\at$s$};
\node[poly, cod, above=of p, "$\car{s}$" right] (p') {$g$\at$\alpha_2(s,f)$};
\draw[double,-] (yX_pos) to[first] (p_pos);
\draw (p_dir) to[climb] node[right] {$\cod$} (p'_pos);
\draw (p'_dir) to[last] node[above left] {$\comp$} (yX_dir);
\end{tikzpicture}
\]

In <ref> we check that $(\car{s},\epsilon,\delta)$ really is a comonoid, that $(\alpha_1,\id)\colon\car{s}\cof\car{c}$ is a cofunctor, that the roundtrips between cartesian cofunctors and coalgebras are identities, and that these assignments are functorial.

$4\cong5$:This is straightforward and was mentioned in <ref>.

$5\cong6$:A right $\0$-comodule is in particular a polynomial $m\in\poly$ and a lens $\rho\colon m\to m\tri\0$ such that $(m\tri\epsilon)\circ\rho=\id_m$. This implies $\rho$ is monic, which itself implies by <ref> that $m$ must be constant since $m\tri\0$ is constant. This makes $m\tri\epsilon$ the identity, at which point $\rho$ must also be the identity. Conversely, for any set $M$, the corresponding constant polynomial is easily seen to make the diagrams in (<ref>) commute.

$5\cong7$: By the adjunction in <ref> and the fully faithful inclusion $\smset\to\poly$ of sets as constant polynmials, <ref>, we have isomorphisms

\[\poly(S\yon,\car{c}\tri S\yon)\cong\smset(S,\car{c}\tri S\yon\tri\1)=\smset(S,\car{c}\tri S)\cong\poly(S,\car{c}\tri S).\]

One checks easily that if $S\yon\to\car{c}\tri S\yon$ corresponds to $S\to\car{c}\tri S$ under the above isomorphism, then one is a left comodule if and only if the other is.

$7\cong8$: By (<ref>) we have a natural isomorphism

\[
\poly(S\yon,\car{c}\tri S\yon)\cong\poly(\yon^S,\yon^S\tri\car{c}).
\]

In pictures,

\[
\begin{tikzpicture}
\node (p1) {
\begin{tikzpicture}[polybox, tos]
\node[poly, linear dom] (s) {};
\node[poly, cod, right=of s.south, yshift=-1ex] (c) {};
\node[poly, linear cod, above=of c] (s') {};
\node[left=0pt of s_pos] {$S$};
\node[right=0pt of c_pos] {$\car{c}(\1)$};
\node[right=0pt of c_dir] {$\car{c}[\ ]$};
\node[right=0pt of s'_pos] {$S$};
\draw (s_pos) to[first] node[below] {$f$} (c_pos);
\draw (c_dir) to[climb] node[right] {$g$} (s'_pos);
\draw (s'_dir) to[last] node[above] {$!$} (s_dir);
\end{tikzpicture}
\node (p2) [right=2 of p1] {
\begin{tikzpicture}[polybox, tos]
\node[poly, pure dom] (s) {};
\node[poly, pure cod, right=of s.south, yshift=-1ex] (s') {};
\node[poly, cod, above=of s'] (c) {};
\node[left=0pt of s_dir] {$S$};
\node[right=0pt of c_pos] {$\car{c}(\1)$};
\node[right=0pt of c_dir] {$\car{c}[\ ]$};
\node[right=0pt of s'_dir] {$S$};
\draw (s_pos) to[first] node[below] {$!$} (s'_pos);
\draw (s'_dir) to[climb] node[right] {$f$} (c_pos);
\draw (c_dir) to[last] node[above] {$g$} (s_dir);
\end{tikzpicture}
\end{tikzpicture}
\]

The last claim was proven in <ref>.

Complete the proof of <ref> ($3\cong 4$) by proving the following.

* Show that $(\car{s},\epsilon,\delta)$ really is a comonoid.

* Show that $(\alpha_1,\id)\colon\car{s}\cof\car{c}$ is a cofunctor.

* Show that the roundtrips between cartesian cofunctors and coalgebras are identities.

* Show that the assignment of a $\com{C}$-coalgebra to a cartesian cofunctor over $\cat{C}$ is functorial.

* Show that the assignment of a cartesian cofunctor over $\cat{C}$ to a $\com{C}$-coalgebra is functorial.

Let $\cat{C}$ be a category. Under the above correspondence, the terminal functor $\cat{C}\to\smset$ corresponds to the identity discrete opfibration $\cat{C}\to\cat{C}$, the identity cofunctor $\com{C}\to\com{C}$, a certain left $\com{C}$ comodule with carrier $\com{C}(\1)\yon$ which we call the canonical left $\com{C}$-comodule, a certain constant left $\com{C}$ comodule with carrier $\com{C}(\1)$ which we call the canonical $(\com{C},\0)$-bicomodule, and a certain representable right $\com{C}$-comodule with carrier $\yon^{\com{C}(\1)}$ which we call the canonical right $\cat{C}$-comodule.

For any object $c\in \cat{C}$, consider the representable functor $\cat{C}(c,-)\colon\cat{C}\to\smset$. What does it correspond to as a

* discrete opfibration over $\cat{C}$?

* cartesian cofunctor to $\com{C}$?

* linear left $\com{C}$-comodule?

* constant left $\com{C}$-comodule?

* $(\com{C},\0)$-bicomodule?

* representable right $\com{C}$-comodule?

* dynamical system with comonoid interface $\com{C}$?

We saw in <ref> that the category $\bimod{\cat{C}}{\0}$ of $(\cat{C},\0)$-bicomodule has a very nice structure: it's the topos of copresheaves on $\cat{C}$.

* What is a $(\0,\cat{C})$-bicomodule?

* What is $\bimod{\0}{\cat{C}}$?

§.§ Bicomodules are parametric right adjoints

There is an equivalent characterization of bicomodules over a pair of polynomial comonoids due to Richard Garner.

Let $\cat{C}$ and $\cat{D}$ be categories.
Then the following can be identified, up to isomorphism:

* a $(\cat{C},\cat{D})$-bicomodule.

* a parametric right adjoint $\smset^{\cat{D}}\to\smset^{\cat{C}}$.

* a connected limit-preserving functor $\smset^{\cat{D}}\to\smset^{\cat{C}}$.

When a polynomial

\[
m\coloneqq\sum_{i\in m(\1)}\yon^{m[i]}
\]

is given the structure of a $(\cat{D},\cat{C})$-bicomodule, the symbols in that formula are given a hidden special meaning:

\[
\qqand
\]

Before we knew about bicomodule structures, what we called positions and directions—and what we often think of as outputs and inputs of a system—were understood as each forming an ordinary set. In the presence of a bicomodule structure, the positions $m(\1)$ have been organized into a $\cat{D}$-set and the directions $m[i]$ have been organized into a $\cat{C}$-set for each position $i$. We are listening for $\cat{C}$-sets and positioning ourselves in a $\cat{D}$-set.

Let $\cat{C}$ and $\cat{D}$ be categories. A prafunctor (also called a parametric right adjoint functor) $\smset^{\cat{C}}\to\smset^{\cat{D}}$ is one satisfying any of the conditions of <ref>.

§.§ Bicomodules in dynamics

We conclude with a peek at how bicomodules can model dynamical systems themselves.

[Cellular automata]
In <ref> we briefly discussed cellular automata; here we will discuss another way that cellular automata show up, this time in terms of bicomodules.

Suppose that $\src,\tgt\colon A\tto V$ is a graph, and consider the polynomial

\[
g\coloneqq\sum_{v\in V}\yon^{\src\inv(v)}
\]

so that positions are vertices and directions are emanating arrows. It carries a natural bicomodule structure

\[
\]

where the right structure lens uses $\tgt$; see <ref> for details. A bicomodule

\[
\]

can be identified with a functor $T\colon V\to\smset$, i.e. it assigns to each vertex $v\in V$ a set. Let's call $T(v)$ the color set at $v$; for many cellular automata we will put $T(v)\cong\2$ for each $v$.

Then a cellular automata on $g$ with color sets $T$ is given by a map

\[
\begin{tikzcd}
V\yon\ar[r, bimr-biml, "g"]\ar[rr, bend right=40pt, bimr-biml, "T"', "" name=T]&
V\yon\ar[r, bimr-biml, "T"]\ar[to=T, Rightarrow, "\alpha"]&
\0
\end{tikzcd}
\]

Indeed, for every vertex $v\in V$ the map $\alpha$ gives a function

\[
\prod_{\src(a)=v}T(\tgt(a))\Too{\alpha_v} T(v),
\]

which we call the update function. In other words, given the current color at the target of each arrow emanating from $v$, the function $\alpha_v$ returns a new color at $v$.

Note that if $V\in\bimod{V\yon}{\0}$ is the terminal object, then the composite $V\yon\bimodfrom[g]V\yon\bimodfrom[V]\0$ is again $V$.

Let $\src,\tgt\colon A\tto V$ and $g$ and $T$ be as in <ref>.

* Give the structure lens $\lambda\colon g\to V\yon\tri g$

* Give the structure lens $\rho\colon g\to g\tri V\yon$.

* Give the set $T$ and the structure lens $T\to V\yon\tri T$ corresponding to the functor $V\to\smset$ that assigns $\2$ to each vertex.

For each $v\in V$, let $A_v\coloneqq\fun{src}\inv(v)$, the set of arrows emanating from $v$.

* We need a lens $\sum_{v\in V}\yon^{A_v}\to V\sum_{v\in V}\yon^{A_v}$, and we use the obvious “diagonal” lens, which on positions sends $v\mapsto (v,v)$ and on directions is the identity.

* We need a lens $\sum_{v\in V}\yon^{A_v}\to\sum_{v\in V}\prod_{a\in A_v}\sum_{v\in V}\yon$, which is the same as an element of

\[
\prod_{v\in V}\sum_{v'\in V}\prod_{a\in A_{v'}}\sum_{v''\in V}A_v
\]

and we use $v\mapsto (v, a\mapsto\fun{tgt}(a), a)$. Most of this is forced on us, and the only interesting part is the function $A_v\to V$, which we can take to be anything, the choice being exactly the choice of “target map” that defines our graph.

* Let $T=\2V$ and take the map $\2V\to V\times \2V$ to be $(i,v)\mapsto(v,i,v)$ for any $i\in \2$ and $v\in V$.

[Running a cellular automaton]
Let $g$ be a graph on vertex set $V$, let $T$ assign a color set to each $v\in V$, and let $\alpha$ be the update function for a cellular automaton. As in <ref>, this is all given by a diagram

\[
\begin{tikzcd}
V\yon\ar[r, bimr-biml, "g"]\ar[rr, bend right=40pt, bimr-biml, "T"', "" name=T]&
V\yon\ar[r, bimr-biml, "T"]\ar[to=T, Rightarrow, "\alpha"]&
\0
\end{tikzcd}
\]

To run the cellular automaton, one simply chooses a starting color in each vertex. We call this an initialization; it is given by a map of bicomodules

\begin{equation}\label{eqn.starting_color_v}
\begin{tikzcd}
\ar[r, bimr-biml, bend left, "V"]
\ar[r, bimr-biml, bend right, "T"']\ar[r, phantom, "\hphantom{\scriptstyle\sigma}\Downarrow\scriptstyle\sigma"]&
\end{tikzcd}
\end{equation}

Note that $g$ is a profunctor, i.e. for each $v\in V$ the summand $g_v=\yon^{\fun{src}\inv(v)}$ is representable, so it preserves the terminal object. In other words $g\tri_{V\yon}V\cong V$.

Now to run the cellular automaton on that initialization for $k\in\nn$ steps is given by the composite

\[
\begin{tikzcd}
V\yon\ar[d, equal]\ar[r, bimr-biml, "g"]\ar[rrrr, bimr-biml, bend left, "V", ""' name=V']&
\cdots\ar[r, bimr-biml, "g"]&|[alias=VV]|
V\yon\ar[d, equal]\ar[r, bimr-biml, "g"]&
V\yon\ar[d, equal]\ar[r, bimr-biml, "V"]&
\0\ar[d, equal]\ar[dl, phantom, "\Downarrow\scriptstyle\sigma"]\\
V\yon\ar[d, equal]\ar[r, bimr-biml, "g"]&
\cdots\ar[r, bimr-biml, "g"]&
V\yon\ar[d, equal]\ar[r, bimr-biml, "g"]&
V\yon\ar[r, bimr-biml, "T"]&
\0\ar[d, equal]\ar[dll, phantom, "\Downarrow\scriptstyle\alpha"]\\