\begin{document}

\title{All Concepts are $\mathbb{C}atsharp$}

\author{Owen Lynch \and Brandon T. Shapiro \and David I. Spivak}

\date{
}

\maketitle

\begin{abstract}
We show that the double category $\mathbb{C}atsharp$ of comonoids in the category of polynomial functors (previously shown by Ahman-Uustalu and Garner to be equivalent to the double category of categories, cofunctors, and prafunctors) contains several formal settings for basic category theory, provides an elegant description of Weber's nerve construction for generalized higher categories, and has subcategories equivalent to both the double category ${\mathbb{O}\mathbf{C}at{rg}}$ of dynamic rewiring systems and the double category $\mathbb{P}oly_{\cat{E}}$ of generalized polynomials in a finite limit category ${\cat{E}}$. Also serving as a natural setting for categorical database theory, $\mathbb{C}atsharp$ at once hosts models of a wide range of concepts from the theory and applications of polynomial functors and higher categories.
\mathbf{C}at{End}d{abstract}

\renewcommand\cftbeforechapterskip{2pt plus 1pt}

\begin{KeepFromToc}
\tableofcontents
\mathbf{C}at{End}d{KeepFromToc}

\chapter{Introduction}

Mac Lane famously declared that ``The notion of Kan extensions subsumes all the other fundamental concepts of category theory''  referring to the fact that limits, colimits, adjunctions, and the Yoneda lemma can all be defined in terms of Kan extensions, and titled that section ``All concepts are Kan extensions".

In the theory of polynomial functors, particularly as it has been explored by the authors, the main avenues of development have been the generalization from polynomials in the category $\mathbf{C}at{Set}$ to polynomials in other categories \cite{kock2012polynomial,weber2015polynomials,shapiro2023structures} and applications to categorical database theory \cite{spivak2012functorial,spivak2021functorial}, open dynamical systems \cite{spivak2021learners,shapiro2022dynamic}, and algebraic higher category theory \cite{weber2007familial,weber2015operads,shapiro2022thesis}. Recent results of Ahman-Uustalu \cite{ahman2016directed,ahman2017taking} and Garner show that comonoids in the monoidal category $\mathbf{C}at{Poly}$ of polynomial endofunctors on $\mathbf{C}at{Set}$, coincide with the usual notion of categories, comonoid homomorphisms correspond to cofunctors, and bicomodules between comonoids correspond to parametric right adjoint functors between their associated copresheaf categories (also called \emph{prafunctors}). In \cite{spivak2021functorial}, the author assembled these components into a double category $\mathbb{C}atsharp$ and showed it to be a natural setting for categorical database theory. The author and Brown in \cite{brown2023dynamic} use $\mathbb{C}atsharp$ as a formal semantics for rewriting protocols, and provides a graphical language for a fragment of it. The goal of the present work is to demonstrate that $\mathbb{C}atsharp$ in fact subsumes the other fundamental concepts of polynomial functor theory as well, and begin to describe how basic category theory, as well as notions in higher category theory, find a home (or many) in $\mathbb{C}atsharp$.

While the objects of $\mathbb{C}atsharp$ are categories and the vertical and horizontal morphisms (cofunctors and prafunctors) are fundamental to the study of their copresheaf categories, functors between the categories themselves are not explicitly present in the data of $\mathbb{C}atsharp$, which would seem to limit the usefulness of this setting for modeling basic category theory. Several remedies have been proposed, including by upgrading $\mathbb{C}atsharp$ to include higher dimensional data \cite[Example 5.13]{shapiro2023structures} or finding functors in alternative places in $\mathbb{C}atsharp$.
\footnote{See for instance \href{https://youtu.be/aTZyHHAwk2E?t=7364}{Todd Trimble's talk} at the 2021 Workshop on Polynomial Functors.}
We take the latter approach by considering both monads in the bicategory of spans and algebras for a certain monad on the category of graphs as notions of categories whose morphisms are functors. We show that they both exist in $\mathbb{C}atsharp$ and can be recovered from categories regarded as objects in $\mathbb{C}atsharp$. We also show that opposites of categories can be recovered using adjoint and monoidal dualization operations in $\mathbb{C}atsharp$.

In \cite{shapiro2023structures}, the authors establish the category $\mathbf{C}at{Poly}_{\cat{E}}$ of polynomials in a finite limit category ${\cat{E}}$ and show that a wide range of structures and results previously known for polynomials in $\mathbf{C}at{Set}$ generalize to this setting. Much like $\mathbf{C}at{Poly}$, $\mathbf{C}at{Poly}_{\cat{E}}$ is a duoidal category under composition and a generalization of the Dirichlet tensor product, and comonoids in $\mathbf{C}at{Poly}_{\cat{E}}$ are precisely the categories internal to ${\cat{E}}$ whose source morphism is exponentiable. \cref{polyEembed} shows that $\mathbf{C}at{Poly}_{\cat{E}}$ has a faithful embedding into $\mathbb{C}atsharp$, so that in order to study polynomials in any category ${\cat{E}}$ one need only consider structures based on polynomials in $\mathbf{C}at{Set}$. 

In \cite{weber2007familial}, Weber defined a generalization of the Lawvere theory associated to an algebraic structure on sets, the nerve construction for categories, and generalizations of the nerve to various flavors of algebraic higher categories. For a class of monads $m$ including those whose underlying endofunctor is parametric right adjoint, there is a fully faithful ``nerve'' functor from $m$-algebras to presheaves on a category $\Theta_m$. We show in \cref{nervecoalgebra} that for any parametric right adjoint monad $m$ on a copresheaf category considered as a monad in $\mathbb{C}atsharp$, the category $\Theta_m^\tn{op}$ is the comonoid recovered by a right coclosure operation for composition in $\mathbb{C}atsharp$, and the nerve construction is easily recovered using the universal property of the coclosure. This shows that $\Theta_m$ has a universal property relative to the monad $m$, and opens the door for the further study of higher category theory in the language of polynomials.

In \cite{spivak2021learners,shapiro2022dynamic}, the authors explore how coalgebras for polynomial functors and algebraic structures built from such coalgebras provide a wide-reaching language for modeling dynamical systems which respond to external feedback, and construct the double category ${\mathbb{O}\mathbf{C}at{rg}}$ as a convenient setting for the study of such ``open'' dynamics which includes examples from machine learning and economics. Separately in \cite{Lynch:blog}, the author introduces ``effects handlers,'' a mathematical object defined in terms of polynomials which models a way of incorporating side effects into the functional programming paradigm. In \cref{thm.eff_statement}, we show that effects handlers form the horizontal morphisms of a sub-double category of $\mathbb{C}atsharp$, and in \cref{thm.org_statement} we show that ${\mathbb{O}\mathbf{C}at{rg}}$ is a sub-double category of effects handlers, so that both effects handlers and coalgebras can be reasoned about in the language of $\mathbb{C}atsharp$.

Of course, not all concepts in category theory are Kan extensions (for example, categories are not Kan extensions), and neither is every concept in category theory found in $\mathbb{C}atsharp$. However, in both cases the exaggeration is worthwhile because the overwhelming ubiquity and power of the formalism makes it worthy of deep study. 

\section*{Notation}

The symbol $\sum$ denotes an indexed coproduct, the symbol $+$ denotes binary coproduct, and $0$ denotes an initial object. For a morphisms $f \colon A \to B$ and $C \to B$ in a category, we will sometimes write $f^\ast C$ for the pullback $A \times_B C$. 

\section*{Acknowledgments}

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-20-1-0348.

\chapter{The Double Category $\mathbb{C}atsharp$}

We begin by recalling the definition of the double category $\mathbb{C}atsharp$ and the foundational results that make it so broadly applicable.

\section{The category of polynomials}

\begin{definition}
A \emph{polynomial} $p$ consists of a set $p(1)$ along with, for each element $I \in p(1)$, a set $p[I]$. We write
\[
p = \sum_{I \in p(1)} \mathcal{y}^{p[I]}
\]
for such a polynomial, which is also the form of the associated \emph{polynomial functor} $\mathbf{C}at{Set} \to \mathbf{C}at{Set}$. A morphism $\phi$ of polynomials $p \to q$ is a natural transformation. It can be cast set-theoretically as consisting of a function $\phi_1 \colon p(1) \to q(1)$ along with, for each $I \in p(1)$, a function $\phi^\#_I \colon p[I] \leftarrow q[\phi_1I]$. We write $\mathbf{C}at{Poly}$ for the category of polynomials.
\mathbf{C}at{End}d{definition}

Elements of the set $p(1)$ are called \emph{positions} of a polynomial $p$, and for each $I\in p(1)$, elements of $p[I]$ are called \emph{directions} of $p$. The set of all directions of $p$, or the disjoint union of all the sets $p[I]$, is denoted $p_\ast(1)$ and has a canonical function to $p(1)$. If each $p[I]\cong 1$ is singleton, we say that $p$ is \emph{linear}. A morphism $\phi$ is called \emph{cartesian} if each $\phi^\#_I$ is a bijection, and \emph{vertical} if $\phi_1$ is a bijection.

\begin{definition}[{\cite[Proposition 2.1.7]{spivak2021functorial}}]
We denote by $\mathcal{y}$ the polynomial with a single position and a single direction. For polynomials $p,q$, their \emph{composition} is the polynomial
\[
p \mathbin{\triangleleft} q \coloneq \sum_{\substack{I \in p(1) \\ J \colon p[I] \to q(1)}} \mathcal{y}^{\sum\limits_{i \in p[I]} q[Ji]}.\qedhere 
\]
\mathbf{C}at{End}d{definition}

There is a monoidal structure on the category $\mathbf{C}at{Poly}$ given by $(\mathcal{y},\mathbin{\triangleleft})$, and there are three additional monoidal structures given by
\begin{itemize}
	\item $(0,+)$, where $0$ is the polynomial with no positions, $(p + q)(1) \coloneq p(1) + q(1)$, $(p + q)[I] \coloneq p[I]$ for $I \in p(1)$, and $(p + q)[J] \coloneq q[J]$ for $J \in q(1)$;
	\item $(1,\times)$, where $1$ is the polynomial with one position and no directions, $(p \times q)(1) \coloneq p(1) \times q(1)$, and $(p \times q)[I,J] \coloneq p[I] + q[J]$; and
	\item $(\mathcal{y},\otimes)$, where $(p \otimes q)(1) \coloneq p(1) \times q(1)$ and $(p \otimes q)[I,J] \coloneq p[I] \times q[J]$.
\mathbf{C}at{End}d{itemize}

\section{Comonoids and bicomodules}

\begin{definition}
A \emph{comonoid} in $\mathbf{C}at{Poly}$ is a polynomial $c$ equipped with morphisms $\epsilon \colon c \to \mathcal{y}$ (the counit) and $\delta \colon c \to c \mathbin{\triangleleft} c$ (the comultiplication) satisfying unit and associativity equations. A comonoid homomorphism is a morphism of polynomials $c \to c'$ which commutes with counits and comultiplications.
\mathbf{C}at{End}d{definition}

\begin{definition}
For comonoids $c,d$ in $\mathbf{C}at{Poly}$, a $(c,d)$-bicomodule is a polynomial $p$ equipped with morphisms
\[
c \mathbin{\triangleleft} p {\cat{F}}rom{\lambda} p \To{\rho} p \mathbin{\triangleleft} d
\]
which commute with each other as well as the counits and comultiplications of $c$ and $d$, in the sense of \cite[Definition 2.2.11]{spivak2021functorial}. We will often denote a $(c,d)$-bicomodule $p$ as $c \bifrom[p] d$.
\mathbf{C}at{End}d{definition}

In \cite[Corollary 2.2.10]{spivak2021functorial}, the author established using a theorem of Shulman \cite[Theorem 11.5]{shulman2008framed} that there is a double category $\mathbb{C}\mathbf{C}at{omod}(\mathbf{C}at{Poly})$ (in fact an equipment) whose objects are comonoids and horizontal morphisms are bicomodules.

\begin{definition}\label{defcatsharp}
$\mathbb{C}atsharp$ is the pseudo-double category $\mathbb{C}\mathbf{C}at{omod}(\mathbf{C}at{Poly})$ which has
\begin{itemize}
	\item as objects, the comonoids in $\mathbf{C}at{Poly}$;
	\item as vertical morphisms, the comonoid homomorphisms;
	\item as horizontal morphisms from $c$ to $d$, the $(c,d)$-bicomodules;
	\item as squares between homomorphisms $\phi,\psi$ and bicomodules $p,p'$, the morphisms of polynomials $\gamma \colon p \to p'$ such that the diagram in \eqref{eqn.square} commutes;
	\begin{equation}\label{eqn.square}
	\begin{tikzcd}
	c \mathbin{\triangleleft} p \dar[swap]{\phi \mathbin{\triangleleft} \gamma} & p \lar \rar \dar{\gamma} & p \mathbin{\triangleleft} d \dar{\gamma \mathbin{\triangleleft} \psi} \\
	c' \mathbin{\triangleleft} p' & p' \lar \rar & p' \mathbin{\triangleleft} d'
	\mathbf{C}at{End}d{tikzcd}
	\mathbf{C}at{End}d{equation}
	\item as horizontal identities, the comultiplication bicomodules $c \mathbin{\triangleleft} c {\cat{F}}rom{\delta} c \To{\delta} c \mathbin{\triangleleft} c$; and
	\item as composition of horizontal morphisms $c \bifrom[p] d \bifrom[q] e$, the bicomodule $p \mathbin{\triangleleft}_d q$ on the top row of \eqref{eqn.biccomp},
	\begin{equation}\label{eqn.biccomp}
	\begin{tikzcd}
	c \mathbin{\triangleleft} (p \mathbin{\triangleleft}_d q) \dar & p \mathbin{\triangleleft}_d q \dar \rar \lar & (p \mathbin{\triangleleft}_d q) \mathbin{\triangleleft} e \dar \\
	c \mathbin{\triangleleft} p \mathbin{\triangleleft} q \dar[shift right=2] \dar[shift left=2] & p \mathbin{\triangleleft} q \dar[shift right=2] \dar[shift left=2] \rar \lar & p \mathbin{\triangleleft} q \mathbin{\triangleleft} e \dar[shift right=2] \dar[shift left=2] \\
	c \mathbin{\triangleleft} p \mathbin{\triangleleft} d \mathbin{\triangleleft} q & p \mathbin{\triangleleft} d \mathbin{\triangleleft} q \rar \lar & p \mathbin{\triangleleft} d \mathbin{\triangleleft} q \mathbin{\triangleleft} e
	\mathbf{C}at{End}d{tikzcd}
	\mathbf{C}at{End}d{equation}
	where each object in the top row of \eqref{eqn.biccomp} is computed as the equalizer of the column below it, using the fact that the functors $c \mathbin{\triangleleft} -$ and $- \mathbin{\triangleleft} e$ preserve connected limits, and the maps between them are induced by the underlying transformations between equalizer diagrams. This also shows how to horizontally compose squares, as a pair of adjacent squares provides the data of a transformation of equalizer diagrams which induces a map between the composite bicomodules.\qedhere
\mathbf{C}at{End}d{itemize}
\mathbf{C}at{End}d{definition}

\section{Categories, cofunctors, and prafunctors}

The motivation for studying $\mathbb{C}atsharp$ comes from recent results of Ahman--Uustalu \cite{ahman2014when} and Garner
\footnote{We refer to \href{https://www.youtube.com/watch?v=tW6HYnqn6eI}{Garner's HoTTEST video}, where the proof was sketched; see also \cite{spivak2021functorial}.}
 that, respectively, comonoids in $\mathbf{C}at{Poly}$ are precisely categories and that bicomodules between them are precisely parametric right adjoint functors (sometimes shortened to \emph{prafunctors}) between their copresheaf categories. This makes $\mathbb{C}atsharp$ a natural setting for categorical database theory \cite{spivak2012functorial,spivak2021functorial}, where database schemas are categories, instances are copresheaves, and queries (along with more general data migration operations) are prafunctors.

\begin{definition}\label{comonoidcategory}
For a polynomial comonoid $(c,\epsilon,\delta)$, its corresponding category has
\begin{itemize}
	\item as objects, elements of the set $c(1)$;
	\item as morphisms out of an object $C \in c(1)$, the set $c[C]$;
	\item as codomain assignment for morphisms out of $C$, the function $\delta_1(c) \colon c[C] \to c(1)$;
	\item as composition of morphisms out of $C$, the function $\delta^\sharp_C \colon c[C] \times_{c(1)} c_\ast(1) \to c[C]$; and
	\item as the identity morphism at $C$, the function $\epsilon^\#_C \colon 1 \to c[C]$.\qedhere
\mathbf{C}at{End}d{itemize}
\mathbf{C}at{End}d{definition}

Comonoid homomorphisms, however, correspond not to functors but to cofunctors.

\begin{definition}[{\cite[Definition 2.2.2]{spivak2021functorial}}]
For categories $c$ and $d$ (regarded as polynomial comonoids), a cofunctor $c \to d$ is a function $\phi_1 \colon c(1) \to d(1)$ along with, for each $C \in c(1)$, a function $d[\phi_1C] \to c[C]$ which preserves identities, codomains, and composites.
\mathbf{C}at{End}d{definition}

For $c$ a category, we write $c\tn{-}\mathbf{C}at{Set}$ for the category of copresheaves on $c$, meaning functors $c \to \mathbf{C}at{Set}$. For $X$ a $c$-copresheaf and $C \in c(1)$ an object, we write $X_C$ for $X(C)\in\mathbf{C}at{Set}$.

\begin{definition}\label{defprafunctor}
A parametric right adjoint functor $F \colon d\tn{-}\mathbf{C}at{Set} \to c\tn{-}\mathbf{C}at{Set}$ is a functor with the following form, for any $d$-copresheaf $X$ and object $C \in c(1)$,
\[
F(X)_C = \sum_{I \in p_C(1)} \Hom_{d\tn{-}\mathbf{C}at{Set}}(p[I],X)
\]
where $p_{(-)}(1)$ is a functor $c \to \mathbf{C}at{Set}$, $p_C(1)$ is its evaluation at $C$, and $p[-]$ is a functor $\left(\int p_{(-)}(1)\right)^\tn{op} \to d\tn{-}\mathbf{C}at{Set}$ from the dual of the category of elements of $p_{(-)}(1)$.

When $p$ is a $(c,d)$-bicomodule and $C \in c(1)$, we have $p(1)\cong\sum_{C\in c(1)}p_C(1)$, and we recover $p_C(1)$ as the preimage of $C$ under the function $p(1) \To{\lambda(1)} (c \mathbin{\triangleleft} p)(1) \To{c\mathbin{\triangleleft}\,!} c(1)$. Moreover, for $I \in p_C(1)$ and $D \in d(1)$, the set $p[I]_D$ is the preimage of $D$ under the function $p[I] \to d(1)$ given by the element $1\To{I}p(1) \To{\rho(1)} (p \mathbin{\triangleleft} d)(1)$.
\mathbf{C}at{End}d{definition}

Based on this interpretation, we will often denote a $(c,d)$-bicomodule $p$ as
\[
\sum_{C \in c(1)} \sum_{I \in p_C(1)} \mathcal{y}^{p[I]}
\]
where $p[I]$ is presumed to have the structure of a $d$-copresheaf.

\begin{example}
For any set $A$, the linear polynomial $A\mathcal{y}$ has a unique comonoid structure; it corresponds to the discrete category on $A$. Cofunctors $A\mathcal{y}\to B\mathcal{y}$ are functions $A\to B$.
\mathbf{C}at{End}d{example}

\begin{example}
For $c$ any category, a $(c,0)$-bicomodule $p$ is a parametric right adjoint functor from $0\tn{-}\mathbf{C}at{Set}$, the terminal category, to $c\tn{-}\mathbf{C}at{Set}$. The particular copresheaf on $c$ this functor picks out is $p_{(-)}(1)$, whose elements are positions of $p$ and whose $c$-copresheaf structure is determined by the map $c \mathbin{\triangleleft} p {\cat{F}}rom{\lambda} p$. As there is also a map $p \to p \mathbin{\triangleleft} 0$ which preserves the positions of $p$, and forces the polynomial $p$ to have an empty set of directions. The category of $(c,0)$-bicomodules and maps between them as in \eqref{eqn.square} with $\phi,\psi$ identities is equivalent to the category $c\tn{-}\mathbf{C}at{Set}$.

The composition of a $(c,d)$-bicomodule and a $(d,0)$-bicomodule is precisely the $c$-copresheaf given by applying the a prafunctor $d\tn{-}\mathbf{C}at{Set} \to c\tn{-}\mathbf{C}at{Set}$ to a $d$-copresheaf.
\mathbf{C}at{End}d{example}

\begin{example}
More generally, parametric right adjoint functor $d\tn{-}\mathbf{C}at{Set} \to c\tn{-}\mathbf{C}at{Set}$ is a right adjoint precisely when it arises from a profunctor from $c$ to $d$: a copresheaf on $c^\tn{op} \otimes d$ induces a functor $c^\tn{op} \to d\tn{-}\mathbf{C}at{Set}$ whose corresponding singular functor is a right adjoint $d\tn{-}\mathbf{C}at{Set} \to c\tn{-}\mathbf{C}at{Set}$. However, unlike when $d$ is discrete, the left adjoint of this prafunctor will not generally be a prafunctor itself.
\mathbf{C}at{End}d{example}

\chapter{Basic Category Theory in $\mathbb{C}atsharp$}

While cofunctors and prafunctors are interesting and useful branches of category theory, they are not the stuff of a category theorist's typical toolbox. However, traditional features of category theory can also be recovered in $\mathbb{C}atsharp$ by various means which we now discuss.

\section{Products and coproducts}

Both monoidal products $\otimes$ and $+$ have a \emph{duoidal} relationship with composition $\mathbin{\triangleleft}$, meaning there are natural morphisms
\begin{equation}\label{eqn.duoidal}
(p \mathbin{\triangleleft} q) \otimes (r \mathbin{\triangleleft} s) \to (p \otimes r) \mathbin{\triangleleft} (q \otimes s) \mathbb{Q}and (p \mathbin{\triangleleft} q) + (r \mathbin{\triangleleft} s) \to (p + r) \mathbin{\triangleleft} (q + s).
\mathbf{C}at{End}d{equation}
As a general consequence of duoidality, comonoids in $\mathbf{C}at{Poly}$ are closed under $+$ and $\otimes$.

\begin{theorem}[{\cite[Proposition 2.6.2]{spivak2021functorial}}]
For categories $c,d$ regarded as polynomial comonoids, $c + d$ corresponds to the usual coproduct and $c \otimes d$ to the usual product of $c$ and $d$ as categories. Similarly, $0$ corresponds to the empty category and $\mathcal{y}$ to the terminal category.
\mathbf{C}at{End}d{theorem}

\begin{example}
For categories $c,d$, there is a bicomodule $c \otimes d \bifrom[c \times d] c + d$ where the set $(c \times d)(1) = c(1) \times d(1)$ forms the elements of the terminal copresheaf on $c \otimes d$ and each direction set $(c \times d)[C,D] = c[C] + d[D]$ forms the elements of the copresheaf $(c[C],d[D])$ in $(c+d)\tn{-}\mathbf{C}at{Set} \simeq c\tn{-}\mathbf{C}at{Set} \times d\tn{-}\mathbf{C}at{Set}$. The corresponding prafunctor sends the pair $(X,Y)$ of copresheaves $X$ on $c$ and $Y$ on $d$ to the copresheaf $X \boxtimes Y$ on $c \otimes d$ with
\begin{align*}
	(X \boxtimes Y)_{C,D} &= 
  \Hom_{(c+d)\tn{-}\mathbf{C}at{Set}}\left((c[C],d[D]),(X,Y)\right)\\&\cong 
  \Hom_{c\tn{-}\mathbf{C}at{Set}}(c[C],X) \times \Hom_{d\tn{-}\mathbf{C}at{Set}}(d[D],Y) \cong X_C \times Y_D.
\mathbf{C}at{End}d{align*}
because $c[C]$ and $d[D]$ correspond to representable copresheaves. The prafunctor we have thus described is sometimes called the \emph{external product on copresheaves}.
\mathbf{C}at{End}d{example}

\section{Three homes for categories}

We now show how categories live in $\mathbb{C}atsharp$ in at least three different ways, and how to mediate between them. Categories are, simultaneously:
\begin{itemize}
	\item comonoids in $\mathbf{C}at{Poly}$, and hence objects in $\mathbb{C}atsharp$ (\cref{comonoidcategory});
	\item monads in the double subcategory of $\mathbb{C}atsharp$ consisting of linear comonoids and linear bicomodules (spans) \cite[5.4.3]{benabou1967introduction}; and
	\item algebras for the parametric right adjoint monad $\mathit{path}$ on graphs (\cref{pathmonad}) \cite[Section II.7]{MacLane:1998a}.
\mathbf{C}at{End}d{itemize}

\begin{definition}
We denote by $g$ the category $e \Tto{s}{t} v$ whose copresheaves are precisely graphs, and by $\vec n$ the graphs with vertices $0,...,n$ and edges $i \mathbin{\tn{-}} 1 \to i$ for all $1 \le i \le n$.
\mathbf{C}at{End}d{definition}

\begin{definition}\label{pathmonad}
The bicomodule $g \bifrom[\mathit{path}] g$ has carrier given by $\{v\}\mathcal{y} + \{e\}\sum\limits_{n \in \mathbb{N}} \mathcal{y}^{\vec n}$, where the labels $e,v$ indicate how the left coaction is defined on positions.
\mathbf{C}at{End}d{definition}

This is a monad in $\mathbb{C}atsharp$ whose corresponding prafunctor is the free category monad on graphs: it is the identity on vertices and adds in formal associative composites for paths of edges with any length $n$, which are precisely the maps into a graph from $\vec n$ \cite[Example C.3.3]{Leinster:2004a}. A category is then precisely a graph $X$, which can be modeled as a $(g,0)$-bicomodule, equipped with a left module structure of the form $\mathit{path} \mathbin{\triangleleft}_g X \to X$. 

Given a category $c$, there is a bicomodule $g \bifromlong{50pt}{\{v\}c + \{e\}c_\ast} c$, where $c_\ast \coloneq \sum\limits_{C \in c(1)} c[C]\mathcal{y}^{c[C]}$. The left $g$-comodule structure arises from the cartesian source and target morphisms $c_\ast \to c$, while the right $c$-comodule structure is given by the comultiplication $c \to c \mathbin{\triangleleft} c$ and its composition with the source morphism $c_\ast \to c$.

The corresponding prafunctor $c\tn{-}\mathbf{C}at{Set} \to g\tn{-}\mathbf{C}at{Set}$ sends a copresheaf $X$ on $c$ to the graph whose vertices are the elements of $X$ and whose morphisms are pairs of a morphism in $c$ and an element of $X$ over its source object. This is precisely the underlying graph of the category of elements of $X$, and as such $c+c_\ast$ has a left $\mathit{path}$-module structure $\mathit{path} \mathbin{\triangleleft}_g (c+c_\ast) \to c+c_\ast$ which induces by precomposition a left $\mathit{path}$-module on $(c + c_\ast) \mathbin{\triangleleft}_c X$ for any copresheaf $X$: this $\mathit{path}$-algebra is precisely $X$'s category of elements. Applying this to the terminal copresheaf $c \bifrom[c(1)] 0$ recovers the category $c$ itself as a $\mathit{path}$-algebra.

Furthermore, for any functor $f$ from $c$ to $d$, there is a bicomodule $c \bifrom[{\cat{D}}elta_f] d$, where ${\cat{D}}elta_f\coloneqq \sum\limits_{C \in c(1)} \mathcal{y}^{d[f(C)]}$. It comes equipped with a canonical morphism $(c + c_\ast) \mathbin{\triangleleft}_c {\cat{D}}elta_f \to d + d_\ast$ of $(c,d)$-bicomodules which commutes with the $\mathit{path}$-module structures of $c+c_\ast$ and $d+d_\ast$. As ${\cat{D}}elta_f \mathbin{\triangleleft}_d d(1) \cong c(1)$ as $(c,0)$-bicomodules, we have constructed in $\mathbb{C}atsharp$ the morphism of $\mathit{path}$-algebras corresponding to the functor $f$.

We now describe how each object in $\mathbb{C}atsharp$ also gives rise to a monad among spans, using the fact that for discrete categories $A\mathcal{y},B\mathcal{y}$ an $(A\mathcal{y},B\mathcal{y})$-bicomodule $p$ can be summarized by a diagram $B {\cat{F}}rom{g} p_\ast(1) \to p(1) \To{f} A$ of sets and functions. The left coaction $A\mathcal{y} \mathbin{\triangleleft} p \leftarrow p$ is cartesian and given on positions by $\langle f,\mathrm{id} \rangle \colon p(1) \to A \times p(1)$, and the right coaction $p \to p \mathbin{\triangleleft} B\mathcal{y}$ is also cartesian and on positions sends $I \in p(1)$ to $(I, g_{p[I]} \colon p[I] \to B)$.

For any category $c$, there is a bicomodule $c(1)\mathcal{y} \bifrom[c] c(1)\mathcal{y}$ given by the diagram
\[
c(1) {\cat{F}}rom{t} c_\ast(1) \To{s} c(1) \To{\mathrm{id}} c(1)
\]
where the left and middle functions are respectively the target and source functions from the set $c_\ast(1)$ of morphisms in $c$ to the set of objects $c(1)$.

By \cite[Proposition 2.5.4]{spivak2021functorial}, a bicomodule between discrete categories whose rightmost function is an identity is always a right adjoint in $\mathbb{C}atsharp$, whose left adjoint is the bicomodule given by the diagram
\[
c(1) {\cat{F}}rom{s} c_\ast(1) \To{\mathrm{id}} c_\ast(1) \To{t} c(1).
\] 
By \cite[Proposition 2.5.6]{spivak2021functorial}, as $c(1) \bifrom[c] c(1)$ is a comonad in $\mathbb{C}atsharp$ its left adjoint $c(1) \bifrom[c\ldag] c(1)$ is a linear monad in $\mathbb{C}atsharp$, i.e.\ a monad in $\mathbb{S}\mathbf{C}at{pan}$, i.e.\ a category. This gives a third home for the category $c$. As desired, for categories $c,d$ a functor between them is a monad map between their corresponding left adjoint spans, so this provides another encoding of functors in $\mathbb{C}atsharp$.

\section{Opposites}\label{sec.op}

Representing categories as spans allows for a construction of dual categories using only universal constructions in $\mathbb{C}atsharp$. In \cite[Proposition 2.7.3]{spivak2021functorial}, the author defines a \emph{closure} for the category of $(c,d)$-bicomodules. When $c = A\mathcal{y}$ and $d = B\mathcal{y}$, this has the form
\[
\ih{A\mathcal{y}}{p}{q}{B\mathcal{y}} \coloneq \sum_{\substack{a \in A \\ \phi \colon p_a \to q_a}} \mathcal{y}^{\sum\limits_{I \in p_a(1)} q[\phi_1(I)]}
\]
where the maps $p_a \to q_a$ are morphisms of $(\mathcal{y},B\mathcal{y})$-bicomodules. We can then define a \emph{dualizing} operation for $(A\mathcal{y},B\mathcal{y})$-bicomodules by setting 
\[
p^\vee \coloneq \ih{A\mathcal{y}}{p}{AB\mathcal{y}}{B\mathcal{y}} = \sum_{a \in A} \Hom(p_a, B\mathcal{y}) \mathcal{y}^{p_a(1)}.
\]
In particular, this dual interpolates between left-adjoint bicomodules of the form $B \leftarrow C = C \to A$ and right-adjoint bicomodules of the form $B \leftarrow C \to A = A$.

This allows spans from $A$ to $A$, modeled as left-adjoint $(A\mathcal{y},A\mathcal{y})$-bicomodules, to be reversed using only adjunctions and duals: given a left adjoint $p$ represented by $A {\cat{F}}rom{f} C = C \To{g} A$, its adjoint $p\ldag$ is represented by $A {\cat{F}}rom{g} C \To{f} A = A$ and its dual $p^\vee$ by $A {\cat{F}}rom{f} C \To{g} A = A$, so both $(p\ldag)^\vee$ and $(p^\vee)\ldag$ are represented by $A {\cat{F}}rom{f} C = C \To{g} A$, the reverse of $p$.

\begin{theorem}
For $c$ a category regarded as a $(c(1),c(1))$-bicomodule, its opposite category $c^\tn{op}$ is given by the $(c(1),c(1))$-bicomodule $(c\ldag)^\vee \cong (c^\vee)\ldag$.
\mathbf{C}at{End}d{theorem}

\chapter{Generalized Polynomials in $\mathbb{C}atsharp$}

Much of the development of the theory of polynomials (for instance \cite{kock2012polynomial,weber2015polynomials,shapiro2023structures}) is focused on generalizing the basic aspects of the theory to categories other than $\mathbf{C}at{Set}$. We show that, in fact, these categories of polynomials embed fully faithfully into categories of bicomodules, so that the constructions in these contexts are in fact merely specializations of the analogous constructions for bicomodules in $\mathbb{C}atsharp$.

\section{Polynomials in a category ${\cat{E}}$}

Throughout this section, let ${\cat{E}}$ be a category with finite limits. Polynomials in ${\cat{E}}$ will generalize the definition of polynomials as morphisms $p_\ast(1) \to p(1)$ in $\mathbf{C}at{Set}$.

\begin{definition}
A \emph{polynomial} in ${\cat{E}}$ is an exponentiable morphism $p \colon P_\ast \to P$ in ${\cat{E}}$, and a \emph{morphism of polynomials} $p \to q$ in ${\cat{E}}$ consists of a morphism $P \to Q$ and a morphism $P_\ast \leftarrow P \times_Q Q_\ast$. A \emph{typed polynomial} from $D$ to $C$ in ${\cat{E}}$ is a diagram $D \leftarrow P_\ast \to P \to C$ such that $P_\ast \to P$ is exponentiable, with morphisms defined similarly (\cref{defppoly}).
\mathbf{C}at{End}d{definition}

We denote by $\mathbf{C}at{Poly}_{\cat{E}}$ the category of polynomials in ${\cat{E}}$. Typed polynomials form the horizontal morphisms of a double category $\mathbb{P}oly_{\cat{E}}$ under composition (\cref{defppoly}), and this makes $\mathbf{C}at{Poly}_{\cat{E}}$ a monoidal category \cite[Section 3.2]{shapiro2023structures}. As discussed in \cite[proof of Theorem 3.15]{shapiro2023structures}, the category $\mathbf{C}at{Poly}_{\cat{E}}$  embeds fully faithfully into $\mathbf{C}at{Poly}_{a\tn{-}\mathbf{C}at{Set}}$ for $F \colon a^\tn{op} \to {\cat{E}}$ any fully faithful dense functor, e.g.\ $a\coloneqq{\cat{E}}^\tn{op}$. For such an $F$, let $F^\ast\colon{\cat{E}}\to a\tn{-}\mathbf{C}at{Set}$ be given by $F^\ast(C)(A)\coloneqq{\cat{E}}(F(A),C)$.

\begin{theorem}[Proven as \cref{proofPolyE}]\label{polyEembed}
For a fully faithful dense functor $F\colon a^\tn{op} \to {\cat{E}}$, the category $\mathbf{C}at{Poly}_{\cat{E}}$ embeds fully faithfully and strong monoidally into the horizontal category $\mathbb{C}atsharp(a,a)$. In particular, for a polynomial $P_\ast \to P$ in ${\cat{E}}$, the corresponding $(a,a)$-bicomodule is given by
\[
\sum_{A \in a(1)} \sum_{x \colon F(A) \to P} \mathcal{y}^{F^\ast(x^\ast P_\ast)}.
\]
More generally, there is a locally fully faithful double functor from $\mathbb{P}oly_{\cat{E}}$ to $\mathbb{C}atsharp$. It sends an object $C$ to the slice category $F/C \cong \int F^\ast(C)$, and a typed polynomial $D \leftarrow P_\ast \to P \to C$ to the $(F/C,F/D)$-bicomodule
\[
\sum_{\substack{A \in a(1) \\ F(A) \to C}} 
\sum_{x \in \Hom_{/C}(F(A),P)}

\mathcal{y}^{F^\ast(x^\ast P_\ast)}.\qedhere
\]
\mathbf{C}at{End}d{theorem}

\section{Structures in $\mathbf{C}at{Poly}_{\cat{E}}$ and $\mathbb{C}atsharp$}

Following \cite[Proposition 2.7.1]{spivak2021functorial}, the category of $(c,d)$-bicomodules has a monoidal structure $(c(1)\mathcal{y}^{d(1)},\ot{c}{d})$ where the tensor product is given by
\[
p \ot{c}{d} q \coloneq \sum_{C \in c(1)} \sum_{(I,J) \in p_C(1) \times q_C(1)} \mathcal{y}^{p[I] \times_{d(1)} q[J]},
\]
where the fiber product $\times_{d(1)}$ of directions is the product on $d$-copresheaves. The composition product $\mathbin{\triangleleft}$ has a right coclosure $\lens{-}{-}$ (\cref{coclosure}). 

In \cite[Chapter 4]{shapiro2023structures}, a tensor product $\otimes$, closure for $\otimes$, and coclosure for $\mathbin{\triangleleft}$ are defined in $\mathbf{C}at{Poly}_{\cat{E}}$, though the latter two require additional assumptions on the category ${\cat{E}}$.

\begin{corollary}[Proven as \cref{Etensorproof,coclosureproof}]\label{preservesstructure}
The monoidal functor of \cref{polyEembed} is lax monoidal with respect to $\otimes$ and $\ot{a}{a}$, and preserves $\mathbin{\triangleleft}$-coclosures up to isomorphism when they exist.
\mathbf{C}at{End}d{corollary}

The failure of strong monoidality here arises from the fact that in the category $a\tn{-}\mathbf{C}at{Set}$, the fibers of a product of morphisms are given not by products of fibers but by fiber products.

\chapter{Lawvere Theories and Nerves of Higher Categories in $\mathbb{C}atsharp$}

The nerve functor from categories to simplicial sets allows the algebraic structure of a category to be modeled using only the geometric structure of combinatorial simplices. Variants of the nerve construction proliferate in the literature for various flavors of higher categories, such as 2-categories, multicategories, and double categories, each landing in a presheaf category whose cell shapes correspond to the composable shapes in the higher category structure. Nerves are in fact a generalization of models for Lawvere theories, which also model algebraic structures on sets as presheaves.

Most of these structures, including all nerves and the Lawvere theories corresponding to $\sigma$-free symmetric operads (or in the multisorted case, multicategories), arise as algebras for a monad on a presheaf category whose underlying endofunctor is a parametric right adjoint: that is, a monad in $\mathbb{C}atsharp$. In fact, for any such monad we can define its (generalized) Lawvere theory and the corresponding nerve construction using only categorical operations in $\mathbb{C}atsharp$.

\section{Familial monads and theory categories}

The $\mathit{path}$ monad on graphs (see \cref{pathmonad}), whose algebras are categories, is an example of a ``familial'' monad: one whose underlying endofunctor is a parametric right adjoint on a presheaf category, and hence arises from a monad in $\mathbb{C}atsharp$. There are many examples of such monads whose algebras are various types of higher and ``lower'' categories, such as:
\begin{itemize}
	\item any $\Sigma$-free symmetric operad corresponds to a familial monad on sets \cite[Example C.2.5]{Leinster:2004a}; 
	\item the free $n$-category monad on $n$-graphs (also known as $n$-globular sets) \cite[Proposition F.2.3]{Leinster:2004a}; 
	\item the free double category monad on double graphs \cite[Example 1.14]{shapiro2022thesis};
	\item the free (symmetric or nonsymmetric) multicategory monad on multigraphs\footnote{We use the category theorists' convention that graphs are by default directed with loops and multiple edges, so that the term ``multigraph'' may refer to the data underlying a multicategory.} \cite[Example 2.14]{weber2007familial}; and 
	\item the free symmetric monoidal category monad on graphs.\footnote{This example is explained in some detail at \href{https://youtu.be/u8XCiI-ZSHc?t=10}{https://youtu.be/u8XCiI-ZSHc?t=10}.}
\mathbf{C}at{End}d{itemize}

In each case there is a category $c$ and a $(c,c)$-bicomodule 
\[
m = \sum_{C \in c(1)}\sum_{M \in m_C(1)} \mathcal{y}^{m[M]},
\]
where $c$-sets model the ``cells'' of the higher categories in question, and the \emph{arities} $m[M]$ are the copresheaves on $c$ describing the arrangements of cells which can be composed into a $C$-cell, such as the graphs $\vec n$ which compose to a morphism in a category. The monad structure ensures that the \emph{operations} $M \in m(1)$ are closed under identities and substitutions.

Much like categories, for which the nerve is a simplicial set with an $n$-simplex for each arrangement of $n$ adjacent edges in the category, higher categories also have nerves which are copresheaves on a \emph{theory} category, whose objects are the operations and whose morphisms are given by maps between the free algebras generated by the arities. This category is typically defined as a full subcategory of free $m$-algebras, but $\mathbb{C}atsharp$ provides a definition in terms of universal properties via the \emph{right coclosure} of the composition product. 

\begin{definition}[{\cite[Proposition 2.4.6]{spivak2021functorial}}]\label{coclosure}
For a $(d,e)$-bicomodule $q$, the functor $- \mathbin{\triangleleft}_d q$ from $(c,d)$-bicomodules to $(c,e)$-bicomodules has a left adjoint $\lens{-}{q}$. For a $(c,e)$-bicomodule $p$ its carrier is defined to be
\begin{equation}\label{eqn.coclosure}
\lens{p}{q} \coloneq \sum_{C \in c(1)}\sum_{I \in p_C(1)} \mathcal{y}^{q \mathbin{\triangleleft}_e p[I]},
\mathbf{C}at{End}d{equation}
where $p[I]$ is regarded as a $(e,0)$-bicomodule.
\mathbf{C}at{End}d{definition}

The unit of this adjunction is a canonical morphism of $(c,e)$-bicomodules $p \to \lens{p}{q} \mathbin{\triangleleft}_d q$. The coclosure from \cref{eqn.coclosure} corresponds to the left Kan extension
\[
\begin{tikzcd}
	c\ar[r,bimr-biml, "p", ""' name=p]&
	e\ar[d,biml-bimr, "q"]\\&
	d\ar[ul, bend left, biml-bimr, pos=.8, "\lens{p}{q}", ""' name=cocl]
	\ar[from=p, to=p|-cocl.south, shorten >=-8pt, Rightarrow]
\mathbf{C}at{End}d{tikzcd}
\hspace{1in}
\begin{tikzcd}
	e\tn{-}\mathbf{C}at{Set}\ar[d, "q\mathbin{\triangleleft}-"']\ar[r, "p\mathbin{\triangleleft}-", ""' name=p]&
	c\tn{-}\mathbf{C}at{Set}\\
	d\tn{-}\mathbf{C}at{Set}\ar[ur, bend right, "\tn{Lan}"', "" name=cocl]
	\ar[from=p, to=p|-cocl.south, shorten >=0pt, Rightarrow]
\mathbf{C}at{End}d{tikzcd}
\]

\begin{definition}
For $m$ a monad on $c$ in $\mathbb{C}atsharp$, its \emph{theory category} $\Theta_m$ is the opposite of the $(c,c)$-bicomodule $\lens{m}{m \mathbin{\triangleleft}_c m}$, which by \cref{thetacomonoid} has the structure of a comonoid in $\mathbb{C}atsharp$ and whose carrier is by \cref{comonadcofunctor} a category.
\mathbf{C}at{End}d{definition}

\begin{lemma}[Dual to {\cite[Remark 5.15]{Cruttwell.Shulman:2010a}}]\label{comonadcofunctor}
For $c$ a polynomial comonoid, given a $(c,c)$-bicomodule $e$ with the structure of a $(c,\mathbin{\triangleleft}_c)$-comonoid, the carrier polynomial $e$ itself forms a comonoid equipped with a homomorphism to $c$. 
\mathbf{C}at{End}d{lemma}

Unwinding this definition, the category $\Theta_m$ has as objects $m(1)$, the set of operations of $m$, and as morphisms into $M$ the set $m \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c m[M] = \sum_{M' \in m(1)} \Hom_{c\tn{-}\mathbf{C}at{Set}}(m[M'],m \mathbin{\triangleleft}_c m[M])$ of Kleisli morphisms from $m[M']$ to $m[M]$ for the familial monad $m$ on $c\tn{-}\mathbf{C}at{Set}$. This agrees with Weber's category $\Theta_T$ \cite[above Definition 4.4]{weber2007familial} when $T$ is taken to be the familial monad on $c\tn{-}\mathbf{C}at{Set}$ corresponding to $m$, using the correspondence between Kleisli morphisms and maps between free algebras.

\begin{example}
For the monad $\mathit{path}$, the theory category $\Theta_\mathit{path}$ has as objects the set $\{0\} + \mathbb{N}$ of natural numbers with two distinct copies of 0 and as morphisms $k \to \ell$ Kleisli arrows $\vec k \to \mathit{path} \mathbin{\triangleleft}_g \vec \ell$, or equivalently functors $\mathit{path} \mathbin{\triangleleft}_g \vec k \to \mathit{path} \mathbin{\triangleleft}_g \vec \ell$, where the domain and codomain are the ordinal categories $[k]$ and $[\ell]$. Thus $\Theta_{\mathit{path}}$ coincides with the simplex category ${\cat{D}}elta$, albeit with two isomorphic copies of the terminal category $\mathit{path} \mathbin{\triangleleft}_g \vec 0$,\footnote{This choice of category in the equivalence class of ${\cat{D}}elta$ admits a cofunctor from its opposite category to $g$, and is used in \cite[Section 6]{shapiro2022thesis} as a convenient convention for general theory categories.} corresponding to the nerve of a category being a simplicial set, equivalently a $\lens{\mathit{path}}{\mathit{path} \mathbin{\triangleleft}_g \mathit{path}}$-comodule.
\mathbf{C}at{End}d{example}

\begin{example}
This construction also recovers the appropriate type of presheaves for the nerves of various types of higher categories:
\begin{itemize}
	\item the theory category for the free $n$-category monad is Joyal's category $\Theta_n$, whose objects are free pasting diagrams of globular cells up to dimension $n$ \cite[Example 4.18]{weber2007familial}; 
	\item for the free double category monad it is ${\cat{D}}elta \times {\cat{D}}elta$ whose objects are finite grids; and
	\item for the free (symmetric/nonsymmetric) multicategory monad it is the (ordinary/planar) dendroid category $\Omega$ whose objects are planar trees (in the symmetric case equipped with a permutation on the leaves).\cite[Example 2.14]{weber2007familial} \qedhere
\mathbf{C}at{End}d{itemize}
\mathbf{C}at{End}d{example}

For some monads, such as $\Sigma$-free symmetric operads, it is desirable to have the objects of the theory category be indexed not by the operations of the monad itself, but rather by the operations of some other bicomodule. Given a monad $m$ on $c$ in $\mathbb{C}atsharp$ and a $(d,c)$-bicomodule $p$, the coclosure $(d,d)$-bicomodule $\lens{p}{p \mathbin{\triangleleft}_c m}$ forms a comonad on $d$ (\cref{thetacomonoid}) and corresponds to the opposite of the full subcategory of the Kleisli category of $m$ spanned by the $c$-copresheaves of the form $p[I]$. We call the opposite of this category $\Theta_m^p$.

\begin{example}
For $O$ a $\Sigma$-free symmetric operad regarded as a polynomial monad and $\mathit{list}$ the polynomial $\sum\limits_{N \in \mathbb{N}} \mathcal{y}^{\underline N}$ whose arity $\underline N$ is the finite set $\{1,...,N\}$, the category $\lens{\mathit{list}}{\mathit{list} \mathbin{\triangleleft} O}$ is the opposite of the skeleton of the category of finitely generated free $O$-algebras. This is precisely the Lawvere theory corresponding to the finitary monad associated to $O$.\cite[Example 4.15]{weber2007familial} The theory category $\Theta_O$, by comparison, may have many more objects (one for each operation in $O$ rather than one for each finite arity) and does not necessarily include all finite arities as $O$ may have no $N$-ary operations for certain $N$.
\mathbf{C}at{End}d{example}

\section{Nerves}

Given a monad $m$ on $c$ in $\mathbb{C}atsharp$ and a $(d,c)$-bicomodule $p$, to construct from an $m$-algebra a presheaf on $\Theta_m^p$, equivalently a $\left(\lens{p}{m \mathbin{\triangleleft}_c m},0\right)$-bicomodule, we use the fact that copresheaves on $\lens{p}{p \mathbin{\triangleleft}_c m}$ are equivalent to left $\lens{p}{p \mathbin{\triangleleft}_c m}$-comodules among $(d,0)$-bicomodules (\cref{lenscoalgebras}). 

For an $m$-algebra $A$ then, modeled as a $(c,0)$-bicomodule with a left module structure $m \mathbin{\triangleleft}_c A \to A$, its nerve has as elements $p \mathbin{\triangleleft}_c A$. This copresheaf on $c$ has the structure of a $\lens{p}{p \mathbin{\triangleleft}_c m}$-comodule as constructed in \eqref{eqn.nerve}, giving it the structure of a presheaf on $\Theta_m^p$. 
\begin{equation}\label{eqn.nerve}
\begin{tikzcd}
d \ar[bimr-biml,""{name=S, below}]{rrr}{p} \ar[bimr-biml]{dr}[swap]{\lens{p}{p \mathbin{\triangleleft}_c m}} & & & c \rar[bimr-biml]{A} \dar[Rightarrow,shorten >=9,shorten <=3] & 0 \\
& d \rar[bimr-biml,""{name=T, above},swap]{p} & c \ar[bimr-biml]{ur}[description]{m} \ar[bimr-biml,bend right=20]{urr}[swap]{A} & {}
\arrow[Rightarrow,shorten=4,from=S,to=T]
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}

\begin{theorem}[Proved as \cref{thm.nerveproof}]\label{nervecoalgebra}
This construction of the nerve of an $m$-algebra is a $\Theta_m^p$-presheaf which when $p=m$ agrees with the nerve given by Weber in \cite[Definition 4.4]{weber2007familial}.
\mathbf{C}at{End}d{theorem}

Note that an element of $m \mathbin{\triangleleft}_c A$ consists of an operation $M \in m_C(1)$ and a map of $c$-copresheaves $m[M] \to A$, equivalently a map of $m$-algebras from $m \mathbin{\triangleleft}_c m[M]$ to $A$, precisely the definition of an $M$-cell in Weber's nerve of $A$ from \cite[Definition 4.4]{weber2007familial}. 

\chapter{Open dynamics and computational effects in $\mathbb{C}atsharp$}

Algebraic effects and effect handlers are a popular way of working with side effects in functional programming languages and they have received much research and development in the last decade, both via new languages and integration into current functional languages like OCaml, Haskell, and Scala \cite{leijen_koka_2014, bauer_programming_2015, ocaml_ocaml_2022, king_7942_2022, odersky_capabilities_2022}.

The idea is that instead of directly implementing side effects, an effectful program should instead signal that a side effect should be performed, and another program should ``handle'' that signal, afterwards returning control flow to the original program along with the result of that effect. The advantage of this is that side effects can be handled in different ways. For instance, the side-effect of accessing a database could be implemented with an in-memory database, an on-file database, a dummy database, or a database distributed across the entire world. The application logic should be indifferent to this implementation.

We can model a program that uses effects as a polynomial coalgebra, i.e. a set of ``states'' $S$ along with a function $\vartheta \colon S \to p(S)$ for some polynomial $p$. The positions $I \in p(1)$ represent the different effects that can be ``thrown'', and then the directions $x \in p[I]$ represent the possible results of that effect returned to the program. Given a state $s \in S$, $\vartheta(s)$ represents running the program until the next effect is thrown, and then returning that effect $I$ along with a continuation function $p[I] \to S$ saying what the next state is given the result of the effect. A position $I \in p(1)$ with $p[I] = \emptyset$ signals termination of the program.

An effect handler is then something which ``migrates'' a $p$-coalgebra to a $q$-coalgebra. For instance, this could translate abstract database accesses into UNIX system calls to the network stack. 

\section{Effects handlers}

\begin{definition}\label{def.eff}
For polynomial comonoids $c,d$, a \emph{$(c,d)$-effects handler} is a pair $(s,\varphi)$ where $s:\mathbf{C}at{Poly}$ and $\varphi$ is a morphism $c \mathbin{\triangleleft} s {\cat{F}}rom{\varphi} s \mathbin{\triangleleft} d$ which commutes with counits and comultiplications in the sense of \cref{eqn.eff}. We say it is \emph{linear} if $s=S\mathcal{y}$ for some $S:\mathbf{C}at{Set}$.

For polynomials $p,q$, a \emph{$(p,q)$-effects handler} is a polynomial $s$ equipped with a morphism $p \mathbin{\triangleleft} s {\cat{F}}rom{\varphi} s \mathbin{\triangleleft} q$. We refer to these as \emph{elementary effects handlers}. As one might expect, elementary effects handlers can be regarded as effects handlers; see \cref{prop.elem_as_eff}.
\mathbf{C}at{End}d{definition}

For a $(c,d)$-effects handler $s$ and a $(d,e)$-effects handler $t$, we get a $(c,e)$-effects handler $s \mathbin{\triangleleft} t$ given by the composite $c \mathbin{\triangleleft} s \mathbin{\triangleleft} t \leftarrow s \mathbin{\triangleleft} d \mathbin{\triangleleft} t \leftarrow s \mathbin{\triangleleft} t \mathbin{\triangleleft} e$, and given comonoid homomorphisms $c \to c'$ and $d \to d'$ we can define a square from a $(c,d)$-effects handler $s$ to a $(c',d')$-effects handler $s'$ as a morphism of polynomials $s \to s'$ which commutes with the effects handler structure maps. In this way, comonoids, homomorphisms, effects handlers, and squares between them form a pseudo-double category $\mathbb{E}\mathbf{C}at{ff}$. 
There is similarly a pseudo-double category $\mathbb{E}\mathbf{C}at{ff}el$ of elementary effects handlers without the comonoid structure on objects or morphisms, which includes into $\mathbb{E}\mathbf{C}at{ff}$ by the cofree comonoid functor $\cofree{}$ from \cref{prop.cofree}.

In fact, any $(c,d)$-effects handler $(s,\varphi)$ induces a $(c,d)$-bicomodule $c\bifrom[s\mathbin{\triangleleft} d]d$ with left and right structure maps $(\varphi\mathbin{\triangleleft} d)\circ(s\mathbin{\triangleleft}\delta_d)$ and $s\mathbin{\triangleleft}\delta_d$, as in \eqref{eqn.bicomod_for_eff}
\begin{equation}\label{eqn.bicomod_for_eff}
c \mathbin{\triangleleft} s \mathbin{\triangleleft} d {\cat{F}}rom{\varphi\mathbin{\triangleleft} d} s \mathbin{\triangleleft} d \mathbin{\triangleleft} d {\cat{F}}rom{s\mathbin{\triangleleft}\delta_d} s \mathbin{\triangleleft} d \To{s\mathbin{\triangleleft}\delta_d} s \mathbin{\triangleleft} d \mathbin{\triangleleft} d.
\mathbf{C}at{End}d{equation}

\newcommand{\mathbb{E}\mathbf{C}at{ff}body}{
The pseudo-double category of effects handlers admits a pseudo-double functor $\mathbb{E}\mathbf{C}at{ff}\to\mathbb{C}atsharp$ which is the identity on objects and vertical morphisms and which is faithful on the category of horizontal morphisms between nonempty categories and squares between them. Moreover, every $(c,0)$- and $(c,\mathcal{y})$-bicomodule is in the essential image.}
\begin{theorem}[Proved as \ref{thm.eff}]\label{thm.eff_statement}
\mathbb{E}\mathbf{C}at{ff}body
\mathbf{C}at{End}d{theorem}

\section{Polynomial coalgebras and the double category ${\mathbb{O}\mathbf{C}at{rg}}$}

\begin{definition}\label{pqcoalg}
The closure $[-,-]$ of the monoidal structure $(\mathcal{y},\otimes)$ on $\mathbf{C}at{Poly}$ is given by
\[
[q,p] \coloneq \sum_{\phi \colon q \to p} \mathcal{y}^{\sum\limits_{I \in q(1)} p[\phi_1I]}
\]
for polynomials $p,q$. A $[q,p]$-coalgebra is a set $S$ equipped with a function $S \to [q,p](S)$.
\mathbf{C}at{End}d{definition}

In \cite{spivak2021learners,shapiro2022dynamic}, the authors describe a double category ${\mathbb{O}\mathbf{C}at{rg}}$ whose vertical category is that of polynomials, whose horizontal morphisms from $q$ to $p$ are the $[q,p]$-coalgebras $S\to [q,p]\mathbin{\triangleleft} S$, and whose squares are maps $S\to S'$ satisfying a certain commutativity condition. Monoidal categories and operads enriched in ${\mathbb{O}\mathbf{C}at{rg}}$ include the process of training a deep learning system and running a prediction market.

It turns out that the category of $[q,p]$-coalgebras is equivalent to that of elementary $(p,q)$-effects handlers of the form $(S\mathcal{y},\varphi)$ for some $S:\mathbf{C}at{Set}$, i.e.\ whose carrier is linear,
\footnote{Note that this is not a contravariant assignment, as a $(p,q)$-effects handler is regarded as a morphism from $q$ to $p$ in $\mathbb{E}\mathbf{C}at{ff}$, a convention inherited from $\mathbb{C}atsharp$.} an assignment which furthermore extends to the entire structure of ${\mathbb{O}\mathbf{C}at{rg}}$.

\newcommand{{\mathbb{O}\mathbf{C}at{rg}}body}{
There is a pseudo-double functor ${\mathbb{O}\mathbf{C}at{rg}}\to\mathbb{E}\mathbf{C}at{ff}el$ which is the identity on objects and vertical morphisms and fully faithful on the category of horizontal morphisms and squares, with essential image given by the linear elementary effects handlers.
}
\begin{theorem}[Proved as \cref{thm.org}]\label{thm.org_statement}
{\mathbb{O}\mathbf{C}at{rg}}body
\mathbf{C}at{End}d{theorem}

We have now defined a string of locally fully faithful pseudo-double functors
\[
{\mathbb{O}\mathbf{C}at{rg}} \to \mathbb{E}\mathbf{C}at{ff}el \to \mathbb{E}\mathbf{C}at{ff} \to \mathbb{C}atsharp
\]
which acts by $\cofree{} \colon \mathbf{C}at{Poly} \to \mathbf{C}at{Poly}$ on the vertical category and sends a coalgebra $S \to [q,p](S)$ to the $(\cofree p,\cofree q)$-effects handler $\cofree p \mathbin{\triangleleft} S\mathcal{y} \leftarrow S\mathcal{y} \mathbin{\triangleleft} \cofree q$ sending a state $s_0 \in S$ and a $q$-behavior tree $T$ to the behavior tree of $p$ obtained by running the coalgebra on $s_0$ and each state reached by the paths through $T$, labeled by the states reached along the way.

\printbibliography

\appendix

\chapter{Functoriality of $\mathbb{P}oly_{\cat{E}} \to \mathbb{C}atsharp$}

Throughout this appendix, let ${\cat{E}}$ be a category with pullbacks.

\begin{definition}[{Based on \cite[Section 3]{kock2012polynomial} and \cite[Section 5.3]{shapiro2023structures}}]\label{defppoly}
The double category $\mathbb{P}oly_{\cat{E}}$ of typed polynomials in ${\cat{E}}$ has
\begin{itemize}
	\item as objects, objects of ${\cat{E}}$;
	\item as vertical morphisms, morphisms of ${\cat{E}}$;
	\item as horizontal morphisms from $D$ to $C$, typed polynomials from $D$ to $C$;
	\item as squares between morphisms $f,g$ and types polynomials $P_\ast \to P$ and $P'_\ast \to P'$, isomorphism classes of commuting diagrams as in \eqref{eqn.typedmorphism}, where the isomorphisms are between choices of pullbacks;
\begin{equation}\label{eqn.typedmorphism}
\begin{tikzcd}
D \ar{dd}[swap]{f} & P_\ast \rar \lar & P \dar[equals] \rar & C \ar{dd}{g} \\
& \bullet \dar \uar{\phi^\ast} \rar \ar[phantom]{dr}[pos=0]{\lrcorner} & P \dar{\phi_1} \\
D' & P'_\ast \lar \rar & P' \rar & C'
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}
	\item as horizontal identities, typed polynomials of the form $C = C = C = C$; and
	\item composition of typed polynomials $P_\ast \to P$ and $Q_\ast \to Q$ given by the composite of the top row of morphisms of \eqref{eqn.typedcompose},
\begin{equation}\label{eqn.typedcompose}
\begin{tikzcd}
& \bullet_2 \ar{dd} \ar{rr} \ar[phantom]{ddrr}[pos=0]{\lrcorner} &[25pt] &[-20pt] \bullet_1 \ar{rr} \dar \ar[phantom]{ddrr}[pos=0]{\lrcorner} &[-25pt] & {\Cat{P}}i_p (Q \times_D P_\ast) \ar{dd} &[-25pt] {} \\
& & & Q \times_D P_\ast \ar{dl} \ar{dr} \\
& Q_\ast \rar{q} \ar{dl}[swap]{} & Q \ar{dr}{} & {} & P_\ast \rar{p} \ar{dl}[swap]{} & P \ar{dr}{} \\
E & & & D & & & C
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}
where ${\Cat{P}}i_p(Q \times_D P_\ast)$ is defined by the universal property that morphisms into it from an object $A$ correspond to pairs $(f_1 \colon A \to P, f_2 \colon f_1^\ast P_\ast \to Q)$ with $f_2$ commuting with $f_1^\ast P_\ast \to P_\ast$ over $D$.  
\mathbf{C}at{End}d{itemize}
As we discuss in the proof of \cref{proofPolyE}, as we are constructing a fully faithful strong double functor out of $\mathbb{P}oly_{\cat{E}}$ there is no need to define horizontal composition of squares. Vertical composition of squares is as given for morphisms of untyped polynomials in \cite[Definition 3.13]{shapiro2023structures}, though similarly by fully faithfulness of the double functor constructed out of $\mathbb{P}oly_{\cat{E}}$ it is not strictly necessary to define this composition as it can be deduced from the vertical composition of squares in $\mathbb{C}atsharp$.
\mathbf{C}at{End}d{definition}

Before proving that this double category maps into $\mathbb{C}atsharp$, we first describe how the identities and composition of bicomodules given in \cref{defcatsharp} behaves under the correspondence with prafunctors from \cref{defprafunctor}. For a $(c,d)$-bicomodule $p$ and a $(d,e)$-bicomodule $q$ of the forms
\[
p = \sum_{C \in c(1)}\sum_{I \in p_C(1)} \mathcal{y}^{p[I]} \mathbb{Q}and q = \sum_{D \in d(1)}\sum_{J \in q_D(1)} \mathcal{y}^{q[J]},
\]
the equalizer of $p \mathbin{\triangleleft} q \rightrightarrows p \mathbin{\triangleleft} d \mathbin{\triangleleft} q$ has as positions the subset of functions $p[I] \to q(1)$ which are morphisms between the associated $d$-copresheaf structures; this is because the two maps to $p \mathbin{\triangleleft} d \mathbin{\triangleleft} q$ each append such a map with the data of either the restrictions of elements of $p[I]$ under maps in $d$ or those of elements in $q(1)$, which in the equalizer must agree. The directions for a position given by $f \colon p[I] \to q(1)$ is the coequalizer of the disjoint union 
\[
(p \mathbin{\triangleleft} q)[I,f] = \sum_{i \in p[I]} q[f(i)]
\]
under the maps respectively sending $i$ to its restrictions along maps in $d$ within the $d$-copresheaf $p[I]$ and mapping $q[f(i)]$ to the arities of the restriction of $f(i)$ along maps in $d$ according to the left $d$-module structure of $q$ on directions. These identifications turn the disjoint union $(p \mathbin{\triangleleft} q)[I,f]$ into the corresponding colimit 
\[
(p \mathbin{\triangleleft}_d q)[I,f] = \colim_{i \in p[I]} q[f(i)]
\]
indexed by the category of elements of $p[I]$ as a $d$-copresheaf. It is easily checked (as stated in \cite[Proposition 1.8]{shapiro2022thesis} and a consequence of the proofs of \cite[Propositions 3.11,3.12]{garner2018shapely}) that these positions and directions agree with those of the composite of the corresponding parametric right adjoint functors.

The identity bicomodule $c \bifrom[c] c$ has the form $\sum\limits_{C \in c(1)} \mathcal{y}^{c[C]}$, so it has a single operation for each object of $c$ with arity the corepresentable copresheaf $c[C]$.

\begin{theorem}\label{proofPolyE}
For a fully faithful dense functor $F \colon a^\tn{op} \to {\cat{E}}$, there is a locally fully faithful pseudo-double functor from $\mathbb{P}oly_{\cat{E}}$ to $\mathbb{C}atsharp$. It sends an object $C$ to the slice category $F/C \cong \int F^\ast(C)$, and a typed polynomial $D \leftarrow P_\ast \to P \to C$ to the $(F/C,F/D)$-bicomodule
\[
\sum_{\substack{A \in a(1) \\ F(A) \to C}} 
\sum_{\tiny{\begin{tikzcd}[row sep=tiny,column sep=tiny] x \colon F(A) \ar{rr} \ar{dr} & & P \ar{dl} \\ & C \mathbf{C}at{End}d{tikzcd}}}
\mathcal{y}^{F^\ast(x^\ast P_\ast)}.
\]
\mathbf{C}at{End}d{theorem}

Here ``locally fully faithful'' means that for any fixed square boundary in $\mathbb{P}oly_{\cat{E}}$, the function from its square fillers to squares with the corresponding boundary in $\mathbb{C}atsharp$ is a bijection. In particular this implies that the category of typed polynomials in ${\cat{E}}$ from $D$ to $C$ maps fully faithfully to the category of $(F/C,F/D)$-bicomodules. In the case when ${\cat{E}}$ has finite limits, the first statement of \cref{polyEembed} follows from setting $C$ and $D$ to be the terminal object, resulting in a fully faithful strong monoidal functor from $\mathbf{C}at{Poly}_{\cat{E}}$ to $(a,a)$-bicomodules.

Note that $F^\ast(x^\ast P_\ast)$, as an $a$-copresheaf over $F^\ast(D)$, is equivalently regarded as a copresheaf on $F/D$.

\begin{proof}
Following the approach of \cite[Section 3.2]{shapiro2023structures}, as the assignment $C \mapsto F/C$ is clearly functorial on the vertical categories, it suffices to show that the assignment on horizontal morphisms preserves identities and composition up to coherent isomorphism and that the given assignments are indeed locally fully faithful. The remaining structure and properties of a pseudo-double functor can then be deduced using local fully faithfulness, in the style of \cite[Proposition 3.25]{shapiro2023structures}, as can the composition of squares in $\mathbb{P}oly$.\footnote{The specific analogue of that proposition would proceed by: 1) defining a tentative pseudo-double category as a pair of categories with the same objects and sets of squares filling boundaries of the appropriate type; 2) defining a tentative pseudo-double functor as an assignment on the categories and squares preserving vertical composition strictly and horizontal composition up to bidirectional squares; and 3) concluding that a tentative pseudo-double category with a locally fully faithful tentative pseudo-double functor to an established pseudo-double category endows the domain with the structure of a pseudo-double category such that the tentative pseudo-double functor is in fact a pseudo-double functor.} 

The identity polynomial $C = C = C = C$ is sent to the $(F/C,F/C)$-bicomodule
\[
\sum_{\substack{A \in a(1) \\ F(A) \to C}} \sum_{x \in \Hom_{{\cat{E}}/C}(F(A),C)} \mathcal{y}^{F^\ast(x^\ast C)} \quad\cong\quad \sum_{\substack{A \in a(1) \\ F(A) \to C}} \mathcal{y}^{F^\ast(F(A))} \quad\cong\quad \sum_{\substack{A \in a(1) \\ F(A) \to C}} \mathcal{y}^{a[A]},
\]
as since $F$ is fully faithful $F^\ast(F(A)) \cong a[A]$. As an $F/C$-copresheaf, thiscopy of $a[A]$ corresponds to the copresheaf corepresented by the map $F(A) \to C$, whose elements are in bijection with the set $a[A]$. This is precisely the form of the identity $(F/C,F/C)$-bicomodule, so our desired double functor preserves horizontal identities.

For typed polynomials $D \leftarrow P_\ast \To{p} P \to C$ and $E \leftarrow Q_\ast \To{q} Q \to D$, their composite in $\mathbb{P}oly_{\cat{E}}$ is sent to the $(F/C,F/E)$-bicomodule
\[
\sum_{\substack{A \in a(1) \\ F(A) \to C}} \sum_{x \in \Hom_{{\cat{E}}/C}(F(A),{\Cat{P}}i_p(Q \times_D P_\ast))} \mathcal{y}^{F^\ast(x^\ast \bullet_2)},
\]
where $\bullet_2$ is defined via pullbacks in \eqref{eqn.typedcompose}, and the composite of the associated bicomodules in $\mathbb{C}atsharp$ is the $(F/C,F/E)$-bicomodule
\[
\sum_{\substack{A \in a(1) \\ F(A) \to C}} \sum_{\substack{x_1 \in \Hom_{{\cat{E}}/C}(F(A),P) \\ x_2 \in \Hom_{d\tn{-}\mathbf{C}at{Set}/F^\ast(D)}(F^\ast(x_1^\ast P_\ast),F^\ast(Q))}} \mathcal{y}^{\colim\limits_{y \colon a[A'] \to F^\ast(x_1^\ast P_\ast)} y^\ast F^\ast(x_2^\ast Q_\ast)}.
\]

By the universal property of ${\Cat{P}}i_p(Q \times_D P_\ast)$, a morphism $x \colon F(A) \to {\Cat{P}}i_p(Q \times_D P_\ast)$ commuting over $C$ corresponds to a morphism $x_1 \colon F(A) \to P$ commuting over $C$ along with a map $\bar x_2 \colon x_1^\ast P_\ast \to Q$ commuting over $D$. As the functor $F^\ast$ is fully faithful, maps of the form $x_2$ and $\bar x_2$ are is bijective correspondence, so these bicomodules agree on positions.

To compute the pullback $x^\ast \bullet_2$ in terms of the maps $x_1,x_2$, consider the extension of \eqref{eqn.typedcompose} given in \eqref{eqn.composepb}.
\begin{equation}\label{eqn.composepb}
\begin{tikzcd}
& x_2^\ast Q_\ast \ar{rr} \dar \ar[phantom]{dr}[pos=0]{\lrcorner} &[25pt] &[-20pt] x_1^\ast P_\ast \ar{rr} \dar \ar[phantom]{dr}[pos=0]{\lrcorner} \ar[bend right=20]{dddl}[swap]{x_2} &[-25pt] & F(A) \dar{x} \ar[bend left=60]{ddd}{x_1} &[-25pt] {} \\
& \bullet_2 \ar{dd} \ar{rr} \ar[phantom]{ddrr}[pos=0]{\lrcorner} & {} & \bullet_1 \ar{rr} \dar \ar[phantom]{ddrr}[pos=0]{\lrcorner} & {} & {\Cat{P}}i_p (Q \times_D P_\ast) \ar{dd} \\
& & & Q \times_D P_\ast \ar{dl} \ar{dr} \\
& Q_\ast \rar{q} \ar{dl}[swap]{} & Q \ar{dr}{} & {} & P_\ast \rar{p} \ar{dl}[swap]{} & P \ar{dr}{} \\
E & & & D & & & C
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}
The pullback $x^\ast \bullet_1$ agrees with $x_1^\ast P_\ast$ by the cancellation property of pullbacks, as $x_1$ factors through $x$. Similarly, as $x_2$ factors through the projection $x_1^\ast P_\ast \to \bullet_1$, the pullback of the latter to $\bullet_2$ agrees with $x_2^\ast Q_\ast$. By composition of pullbacks then, we have that $x^\ast \bullet_2 \cong x_2^\ast Q_\ast$, so to show that our desired double functor indeed preserves horizontal composition it suffices to show that
\begin{equation}\label{eqn.directionsiso}
F^\ast(x_2^\ast Q_\ast) \cong \colim_{y \colon a[A'] \to F^\ast(x_1^\ast P_\ast)} y^\ast F^\ast(x_2^\ast Q_\ast).
\mathbf{C}at{End}d{equation}

To see this, recall the canonical colimit decomposition
\begin{equation}\label{eqn.canonicalcolim}
F^\ast (x_1^\ast P_\ast) \cong \colim_{y \colon a[A'] \to F^\ast(x_1^\ast P_\ast)} a[A']
\mathbf{C}at{End}d{equation}
of an object in a copresheaf category. As $a\tn{-}\mathbf{C}at{Set}$ is locally cartesian closed, the pullback functor 
\[
a\tn{-}\mathbf{C}at{Set}/F^\ast(x_1^\ast P_\ast) \to a\tn{-}\mathbf{C}at{Set}/F^\ast(x_2^\ast Q_\ast)
\]
is a left adjoint and therefore preserves colimits. In the case of the colimit in \eqref{eqn.canonicalcolim}, this colimit preservation shows that \eqref{eqn.directionsiso} holds, as the left side is the pullback of the identity on $F^\ast(x_1^\ast P_\ast)$ to $F^\ast(x_2^\ast Q_\ast)$ and the right side is the colimit of the pullbacks $y^\ast F^\ast(x_2^\ast Q_\ast)$ of each map $a[A'] \to F^\ast(x_1^\ast P_\ast)$ along the same map. This completes the proof that our desired double functor preserves horizontal composition up to isomorphism.

It then remains to show local fully faithfulness. Consider an arrangement of typed polynomials as in \eqref{eqn.squareframe}.
\begin{equation}\label{eqn.squareframe}
\begin{tikzcd}
D \dar[swap]{f} & P_\ast \rar \lar & P \rar & C \dar{g} \\
D' & P'_\ast \lar \rar & P' \rar & C'
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}

A square filling in the associated diagram in $\mathbb{C}atsharp$ has the form of a polynomial morphism
\[
\sum_{\substack{A \in a(1) \\ z \colon F(A) \to C}} 
\sum_{x \in \Hom_{{\cat{E}}/C}(F(A),P)}
\mathcal{y}^{F^\ast(x^\ast P_\ast)}
\To{\phi}
\sum_{\substack{A \in a(1) \\ z' \colon F(A) \to C'}} 
\sum_{x' \in \Hom_{{\cat{E}}/C'}(F(A),P')}
\mathcal{y}^{F^\ast(x'^\ast P'_\ast)}
\]
where $(A,z \colon F(A) \to C)$ is sent to the composite $(A,g \circ z \colon F(A) \to C \to C')$, the maps
\[
\phi_1^{A,z} \colon \Hom_{{\cat{E}}/C}(F(A),P) \to \Hom_{{\cat{E}}/C'}(F(A),P')
\]
are natural in $A$ and $z \colon F(A) \to C$, and the maps of $a$-copresheaves on directions
\[
\phi^\#_x \colon F^\ast(\phi_1^{A,z}(x)^\ast P'_\ast) \to F^\ast(x^\ast P_\ast)
\]  
are natural in $x$ (as an object in the category of elements of $F^\ast(P)$) and commute with $F^\ast(f) \colon F^\ast(D) \to F^\ast(D')$. The maps $\phi_1^{A,z}$ assemble into a map $F^\ast(P) \to F^\ast(P')$ commuting with $F^\ast(g) \colon F^\ast(C) \to F^\ast(D)$. As $F^\ast$ is fully faithful, this map arises uniquely from a map $\psi_1 \colon P \to P'$ commuting with $g$ as in \eqref{eqn.typedmorphism}.

Using the observations that $\phi_1^{A,z}(x) = \psi_1 \circ x$ and $F^\ast$ preserves pullbacks, we can equivalently express $\phi^\#_x$ as a map of the form $\bar x^\ast F^\ast(\psi_1^\ast P'_\ast) \to \bar x^\ast F^\ast(P_\ast)$, natural in $\bar x = F^\ast(x) \colon a[A] \to F^\ast(P)$. By the canonical colimit decomposition of $F^\ast(P)$ in $a\tn{-}\mathbf{C}at{Set}$ and preservation of colimits by pullbacks, such a $F/P$-indexed natural transformation is uniquely determined by a morphism $F^\ast(\psi_1^\ast P'_\ast) \to F^\ast(P_\ast)$ which commutes over $F^\ast(P)$ and, by previous assumption on $\phi^\#_x$, over $F^\ast(D')$ as well. As $F^\ast$ is fully faithful, this is equivalently a morphism $\psi_1^\ast P'_\ast \to P_\ast$ over $P$ in ${\cat{E}}$ which also commutes over $D'$.

In conclusion, we have shown that squares in $\mathbb{C}atsharp$ filling in the boundary associated to that of \eqref{eqn.squareframe} from $\mathbb{P}oly_{\cat{E}}$ correspond bijectively with squares of this form in $\mathbb{P}oly_{\cat{E}}$, completing the proof that the desired double functor is locally fully faithful, and thereby a pseudo-double functor.
\mathbf{C}at{End}d{proof}

In \cite[Section 4.1]{shapiro2023structures}, when ${\cat{E}}$ has finite limits the Dirichlet tensor product on $\mathbf{C}at{Poly}_{\cat{E}}$ is defined as the product of morphisms (though this is not a product in the category $\mathbf{C}at{Poly}_{\cat{E}}$), and is shown to form a duoidal category with the composition product. The unit of both monoidal structures is $\mathcal{y}$, the identity morphism on the terminal object.

\begin{corollary}\label{Etensorproof}
The monoidal functor of \cref{polyEembed} is lax monoidal with respect to $\otimes$ and $\ot{a}{a}$.
\mathbf{C}at{End}d{corollary}

\begin{proof}
After unwinding the definitions we can see that for polynomials $P_\ast \to P$ and $Q_\ast \to Q$ in ${\cat{E}}$,
\[
\sum_{A \in a(1)}\sum_{x \colon F(A) \to P \times Q} \mathcal{y}^{F^\ast\left(x^\ast(P_\ast \times Q_\ast)\right)}
\]
\[
\cong \sum_{A \in a(1)}\sum_{\substack{x_1 \colon F(A) \to P \\ x_2 \colon F(A) \to Q}} \mathcal{y}^{F^\ast\left(x_1^\ast(P_\ast) \times_{F(A)} x_2^\ast(Q_\ast)\right)}
\]
\[
\cong \sum_{A \in a(1)}\sum_{\substack{x_1 \colon F(A) \to P \\ x_2 \colon F(A) \to Q}} \mathcal{y}^{F^\ast\left(x_1^\ast(P_\ast)\right) \times_{a[A]} F^\ast\left(x_2^\ast(Q_\ast)\right)}
\]
by the fact that the pullback of a morphism into a product is the pullback of the pullbacks of the component morphisms, and the functor $F^\ast \colon {\cat{E}} \to a\tn{-}\mathbf{C}at{Set}$ preserves pullbacks. Here $a[A]$ denotes the corepresentable $a$-copresheaf, which agrees with $F^\ast F(A)$ as $F$ is fully faithful.

This $(a,a)$-bicomodule has a morphism from the corresponding tensor product of $(a,a)$-bicomodules
\[
\left(\sum_{A \in a(1)}\sum_{x_1 \colon F(A) \to P} \mathcal{y}^{F^\ast(x_1^\ast P_\ast)}\right) \ot{a}{a} \left(\sum_{A \in a(1)}\sum_{x_2 \colon F(A) \to Q} \mathcal{y}^{F^\ast(x_2^\ast Q_\ast)}\right)
\]
\[
= \sum_{A \in a(1)}\sum_{\substack{x_1 \colon F(A) \to P \\ x_2 \colon F(A) \to Q}} \mathcal{y}^{F^\ast\left(x_1^\ast(P_\ast)\right) \times_{a(1)} F^\ast\left(x_2^\ast(Q_\ast)\right)}
\]
induced by the inclusion from a fiber product into a product of $a$-copresheaves on the directions.

The functor sends the unit $\mathcal{y} \colon 1 = 1$ to the $(a,a)$-bicomodule
\[
\sum_{A \in a(1)} \sum_{F(A) \to 1} \mathcal{y}^{F^\ast F(A)} \cong \sum_{A \in a(1)} \sum_{F(A) \to 1} \mathcal{y}^{a[A]},
\]
which likewise admits a map from the unit $a(1)\mathcal{y}^{a(1)}$ of the monoidal structure on $(a,a)$-bicomodules, induced by the unique map $a[A] \to a(1)$ to the terminal $a$-copresheaf on directions.

The unit and associativity equations are then straightforward to deduce from the universal property of products.
\mathbf{C}at{End}d{proof}

The remaining claim of \cref{preservesstructure} then follows immediately from fully faithfulness and strong monoidality for $\mathbin{\triangleleft}$, as the universal property of the coclosure is then preserved and reflected.

\begin{corollary}\label{coclosureproof}
The monoidal functor of \cref{polyEembed} preserves the $\mathbin{\triangleleft}$-closures up to isomorphism whenever they exist.
\mathbf{C}at{End}d{corollary}

\chapter{Structure of Theories and Nerves}\label{chap.nerveproofs}

\begin{lemma}\label{thetacomonoid}
For $m$ a monad on a comonoid $c$ in $\mathbb{C}atsharp$ and $p$ any $(d,c)$-bicomodule, $\lens{p}{p \mathbin{\triangleleft}_c m}$ is a comonad on $d$.
\mathbf{C}at{End}d{lemma}

\begin{proof}
In the interest of space we construct only the counit and comultiplication transformations, but as they are derived directly from the unit and multiplication transformations of the monad $m$ it is straightforward to check that their counitality and coassociativity follow directly from unitality and associativity for $m$, respectively.

The strategy here is to use the universal property of the coclosure that morphisms of $(d,d)$-bicomodules from $\lens{p}{p \mathbin{\triangleleft}_c m}$ to $q$ are in bijective correspondence with morphisms from $p$ to $q \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$. The counit transformation $\lens{p}{p \mathbin{\triangleleft}_c m} \to d$ then corresponds to the transformation $p \to p \mathbin{\triangleleft}_c m \cong d \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$ given by the unit of $m$.

Similarly, the comultiplication $\lens{p}{p \mathbin{\triangleleft}_c m} \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m}$ corresponds to the composite 
\[
p \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \left(\lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m\right) \mathbin{\triangleleft}_c m \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m
\]
consisting of two applications of the unit of the adjunction $\lens{-}{p \mathbin{\triangleleft}_c m} \dashv - \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$ followed by the multiplication of $m$.
\mathbf{C}at{End}d{proof}

\begin{lemma}\label{lenscoalgebras}
For a comonad $e$ on an object $c$ of $\mathbb{C}atsharp$ and $d$ another object of $\mathbb{C}atsharp$, there is a carrier-preserving equivalence between $(e,d)$-bicomodules and $(c,d)$-bicomodules with the structure of a left $e$-comodule.
\mathbf{C}at{End}d{lemma}

\begin{proof}
Given a $(c,d)$-bicomodule $p$, the structure of a left $e$-comodule amounts to a morphism of polynomials $p \to e \mathbin{\triangleleft}_c p$, which by the definition of bicomodule composition induces a morphism $p \to e \mathbin{\triangleleft} p$, where the left $e$-comodule equations in $\mathbb{C}atsharp$ imply the left $e$-comodule equations in $\mathbf{C}at{Poly}$. Similarly, as $p \to e \mathbin{\triangleleft}_c p$ is a morphism of $(c,d)$-bicomodules, this $e$-coaction on $p$ in $\mathbf{C}at{Poly}$ is compatible with the right $d$-coaction on $p$, so that $p$ has the structure of a $(e,d)$-bicomodule.

By \cref{comonadcofunctor}, $e$ has a homomorphism to $c$, and as such there is a square in $\mathbb{C}atsharp$ as on the left in \eqref{eqn.cocartesian} from $e$ as the identity $(e,e)$-bicomodule to $e$ as a $(c,c)$-bicomodule given by the identity morphism on $e$. The $(e,d)$-bicomodule structure on $p$ induces a $(c,d)$-bicomodule structure where the left coaction is given by the composite $c \mathbin{\triangleleft} p \leftarrow e \mathbin{\triangleleft} p \leftarrow p$ and the $(c,d)$-bicomodule equations are guaranteed from the $(e,d)$-bicomodule equations as the map $c \leftarrow e$ is a comonoid homomorphism. The identity morphism on $p$ therefore provides a morphism of bicomodules as on the left in \eqref{eqn.cocartesian}. 
\begin{equation}\label{eqn.cocartesian}
\begin{tikzcd}
e \rar[bimr-biml,""{name=S, below}]{e} \dar & e \rar[bimr-biml,""{name=U, below}]{p} \dar & d \dar[equals] \\
c \rar[bimr-biml,""{name=T, above},swap]{e} & c \rar[bimr-biml,""{name=V, above},swap]{p} & d
\arrow[Rightarrow,shorten=4,from=S,to=T]
\arrow[Rightarrow,shorten=4,from=U,to=V]
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}
Note that both of these squares are cocartesian fillers (in the sense of equipments, see \cite[Lemma 2.3.13]{spivak2021functorial} and \cite{shulman2008framed}) of their respective vertical arrows and source horizontal arrows. This means that the cocartesian filler of the outer frame of the composite agrees with the square on the right, so by the universal property of cocartesian fillers the composite square induces a morphism of $(c,d)$-bicomodules from $p$ to $e \mathbin{\triangleleft}_c p$, providing the coaction of a left $e$-comodule structure on $e$ in $\mathbb{C}atsharp$. The comodule equations are then straightforward to deduce from the left $e$-comodule structure of $p$ in $\mathbf{C}at{Poly}$ and cofunctoriality of $e$ over $c$.
\mathbf{C}at{End}d{proof}

We can now proceed to prove \cref{nervecoalgebra}.

\begin{theorem}\label{thm.nerveproof}
For a monad $m$ on $c$ in $\mathbb{C}atsharp$, $A$ a $(c,b)$-bicomodule with the structure of a left $m$-module, and $p$ a $(d,c)$-bicomodule, $p \mathbin{\triangleleft}_c A$ is a left $\lens{p}{p \mathbin{\triangleleft}_c m}$-comodule with coaction as in \eqref{eqn.nerve} (also pictured below). When $d=0$ $A$ therefore has the structure of a $\Theta_m^p$-presheaf, which when $p=m$ agrees with the nerve given by Weber in \cite[Definition 4.4]{weber2007familial}.
\mathbf{C}at{End}d{theorem}

\[
\begin{tikzcd}
d \ar[bimr-biml,""{name=S, below}]{rrr}{p} \ar[bimr-biml]{dr}[swap]{\lens{p}{p \mathbin{\triangleleft}_c m}} & & & c \rar[bimr-biml]{A} \dar[Rightarrow,shorten >=9,shorten <=3] & b \\
& d \rar[bimr-biml,""{name=T, above},swap]{p} & c \ar[bimr-biml]{ur}[description]{m} \ar[bimr-biml,bend right=20]{urr}[swap]{A} & {}
\arrow[Rightarrow,shorten=4,from=S,to=T]
\mathbf{C}at{End}d{tikzcd}
\]

\begin{proof}
Let a $(c,b)$-bicomodule $A$ have an $m$-action morphism $\psi \colon m \mathbin{\triangleleft}_c A \to A$, and consider the coaction morphism $p \mathbin{\triangleleft}_c A \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c A$ of $(d,0)$-bicomodules from \eqref{eqn.nerve}.

We first show that $p \mathbin{\triangleleft}_c A$ is a comodule, namely that the coaction commutes with counit and comultiplication. To do so, we use the universal property of the coclosure, namely that the composition of the coaction with a morphism $\phi \colon \lens{p}{p \mathbin{\triangleleft}_c m} \to q$ agrees with the composite map 
\[
p \mathbin{\triangleleft}_c A \To{\overline \phi \mathbin{\triangleleft}_c A} q \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c A  \To{q \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c \psi} q \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c A,
\]
where $\overline \phi$ is the map $p \to q \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$ corresponding to $\phi$ under the adjunction $\lens{-}{p \mathbin{\triangleleft}_c m} \dashv - \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$.

For the counit, the composite $p \mathbin{\triangleleft}_c A \to p \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c A \to p \mathbin{\triangleleft}_c A$ of the unit of $m$ with the $m$-action map of $A$ is the identity by the unit law for $m$-modules, so the composite of the coaction with the counit of $\lens{p}{p \mathbin{\triangleleft}_c m}$ as defined in \cref{thetacomonoid} is the identity as desired.

For the comultiplication, the composite
\[
p \mathbin{\triangleleft}_c A \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c \left(m \mathbin{\triangleleft}_c m\right) \mathbin{\triangleleft}_c A
\]
\[
\To{\cdots \mathbin{\triangleleft}_c \mu \mathbin{\triangleleft}_c A} \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c A \To{\cdots \mathbin{\triangleleft}_c \psi} \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c A
\]
agrees with the composite 
\[
p \mathbin{\triangleleft}_c A \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c \left(m \mathbin{\triangleleft}_c A\right)
\]
\[
\To{\cdots \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c \psi} \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m \mathbin{\triangleleft}_c A \To{\cdots \mathbin{\triangleleft}_c \psi} \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c A
\]
by the multiplication law for $m$-modules, so the composite of the coaction with the comultiplication of $\lens{p}{p \mathbin{\triangleleft}_c m}$ agrees with the repeated application of the coaction as desired.

It remains to show that when $p=m$ this $\Theta_m$-presheaf agrees with Weber's nerve of \cite[Definition 4.4]{weber2007familial}. In fact we show that for general $p$ the copresheaf $p \mathbin{\triangleleft}_c A$ has $I$-cells given by maps $m \mathbin{\triangleleft}_c p[I] \to A$ of $m$-algebras and for a morphism $f \colon m \mathbin{\triangleleft}_c p[I'] \to m \mathbin{\triangleleft}_c p[I]$ of $m$-algebras, the corresponding function from $I$-cells to $I'$-cells is given by precomposition with $f$. 

Observe that on positions, the unit morphism $p \to \lens{p}{p \mathbin{\triangleleft}_c m} \mathbin{\triangleleft}_d p \mathbin{\triangleleft}_c m$ sends $I \in p(1)$ to the tuple
\[
\left(I \in p(1), (I' \in p(1))_{f \colon p[I'] \to m \mathbin{\triangleleft}_c p[I]}, \pi \circ f \colon p[I'] \to m \mathbin{\triangleleft}_c p[I] \to m(1) \right),
\]
where $f$ is a morphism of $c$-copresheaves, and on directions sends 
\[
(I',x \in p[I'], y \in m[\pi \circ f(x)])
\]
to $f(x,y)$. The coaction thus sends the pair $(I, p[I] \to A)$ to 
\[
(I, (I')_f, (p[I'] \to m \mathbin{\triangleleft}_c p[I] \to m \mathbin{\triangleleft}_c A \to A)_{f}).
\]
As a $\lens{p}{p \mathbin{\triangleleft}_c m}$-copresheaf then its $I$-cells are the maps $p[I] \to A$ of $c$-copresheaves, equivalently maps $m \mathbin{\triangleleft}_c p[I] \to A$ of $m$-algebras, and the application of a morphism $p[I'] \to m \mathbin{\triangleleft}_c p[I]$ to $p[I] \to A$ is the Kleisli composite, equivalently the composite of maps 
\[
m \mathbin{\triangleleft}_c p[I'] \to m \mathbin{\triangleleft}_c p[I] \to A
\]
of $m$-algebras as desired.
\mathbf{C}at{End}d{proof}

\chapter{Functoriality of ${\mathbb{O}\mathbf{C}at{rg}} \to \mathbb{E}\mathbf{C}at{ff}\to\mathbb{C}atsharp$}

We first make explicit the requisite commutative diagrams from \cref{def.eff}:
\begin{equation}\label{eqn.eff}
\begin{tikzcd}
	c\mathbin{\triangleleft} s\ar[d, "\epsilon_c\mathbin{\triangleleft} s"']&
	s\mathbin{\triangleleft} d\ar[d, "s\mathbin{\triangleleft}\epsilon_d"]\ar[l, "\varphi"']\\
	s\ar[r, equal]&
	s
\mathbf{C}at{End}d{tikzcd}
\hspace{.6in}
\begin{tikzcd}
	c\mathbin{\triangleleft} s\ar[d, "\delta_c\mathbin{\triangleleft} s"']&&
	s\mathbin{\triangleleft} d\ar[d, "s\mathbin{\triangleleft}\delta_d"]\ar[ll, "\varphi"']\\
	c\mathbin{\triangleleft} c\mathbin{\triangleleft} s&
	c\mathbin{\triangleleft} s\mathbin{\triangleleft} d\ar[l, "c\mathbin{\triangleleft}\varphi"]&
	s\mathbin{\triangleleft} d\mathbin{\triangleleft} d\ar[l, "\varphi\mathbin{\triangleleft} d"]
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}

\begin{proposition}\label{prop.cofree}
There is a functor $\cofree -\colon\mathbf{C}at{Poly}\to\mathbf{C}at{Poly}$ such that $\cofree p$ has the structure of a $\mathbin{\triangleleft}$-comonoid for each $p:\mathbf{C}at{Poly}$,
\[
\cofree p\to\mathcal{y}
\mathbb{Q}and
\cofree p\to\cofree p\mathbin{\triangleleft}\cofree p.
\qedhere
\]
\mathbf{C}at{End}d{proposition}
\begin{proof}
Given a polynomial $p$, define polynomials $p^{(i)}$ for $i\in\mathbb{N}$ by
\[
  p\coh{0}\coloneqq\mathcal{y}
  \mathbb{Q}and
  p\coh{1+i}\coloneqq\mathcal{y}\times\left(p\mathbin{\triangleleft} p\coh{i}\right)
\]
There is a projection map $\pi\coh{0}\colon p\coh{1}\to p\coh{0}$, and if $\pi\coh{i}\colon p\coh{1+i}\to p\coh{i}$ has been defined, then we can define $\pi\coh{1+i}\coloneqq \mathcal{y}\times(p\mathbin{\triangleleft}\pi\coh{i})$. Now define the polynomial
\begin{equation}\label{eqn.construct_cofree}
\cofree p\coloneqq\lim\big(\cdots\To{\pi\coh{2}}p\coh{2}\To{\pi\coh{1}}p\coh{1}\To{\pi\coh{0}}p\coh{0}\big)
\mathbf{C}at{End}d{equation}
and we note that this construction $p\mapsto \cofree p$ is natural in $p:\mathbf{C}at{Poly}$.

This polynomial comes equipped with a counit $\epsilon\colon\cofree p\to\mathcal{y}=p\coh{0}$ given by the projection. We next construct the comultiplication $\delta\colon\cofree p\to\cofree p\mathbin{\triangleleft}\cofree p$. Since $\mathbin{\triangleleft}$ commutes with connected limits, we have
\[
  \cofree p\mathbin{\triangleleft}\cofree p=
  \left(\lim_{i_1}p\coh{i_1}\right)\mathbin{\triangleleft}\left(\lim_{i_2}p\coh{i_2}\right)\cong
  \lim_{i_1,i_2}\left(p\coh{i_1}\mathbin{\triangleleft} p\coh{i_2}\right)
\]
To obtain the comultiplication $\lim_ip\coh{i}\to\lim_{i_1,i_2}(p\coh{i_1}\mathbin{\triangleleft} p\coh{i_2})$, it suffices to produce a natural choice of polynomial map $\varphi_{i_1,i_2}\colon p\coh{i_1+i_2}\to p\coh{i_1}\mathbin{\triangleleft} p\coh{i_2}$ for any $i_1,i_2:\mathbb{N}$. When $i_1=0$ or $i_2=0$, we use the unit identity for $\mathbin{\triangleleft}$. By induction, assume given $\varphi_{i_1,1+i_2}$; we construct $\varphi_{1+i_1,1+i_2}$ as follows:
\begin{align}
\nonumber
  p\coh{1+i_1+1+i_2}&=
  \mathcal{y}\times \left(p\mathbin{\triangleleft} p\coh{i_1+1+i_2}\right)\\&\to
\label{eqn.induction}
  \mathcal{y}\times \left(p\mathbin{\triangleleft} p\coh{i_1}\mathbin{\triangleleft} p\coh{1+i_2}\right)\\&\to
\label{eqn.special}
  \left(\mathcal{y}\times p\mathbin{\triangleleft} p\coh{i_1}\right)\mathbin{\triangleleft} p\coh{1+i_2}\\&=
\nonumber
  p\coh{1+i_1}\mathbin{\triangleleft} p\coh{1+i_2}
\mathbf{C}at{End}d{align}
where \eqref{eqn.induction} is $\varphi_{i_1,1+i_2}$ and it remains to construct \eqref{eqn.special}. Recall that $-\mathbin{\triangleleft} q$ preserves products for any $q$, so constructing \eqref{eqn.special} is equivalent to constructing two maps
\[
\mathcal{y}\times \left(p\mathbin{\triangleleft} p\coh{i_1}\mathbin{\triangleleft} p\coh{1+i_2}\right)\To{\phi\coh{i_1,i_2}} p\coh{1+i_2}
\mathbb{Q}and
\mathcal{y}\times \left(p\mathbin{\triangleleft} p\coh{i_1}\mathbin{\triangleleft} p\coh{1+i_2}\right)\to p\mathbin{\triangleleft} p\coh{i_1}\mathbin{\triangleleft} p\coh{1+i_2}.
\]
For the latter we use the second projection. The former, $\phi\coh{i_1,i_2}\colon p\coh{1+i_1+1+i_2}\to p\coh{1+i_2}$, is the more interesting one; for it we also use projections $p\coh{i_1}\to p\coh{0}=\mathcal{y}$ and $\pi\coh{i_2}\colon p\coh{i_2+1}\to p\coh{i_2}$ to obtain:
\[
\mathcal{y}\times \left(p\mathbin{\triangleleft} p\coh{i_1}\mathbin{\triangleleft} p\coh{1+i_2}\right)\to
\mathcal{y}\times \left(p\mathbin{\triangleleft}\mathcal{y}\mathbin{\triangleleft} p\coh{i_2}\right)\cong p\coh{1+i_2}
\]
We leave the naturality of this to the reader.

It remains to check that $\epsilon$ and $\delta$ satisfy unitality and coassociativity. The base cases above imply unitality. Proving coassociativity amounts to proving that the following diagram commutes:
\[
\begin{tikzcd}[column sep=50pt]
	p\coh{1+i_1+1+i_2+1+i_3}\ar[r, "\phi\coh{i_1,i_2+1+i_3}"]\ar[d, "\phi\coh{i_1+1+i_2,i_3}"']&
	p\coh{1+i_2+1+i_3}\ar[d, "\phi\coh{i_2,i_3}"]\\
	p\coh{1+i_3}\ar[r,equal]&p\coh{1+i_3}
\mathbf{C}at{End}d{tikzcd}
\]
This can be shown by induction on $i_3$.
\mathbf{C}at{End}d{proof}

\begin{theorem}\label{thm.cofree_comonad_comonad}
There is an adjunction
\[
\adj{\mathbf{C}at{Cat}^{\sharp}}{U}{\cofree{-}}{\mathbf{C}at{Poly}}
\]
where $U\colon\mathbf{C}at{Cat}^{\sharp}\to\mathbf{C}at{Poly}$ is the forgetful functor $U(c,\epsilon,\delta)\coloneqq c$.
\mathbf{C}at{End}d{theorem}
\begin{proof}
We will abuse notation and denote the comonoid $(c,\epsilon,\delta):\mathbf{C}at{Cat}^{\sharp}$ simply by its carrier $c$. We first provide the counit and unit of the desired adjunction. The counit
\[
\epsilon_p\colon\cofree{p}\to p
\]
is given by composing the projection map $\cofree{p}\to p\coh{1}$ from construction \eqref{eqn.construct_cofree} with the projection $p\coh{1}\cong\mathcal{y}\times p\to p$. Since $\cofree{c}$ is defined as a limit, the unit
\[
\eta_c\colon c\nrightarrow\cofree{c}
\]
will be given by defining maps $\eta\coh{i}\colon c\to c\coh{i}$ commuting with the projections $\pi\coh{i}\colon c\coh{1+i}\to c\coh{i}$, for each $i:\mathbb{N}$, and then showing that the resulting polynomial map $\eta_c$ is indeed a cofunctor. Noting that $c\coh{0}=\mathcal{y}$, we define
\[
\eta\coh{0}\coloneqq\epsilon
\]
Given $\eta\coh{i}\colon c\to c\coh{i}$, we define $\eta\coh{1+i}$ as the composite
\[
c\To{(\epsilon,\delta)}\mathcal{y}\times(c\mathbin{\triangleleft} c)\To{\mathcal{y}\times(c\mathbin{\triangleleft}\eta\coh{i})}\mathcal{y}\times\left(c\mathbin{\triangleleft} c\coh{i}\right)=c\coh{1+i}.
\]
Clearly, we have $\eta\coh{0}=\pi\coh{0}\circ\eta\coh{1}$. It is easy to check that if $\eta\coh{i}=\pi\coh{i}\circ\eta\coh{1+i}$ then $\eta\coh{1+i}=\pi\coh{1+i}\circ\eta\coh{2+i}$. Thus we have constructed a polynomial map $\eta\colon c\to \cofree{c}$. It clearly commutes with the counit, so it suffices to show that $\eta$ commutes with the comultiplication, which amounts to showing that the following diagram commutes
\[
\begin{tikzcd}
  c\ar[r, "\delta"]\ar[d, "{(\epsilon,\delta)}"']&[27pt]
  c\mathbin{\triangleleft} c\ar[r, "{(\epsilon,\delta)\mathbin{\triangleleft}(\epsilon,\delta)}"]&[15pt]
  \big(\mathcal{y}\times(c\mathbin{\triangleleft} c)\big)\mathbin{\triangleleft}\big(\mathcal{y}\times(c\mathbin{\triangleleft} c)\big)\ar[d, "{(\mathcal{y}\times c\mathbin{\triangleleft}\eta\coh{i_1})\mathbin{\triangleleft}(\mathcal{y}\times c\mathbin{\triangleleft}\eta\coh{i_2})}"]\\
  \mathcal{y}\times(c\mathbin{\triangleleft} c)\ar[r, "{\mathcal{y}\times c\mathbin{\triangleleft}\eta\coh{i_1+1+i_2}}"']&
  \mathcal{y}\times(c\mathbin{\triangleleft} c\coh{i_1+1+i_2})\ar[r, "\varphi_{1+i_1,1+i_2}"']&
  \big(\mathcal{y}\times(c\mathbin{\triangleleft} c\coh{i_1})\big)\mathbin{\triangleleft}\big(\mathcal{y}\times(c\mathbin{\triangleleft} c\coh{i_2})\big)
\mathbf{C}at{End}d{tikzcd}
\]
for all $i_1,i_2:\mathbb{N}$, where $\varphi_{1+i_1,1+i_2}$ is the map constructed in \cref{eqn.induction,eqn.special}. Commutativity follows from the counitality and coassociativity of the comonoid $c$.

The triangle identities are straightforward as well. Indeed, for any comonoid $c:\mathbf{C}at{Cat}^{\sharp}$, the composite $c\To{U\circ\eta_c} \cofree{c}\To{\epsilon_{Uc}} c$ is equal to the composite of $c\To{(\epsilon,c)}c\coh{1}=\mathcal{y}\times c$, with the projection $c\coh{1}\to c$, the result of which is the identity. Finally, for any polynomial $p:\mathbf{C}at{Poly}$, the composite $\cofree{p}\To{\eta_{\cofree{p}}}\cofree{\cofree{p}}\To{\cofree{\epsilon_p}}\cofree{p}$ is given by taking a limit of maps of the form
\[
	\cofree{p}\To{(\epsilon,\delta)}
	\mathcal{y}\times(\cofree{p}\mathbin{\triangleleft}\cofree{p})\To{\mathcal{y}\times(\cofree{p}\mathbin{\triangleleft}\eta\coh{i})}
	\mathcal{y}\times(\cofree{p}\mathbin{\triangleleft}\cofree{p}\coh{i})\To{\mathcal{y}\times(\epsilon_p\mathbin{\triangleleft}\epsilon_p\coh{i})}
	\mathcal{y}\times(p\mathbin{\triangleleft} p\coh{i})
\]
Each one is in fact the projection $\cofree{p}\to p\coh{i+1}$, so the resulting map is the identity on $\cofree{p}$, completing the proof.
\mathbf{C}at{End}d{proof}

\begin{lemma}\label{lemma.eff_handler_to_cofree}
For a polynomial $p:\mathbf{C}at{Poly}$ and comonoid $(c,\epsilon,\delta)$, we can identify $(\cofree p,c)$-effects handlers with elementary $(p,c)$-effects handlers.
\mathbf{C}at{End}d{lemma}
\begin{proof}
Given a $(\cofree p,c)$-effects handler $\cofree p\mathbin{\triangleleft} s\leftarrow s\mathbin{\triangleleft} c$, one composes with the projection $\cofree p\to p$ to obtain an elementary $(p,c)$-effects handler. 

Going the other way, suppose given an elementary effects handler $p\mathbin{\triangleleft} s{\cat{F}}rom{\varphi}s\mathbin{\triangleleft} c$. Recall from \eqref{eqn.construct_cofree} that $\cofree p$ is constructed as a limit, and that $(-\mathbin{\triangleleft} s)$ preserves all limits; hence we have
\[\cofree p\mathbin{\triangleleft} s\cong\lim_i(p\coh{i}\mathbin{\triangleleft} s).\]
We construct a map $\cofree p\mathbin{\triangleleft} s{\cat{F}}rom{{\Cat{P}}hi} s\mathbin{\triangleleft} c$ by induction on $i:\mathbb{N}$. 

When $i=0$, we have $p\coh{0}\mathbin{\triangleleft} s\cong s{\cat{F}}rom{{\Cat{P}}hi\coh{0}}s\mathbin{\triangleleft} c$ given by ${\Cat{P}}hi\coh{0}\coloneqq s\mathbin{\triangleleft}\epsilon$. Suppose given $p\coh{i}\mathbin{\triangleleft} s{\cat{F}}rom{{\Cat{P}}hi\coh{i}}s\mathbin{\triangleleft} c$ for some $i:\mathbb{N}$. We obtain
\begin{equation}\label{eqn.get_full_eff}
\begin{aligned}
	s\mathbin{\triangleleft} c\To{\,(s\mathbin{\triangleleft}\delta,s\mathbin{\triangleleft}\epsilon)\,}&
	(s\mathbin{\triangleleft} c\mathbin{\triangleleft} c)\times s\\\To{\;\,(\varphi\mathbin{\triangleleft} c)\times s\;\,}&
	(p\mathbin{\triangleleft} s\mathbin{\triangleleft} c)\times s\\\To{(p\mathbin{\triangleleft} {\Cat{P}}hi\coh{i})\times s}&
	(p\mathbin{\triangleleft} p\coh{i}\mathbin{\triangleleft} s)\times s\\\To{\hspace{5.3mm}\cong\hspace{5.3mm}}&
	((p\mathbin{\triangleleft} p\coh{i})\times\mathcal{y})\mathbin{\triangleleft} s\\\To{\hspace{5.3mm}\cong\hspace{5.3mm}}&
	p\coh{i+1}\mathbin{\triangleleft} s
\mathbf{C}at{End}d{aligned}
\mathbf{C}at{End}d{equation}
We have now constructed ${\Cat{P}}hi$, and one easily observes that its underlying elementary effects handler is again $\varphi$. To conclude, one must check that ${\Cat{P}}hi$ satisfies the two equations from \eqref{eqn.eff} and that the round trip on $(\cofree p,c)$-effects handlers is the identity.

The counit equation from \eqref{eqn.eff} is clear: it follows from the use of $\varphi$ with $i=0$ in the second arrow of \eqref{eqn.get_full_eff}. The comultiplication equation from \eqref{eqn.eff} amounts to checking that two maps of the form $s\mathbin{\triangleleft} c\rightrightarrows\lim_{i_1,i_2}p\coh{i_1}\mathbin{\triangleleft} p\coh{i_2}\mathbin{\triangleleft} s$ agree, and this is straightforward. 

Finally, suppose given an effects handler $\cofree p\mathbin{\triangleleft} s{\cat{F}}rom{{\Cat{P}}si}s\mathbin{\triangleleft} c$. Let $\varphi\coloneqq(\pi\mathbin{\triangleleft} s)\circ{\Cat{P}}si$ be the underlying elementary effects handler, where $\pi\colon\cofree p\to p$ is the projection, and construct ${\Cat{P}}hi$ from $\varphi$ as above; we want to show that ${\Cat{P}}hi={\Cat{P}}si$. For each $i:\mathbb{N}$, let ${\Cat{P}}si\coh{i}\colon s\mathbin{\triangleleft} c\to p\coh{i}\mathbin{\triangleleft} s$ be the composite of ${\Cat{P}}si$ with the projection $\cofree p\to p\coh{i}$; it suffices to show that  ${\Cat{P}}hi\coh{i}={\Cat{P}}si\coh{i}$. This follows from \eqref{eqn.eff} and induction on $i$.
\mathbf{C}at{End}d{proof}

\begin{proposition}\label{prop.elem_as_eff}
For $p,q:\mathbf{C}at{Poly}$, any elementary $(p,q)$-effects handler gives rise to a $(\cofree p,\cofree q)$-effects handler.
\mathbf{C}at{End}d{proposition}
\begin{proof}
Given a $(p,q)$-effects handler $p\mathbin{\triangleleft} s{\cat{F}}rom{\varphi}s\mathbin{\triangleleft} q$, we compose with the projection $s\mathbin{\triangleleft} q\leftarrow s\mathbin{\triangleleft}\cofree q$ to obtain an elementary $(p,\cofree q)$-effects handler. Then by \cref{lemma.eff_handler_to_cofree}, we can identify it with a $(\cofree p,\cofree q)$-effects handler, completing the proof.
\mathbf{C}at{End}d{proof}

\begin{theorem}\label{thm.eff}[See \cref{thm.eff_statement}]
\mathbb{E}\mathbf{C}at{ff}body
\mathbf{C}at{End}d{theorem}
\begin{proof}
We first show that for any $(c,d)$-effects handler $(s,\varphi)$, the structure maps from \eqref{eqn.bicomod_for_eff} do in fact form a bicomodule $c\bifrom[s\mathbin{\triangleleft} d]d$. It is easy to check that $s\mathbin{\triangleleft} d\To{s\mathbin{\triangleleft}\delta}s\mathbin{\triangleleft} d\mathbin{\triangleleft} d$ is a right comodule. To check that the left structure maps commutes with counit, we have the following
\[
\begin{tikzcd}
	s\mathbin{\triangleleft} d\ar[r, "s\mathbin{\triangleleft}\delta"]\ar[dr, equal]&
	s\mathbin{\triangleleft} d\mathbin{\triangleleft} d\ar[r, "\varphi\mathbin{\triangleleft} d"]\ar[d, "s\mathbin{\triangleleft}\epsilon\mathbin{\triangleleft} d"]&
	c\mathbin{\triangleleft} s\mathbin{\triangleleft} d\ar[d, "\epsilon\mathbin{\triangleleft} s\mathbin{\triangleleft} d"]\\&
	s\mathbin{\triangleleft} d\ar[r, equal]&
	s\mathbin{\triangleleft} d
\mathbf{C}at{End}d{tikzcd}
\]
where the triangle commutes because $d$ is a comonad, and the square commutes by \eqref{eqn.eff}. Checking that the left structure commutes with comultiplication is similar, and the compatibility between left and right structures is even easier.

A square in the double category $\mathbb{E}\mathbf{C}at{ff}$ is a map $\gamma\colon s\to s'$ and a commuting square
\[
\begin{tikzcd}
	c\mathbin{\triangleleft} s\ar[d, "\alpha\mathbin{\triangleleft}\gamma"']& 
	s\mathbin{\triangleleft} d\ar[d, "\gamma\mathbin{\triangleleft}\beta"]\ar[l, "\varphi"']\\
	c'\mathbin{\triangleleft} s'&
	s'\mathbin{\triangleleft} d'\ar[l, "\varphi'"]
\mathbf{C}at{End}d{tikzcd}
\]
for cofunctors (comonoid homomorphisms) $\alpha\colon c\to c'$ and $\beta\colon d\to d'$. This gives rise to a square in $\mathbb{C}atsharp$:
\[
\begin{tikzcd}
	c\ar[d, "\alpha"']\ar[r, bimr-biml, "s\mathbin{\triangleleft} d", ""' name=sd]&
	d\ar[d, "\beta"]\\
	c'\ar[r, bimr-biml, "s'\mathbin{\triangleleft} d'"', "" name=s'd']&
	d'\ar[from=sd, to=s'd', shorten=2mm, Rightarrow]
\mathbf{C}at{End}d{tikzcd}
\]
Indeed, squares of this form are in bijection with $(c',d')$-bicomodule maps $s\mathbin{\triangleleft} d\to s'\mathbin{\triangleleft} d'$, and we obtain one from $\gamma$ as follows:
\[
\begin{tikzcd}
	c\mathbin{\triangleleft} s\mathbin{\triangleleft} d\ar[d]&
	s\mathbin{\triangleleft} d\mathbin{\triangleleft} d\ar[d]\ar[l]&
	s\mathbin{\triangleleft} d\ar[d]\ar[l]\ar[r]&
	s\mathbin{\triangleleft} d\mathbin{\triangleleft} d\ar[d]\\
	c'\mathbin{\triangleleft} s'\mathbin{\triangleleft} d'&
	s'\mathbin{\triangleleft} d'\mathbin{\triangleleft} d'\ar[l]&
	s'\mathbin{\triangleleft} d'\ar[l]\ar[r]&
	s'\mathbin{\triangleleft} d'\mathbin{\triangleleft} d'
\mathbf{C}at{End}d{tikzcd}
\]
To see that this map is faithful for $d\neq 0$, suppose given maps $\gamma_1,\gamma_2\colon s\to s'$ which induce the same map $(\gamma_1\mathbin{\triangleleft}\beta)=(\gamma_2\mathbin{\triangleleft}\beta)\colon s\mathbin{\triangleleft} d\to s'\mathbin{\triangleleft} d'$. Then both squares below commute
\[
\begin{tikzcd}
	s\mathbin{\triangleleft} d\ar[r, "s\mathbin{\triangleleft}\epsilon"]\ar[d]&
	s\ar[d, shift right, "\gamma_1"']\ar[d, shift left, "\gamma_2"]\\
	s'\mathbin{\triangleleft} d'\ar[r, "s'\mathbin{\triangleleft}\epsilon"']&
	s'
\mathbf{C}at{End}d{tikzcd}
\]
so it suffices to show that $s\mathbin{\triangleleft}\epsilon$ is an epimorphism. The operation $s\mathbin{\triangleleft}-$ preserves epimorphisms, and $p\to\mathcal{y}$ is an epimorphism for any polynomial $p\neq 0$.

The identity effects handler on $c$ is $(\mathcal{y},c)$, which is sent to the identity bicomodule. We next check that horizontal composition is preserved by our functor. That is, we need to show that for any $c\mathbin{\triangleleft} s{\cat{F}}rom{\varphi} s\mathbin{\triangleleft} d$ and $d\mathbin{\triangleleft} t{\cat{F}}rom{\psi}t\mathbin{\triangleleft} e$, there is a natural isomorphism
\[
\begin{tikzcd}[row sep=13pt]
  c\ar[rr, bimr-biml, "s\mathbin{\triangleleft} t\mathbin{\triangleleft} e", ""' name=e]\ar[dr, bimr-biml, bend right=10pt, "s\mathbin{\triangleleft} d"']&&
  e\\&
  |[alias=x]|d\ar[ur, bimr-biml, bend right=10pt, "t\mathbin{\triangleleft} e"']
  \ar[from=e, to=x, shorten=1pt, Rightarrow, "\cong"]
\mathbf{C}at{End}d{tikzcd}
\]
The composite bicomodule is given by the following equalizer
\[
\begin{tikzcd}
  (s\mathbin{\triangleleft} d)\mathbin{\triangleleft}_d(t\mathbin{\triangleleft} e)\ar[r]&
  s\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\ar[rr, "s\mathbin{\triangleleft}\delta_d\mathbin{\triangleleft} t\mathbin{\triangleleft} e"]\ar[dr, "s\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} \delta_e"']&&
  s\mathbin{\triangleleft} d\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\\&&
  s\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[ur, "s\mathbin{\triangleleft} d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e"']
\mathbf{C}at{End}d{tikzcd}
\]
and it suffices to find a map $s\mathbin{\triangleleft} t\mathbin{\triangleleft} e\to s\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e$ that is also an equalizer of the right-hand triangle. Since $(s\mathbin{\triangleleft} -)$ preserves equalizers, it suffices to find a map $t\mathbin{\triangleleft} e\to d\mathbin{\triangleleft} t\mathbin{\triangleleft} e$ that is an equalizer of the two maps $d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\rightrightarrows d\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e$. We propose the following:
\begin{equation}\label{eqn.two_maps}
\begin{tikzcd}
	t\mathbin{\triangleleft} e\ar[r, "t\mathbin{\triangleleft} \delta_e"]&
	t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[r, "\varphi\mathbin{\triangleleft} e"]&
	d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\ar[rr, "\delta_d\mathbin{\triangleleft} t\mathbin{\triangleleft} e"]\ar[dr, "d\mathbin{\triangleleft} t\mathbin{\triangleleft} \delta_e"']&&
  d\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\\&&&
  d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[ur, "d\mathbin{\triangleleft}\varphi\mathbin{\triangleleft} e"']
\mathbf{C}at{End}d{tikzcd}
\mathbf{C}at{End}d{equation}
To prove the two required maps agree, consider the following diagram:
\[
\begin{tikzcd}[column sep=40pt]
	t\mathbin{\triangleleft} e\ar[r, "t\mathbin{\triangleleft}\delta_e"]&
	t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[r, shift left, "t\mathbin{\triangleleft} e\mathbin{\triangleleft}\delta_e"]\ar[r, shift right, "t\mathbin{\triangleleft} \delta_e\mathbin{\triangleleft} e"']\ar[d, "\varphi\mathbin{\triangleleft} e"']&
	t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[r, "\varphi\mathbin{\triangleleft} e\mathbin{\triangleleft} e"]&
	d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\mathbin{\triangleleft} e\ar[d, "d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e"]\\&
	d\mathbin{\triangleleft} t\mathbin{\triangleleft} e\ar[rr, "\delta_d\mathbin{\triangleleft} t\mathbin{\triangleleft} e"']\ar[urr, bend right=6pt, "d\mathbin{\triangleleft} t\mathbin{\triangleleft} \delta_e"]&&
	d\mathbin{\triangleleft} d\mathbin{\triangleleft} t\mathbin{\triangleleft} e
\mathbf{C}at{End}d{tikzcd}
\]
By \eqref{eqn.eff}, the inner rectangle commutes: $(\varphi\mathbin{\triangleleft} e)\mathbin{\fatsemi}(\delta_d\mathbin{\triangleleft} t\mathbin{\triangleleft} e)=(t\mathbin{\triangleleft} \delta_e\mathbin{\triangleleft} e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e\mathbin{\triangleleft} e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e)$. By associativity of $\delta_e$, the first map equalizes the parallel pair: $(t\mathbin{\triangleleft} \delta_e)\mathbin{\fatsemi}(t\mathbin{\triangleleft} e\mathbin{\triangleleft}\delta_e)=(t\mathbin{\triangleleft} \delta_e)\mathbin{\fatsemi}(t\mathbin{\triangleleft}\delta_e\mathbin{\triangleleft} e)$. And finally, we have $(t\mathbin{\triangleleft} e\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e\mathbin{\triangleleft} e)=(\varphi\mathbin{\triangleleft} e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} t\mathbin{\triangleleft}\delta_e)$. Together these give us the required equation:
\begin{align*}
	(t\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e)\mathbin{\fatsemi}(\delta_d\mathbin{\triangleleft} t\mathbin{\triangleleft} e)&=
	(t\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(t\mathbin{\triangleleft}\delta_e\mathbin{\triangleleft} e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e\mathbin{\triangleleft} e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e)\\&=
	(t\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(t\mathbin{\triangleleft} e\mathbin{\triangleleft} \delta_e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e\mathbin{\triangleleft} e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e)\\&=
	(t\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(\varphi\mathbin{\triangleleft} e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} t\mathbin{\triangleleft}\delta_e)\mathbin{\fatsemi}(d\mathbin{\triangleleft} \varphi\mathbin{\triangleleft} e)
\mathbf{C}at{End}d{align*}
Thus we have proved that the two maps from \eqref{eqn.two_maps} agree. To prove that $t\mathbin{\triangleleft} e$ is actually the equalizer, one can perform a lengthy but routine set-theoretic calculation on positions and directions; we leave this to the reader.

Finally, every bicomodule $c\bifrom[S]0$ gives rise to an effects handler, $c\mathbin{\triangleleft} S\leftarrow S=S\mathbin{\triangleleft} 0$. Similarly, every bicomodule $c\bifrom[s]\mathcal{y}$ gives rise to a an effects handler $c\mathbin{\triangleleft} s\leftarrow s=s\mathbin{\triangleleft}\mathcal{y}$. In both cases, the required commutativity \eqref{eqn.eff} follows from that of the bicomodules.
\mathbf{C}at{End}d{proof}

\begin{lemma}\label{lemma.dir_tri_lin_rep}
For any sets $S,T:\mathbf{C}at{Set}$ and polynomial $p:\mathbf{C}at{Poly}$, the maps
\[
	S\mathcal{y}\otimes p\To\cong S\mathcal{y}\mathbin{\triangleleft} p
  \mathbb{Q}and
	p\otimes\mathcal{y}^T\To\cong p\mathbin{\triangleleft}\mathcal{y}^T
\]
induced by the duoidal structure \eqref{eqn.duoidal} are isomorphisms.
\mathbf{C}at{End}d{lemma}
\begin{proof}
One checks that both maps are bijective on positions and directions.
\mathbf{C}at{End}d{proof}

\begin{lemma}\label{lemma.const_linear}
For any sets $S,T:\mathbf{C}at{Set}$ and polynomial $p$ there is a natural bijection between hom-sets
\[
\mathbf{C}at{Poly}(S\mathcal{y},p\mathbin{\triangleleft} T\mathcal{y})
\cong
\mathbf{C}at{Set}(S,p\mathbin{\triangleleft} T)
.
\]
\mathbf{C}at{End}d{lemma}
\begin{proof}
The functor $(S\mapsto S\mathcal{y}):\mathbf{C}at{Set}\to\mathbf{C}at{Poly}$ is left adjoint to $(-\mathbin{\triangleleft}  1) \colon\mathbf{C}at{Poly}\to\mathbf{C}at{Set}$.
\mathbf{C}at{End}d{proof}

\begin{lemma}\label{lemma.lin_rep_adj}
For a set $S:\mathbf{C}at{Set}$ and polynomials $p,q:\mathbf{C}at{Poly}$, there is a natural bijection between hom-sets
\[
\mathbf{C}at{Poly}(p,q\mathbin{\triangleleft} S\mathcal{y})
\cong
\mathbf{C}at{Poly}(p\mathbin{\triangleleft}\mathcal{y}^S,q)
.
\]
\mathbf{C}at{End}d{lemma}
\begin{proof}
For any $S$, the polynomial functor $S\mathcal{y}$ is left adjoint to $\mathcal{y}^S$, i.e.\ there is a unit $\mathcal{y}\to\mathcal{y}^S\mathbin{\triangleleft} S\mathcal{y}$ and a counit $S\mathcal{y}\mathbin{\triangleleft}\mathcal{y}^S\to\mathcal{y}$ satisfying the triangle equations. Given a map $p\to q\mathbin{\triangleleft} S\mathcal{y}$ one applies $(-\mathbin{\triangleleft}\mathcal{y}^S)$ to both sides and composes with the counit to obtain a map $p\mathbin{\triangleleft}\mathcal{y}^S\to q$, and given a map of the latter form, one applies $(-\mathbin{\triangleleft} S\mathcal{y})$ to both sides and precomposes with the unit to obtain a map $p\to q\mathbin{\triangleleft} S\mathcal{y}$. The round-trips are identities by the triangle equations.
\mathbf{C}at{End}d{proof}

\begin{theorem}[See \cref{thm.org_statement}]\label{thm.org}
{\mathbb{O}\mathbf{C}at{rg}}body
\mathbf{C}at{End}d{theorem}
\begin{proof}
The vertical categories of both ${\mathbb{O}\mathbf{C}at{rg}}$ and $\mathbb{E}\mathbf{C}at{ff}el$ are defined to be $\mathbf{C}at{Poly}$. A horizontal morphism in ${\mathbb{O}\mathbf{C}at{rg}}$ from $q$ to $p$ is a $[q,p]$-coalgebra; we want to show that these can be identified with linear elementary $(p,q)$-effects handlers. Define $\mathbb{E}\mathbf{C}at{ff}ellin(p,q)_S$ to be the category of linear elementary effects handlers with carrier $S\mathcal{y}$ and define $x\tn{-}\mathbf{C}at{Coalg}_S$ to be the category of $x$-coalgebras with carrier $S$. By \cref{lemma.dir_tri_lin_rep,lemma.const_linear,lemma.lin_rep_adj} and the adjunction $(-\otimes q)\dashv[q,-]$, we have the following isomorphisms, natural in $S$:
\begin{align*}
	[q,p]\tn{-}\mathbf{C}at{Coalg}_S&\cong
	\mathbf{C}at{Poly}(S,[q,p]\mathbin{\triangleleft} S)\\&\cong
	\mathbf{C}at{Poly}(S\mathcal{y},[q,p]\mathbin{\triangleleft} S\mathcal{y})\\&\cong
	\mathbf{C}at{Poly}(S\mathcal{y}\mathbin{\triangleleft}\mathcal{y}^S,[q,p])\\&\cong
	\mathbf{C}at{Poly}(S\mathcal{y}\otimes\mathcal{y}^S,[q,p])\\&\cong
	\mathbf{C}at{Poly}(S\mathcal{y}\otimes q\otimes\mathcal{y}^S,p)\\&\cong
	\mathbf{C}at{Poly}((S\mathcal{y}\otimes q)\mathbin{\triangleleft}\mathcal{y}^S,p)\\&\cong
	\mathbf{C}at{Poly}(S\mathcal{y}\mathbin{\triangleleft} q,p\mathbin{\triangleleft}\mathcal{y}^S)\\&\cong
	\mathbb{E}\mathbf{C}at{ff}ellin(p,q)_S
\mathbf{C}at{End}d{align*}
It is straightforward to check that horizontal composition is preserved.

Squares in ${\mathbb{O}\mathbf{C}at{rg}}$ of the form
\[
\begin{tikzcd}
	q\ar[r, slash, "S"]\ar[d, "\psi"']&
	p\ar[d, "\varphi"]\\
	q'\ar[r, slash, "S'"']&
	p'
\mathbf{C}at{End}d{tikzcd}
\]
consist of maps $f\colon S\to S'$ such that the following diagram commutes:
\[
\begin{tikzcd}[column sep=45pt]
	S\ar[r, "\vartheta"]\ar[d, "f"']&
	{[q,p]\mathbin{\triangleleft} S}\ar[r, "{[q,\varphi]\mathbin{\triangleleft} S}"]&
	{[q,p']\mathbin{\triangleleft} S}\ar[d, "{[q,p']\mathbin{\triangleleft} f}"]\\
	S'\ar[r, "\vartheta'"']&
	{[q',p']\mathbin{\triangleleft} S'}\ar[r, "{[\psi,p']\mathbin{\triangleleft} S'}"']&
	{[q,p']\mathbin{\triangleleft} S'}	
\mathbf{C}at{End}d{tikzcd}
\]
This condition is equivalent to that for squares in $\mathbb{E}\mathbf{C}at{ff}el$, which demand that the following diagram commutes:
\[
\begin{tikzcd}
  S\mathcal{y}\mathbin{\triangleleft} q\ar[r, "\vartheta"]\ar[d, "f\mathbin{\triangleleft}\psi"']&
  p\mathbin{\triangleleft} S\mathcal{y}\ar[d, "f\mathbin{\triangleleft} \varphi"]\\
  S'\mathcal{y}\mathbin{\triangleleft} q'\ar[r, "\vartheta'"']&
  p'\mathbin{\triangleleft} S'\mathcal{y}
\mathbf{C}at{End}d{tikzcd}
\]
Thus the squares agree, as do compositions of squares, completing the proof.
\mathbf{C}at{End}d{proof}

\mathbf{C}at{End}d{document}