We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials.
Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, skew multicategories, as well as ordinary cartesian and symmetric multicategories and monoidal categories, polycategories, and linearly distributive and $\ast$-autonomous categories.
To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine.
We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.

§ INTRODUCTION

When presenting logics and type theories, it is generally useful to separate the structural rules, such as exchange, weakening, contraction, identity, and cut, from the logical rules governing particular connectives.
This separation of concerns can be reflected in categorical semantics by starting with a kind of multicategory [29, 19, 30] or polycategory [42] encapsulating the structural rules, in which we can formulate universal properties of objects that correspond to the connectives.

A multicategory is like a category, but allows the domain of a morphism to be a finite list of objects; a polycategory allows both the domain and codomain to be such a list.
Such morphisms correspond respectively to intuitionistic sequents $A_1,\dots,A_m \vdash B$ and classical sequents $A_1,\dots,A_m \vdash B_1,\dots, B_n$.
One can then formulate universal properties for “tensor products” as representing objects for such morphisms, generalizing the classical characterization of the tensor product of vector spaces as a representing object for multilinear maps.

The choice of structural rules in a logic is reflected by an action on the morphisms of a multi- or polycategory that modifies the elements in the domain or codomain lists.
For instance, the exchange rule is reflected by an operation taking any morphism $(\Gamma,A,B,\Delta) \to C$ to a morphism $(\Gamma,B,A,\Delta) \to C$.
This leads to different kinds of multi- and polycategory, such as the following.

* Cartesian multicategories correspond to intuitionistic nonlinear logic, with all structural rules.
A cartesian multicategory with enough representing objects is equivalent to a cartesian monoidal category or a cartesian closed category.

* Symmetric multicategories correspond to intuitionistic multiplicative-additive linear logic, with exchange but no weakening or contraction.
A symmetric multicategory with enough representing objects is equivalent to a symmetric monoidal category, possibly closed.

* Symmetric polycategories correspond to classical multiplicative-additive linear logic.
A symmetric polycategory with enough representing objects is equivalent to a linearly distributive category or a $\ast$-autonomous category.

Multicategories and polycategories also have advantages from a purely category-theoretic standpoint.

can simplify coherence problems, since operations defined by universal properties generally do not require explicit coherence axioms.
They can also enable the unification of different-looking structures in a larger context; for instance, monoidal categories and closed categories can both be represented as multicategories [19, 33], and the Chu and Dialectica constructions are both instances of one polycategorical operation [41].

It seems, however, that no polycategorical structure exists in the literature to correspond to classical linear logic with exponentials.

Structured categories with exponential modalities have certainly been studied, such as adjunctions [7] and linearly distributive categories with storage [6].
And a multicategorical version, corresponding to intuitionistic linear logic with exponentials, is suggested in [24].
But the polycategorical case appears to be missing.

In this paper we fill this gap by defining LNL polycategories.
An polycategory has two classes of objects, called linear and nonlinear.
The linear objects form a symmetric polycategory, while the nonlinear objects form a cartesian multicategory, and there are additional morphisms relating the two classes of objects, enabling a description of the modalities $\oc$ and $\wn$ by universal properties.
This can be regarded as a semantic counterpart of split-context presentations of linear logic, such as [7, 4, 46] in the intuitionistic case and [17] in the classical one.

Like their syntactic counterpart of full classical linear logic, polycategories are an extremely rich structure.
In addition to adjunctions and linearly distributive categories with storage, they include cartesian multicategories (if all objects are nonlinear), symmetric polycategories (if all objects are linear), symmetric multicategories (if all objects are linear and all codomains are unary), and CBPV structures (if all linear codomains are unary and all linear domains are subunary).
Thus, any structured category that can be represented by any of these multi- or polycategorical notions can also be regarded as an polycategory.

This suggests that polycategories should provide a unifying context to compare different kinds of structured category, and to study the correspondence between logic and category.
To facilitate this, we define a notion of LNL doctrine , whose “algebras” (which we call -categories) are polycategories satisfying certain object and arity restrictions and in which objects having certain universal properties exist.
Inspired by [20, 32, 10], we express these universal properties fibrationally: an doctrine is an polycategory $\abs{\dD}$ equipped with a collection of distinguished “cones”, and a -category is an polycategory equipped with a functor $\cP \to \abs{\dD}$ admitting a “cartesian” lift for each distinguished cone.
We also incorporate a “well-sortedness” condition that allows a restriction to Kleisli adjunctions if desired.
In this way, we can represent all of the following kinds of structured category, and many more, as the algebras for doctrines:

* Cartesian multicategories, symmetric multicategories, symmetric polycategories, multicategories, and skew multicategories.

* Symmetric monoidal categories, closed symmetric monoidal categories, and symmetric closed categories.

* Cartesian monoidal categories and cartesian closed categories.

* Cartesian monoidal categories with a commutative strong monad.

* Symmetric monoidal categories with a strong monad.

* CBPV adjunction models, EEC+ models, and ECBV models.

* Linearly distributive categories and $\ast$-autonomous categories.

* adjunctions, possibly closed or $\ast$-autonomous.

* Symmetric monoidal categories with a linear exponential comonad, linearly distributive categories with storage, and $\ast$-autonomous categories with storage.

* Any of the above with any specified family of limits and/or colimits.

We also argue that doctrines provide a unifying context to study substructural logics, and to compare the corresponding kinds of monoidal category.
Specifically, we will use a well-known iterative category-theoretic construction, known as the small object argument, to present the free -category $\sdhat$ generated by an input datum that we call a -sketch.
This has the following two consequences.

Firstly, from this construction we can extract a syntactic sequent calculus that also presents free -categories.
The iterative small object argument corresponds naturally to the inductive definition of sequent calculus derivations.
The structural rules arise since each stage is an polycategory, while the logical rules are inserted by iterative pushouts that enforce the existence of objects with universal properties.
Thus, there is a precise correspondence between the syntactic and semantic versions of the separation of concerns between structural and logical rules.

Secondly, we use the free -category on a sketch to show that any morphism of doctrines $\F:\dD_1\to\dD_2$ induces a pseudo 2-adjunction between $\dD_1$-categories and $\dD_2$-categories.
That is, any $\dD_2$-category $\cT$ has an underlying $\dD_1$-category $\radj{\Fhat}\cT$, and any $\dD_1$-category generates a free $\dD_2$-category $\ladj{\Fhat}\cS$.
Thus, doctrines also supply a uniform way to relate different sorts of monoidal category, potentially with exponential monads and comonads.

§.§ Acknowledgments

I would like to thank Robin Cockett, Max New, Paul Blain Levy, Noam Zeilberger, Christine Tasson, and Martin Hyland for helpful conversations and comments, and Nicolas Blanco for a careful reading and very helpful suggestions.

§ POLYCATEGORIES

The different kinds of multicategories mentioned in <ref>, corresponding to logics with different structural rules, are all instances of a well-developed theory of “generalized multicategories” parametrized by a monad on a bicategory or double category of spans or profunctors.[See [14] for a general framework, building on much prior work cited therein.]

This theory was used for instance in [24] to begin defining an analogue of polycategories for intuitionistic linear logic (see our discussion of “multicategories” below).

polycategories ought to be an instance of a similar theory of “generalized polycategories”,
but unfortunately, no such general theory has been formulated yet (though [16] provides strong evidence for its existence).

Thus, in this paper we simply give the definitions explicitly.

A linear-nonlinear () polycategory consists of:

* A set of nonlinear objects, which we denote by letters near the end of the Roman alphabet such as $X,Y,Z$.
We denote finite lists of nonlinear objects by the Greek letters $\Theta,\Upsilon$.
If $(X_1,\dots, X_m)$ is such a list and $\si : \{1,\dots,n\} \to \{1,\dots,m\}$ is a function, we write $\si : (X_1,\dots, X_m)\to (X_{\si 1},\dots, X_{\si n})$ and call it a structural map.

* For each $\Theta,X$, a nonlinear hom-set $\Pnl(\Theta;X)$ containing nonlinear morphisms,
with a functorial action by any structural map $\si : \Theta \to \Upsilon$:

\[\act{}{-}{\si} : \Pnl(\Upsilon;X) \to \Pnl(\Theta;X). \]

* Compositions and identities for the nonlinear hom-sets

\[ \circ_X : \Pnl(\Theta_1,X,\Theta_2;Y) \times \Pnl(\Upsilon;X) \to \Pnl(\Theta_1,\Upsilon,\Theta_2;Y)
\qquad 1_X \in \Pnl(X;X)\]

satisfying the multicategory axioms and equivariant for the structural actions.

* A set of linear objects, which we denote by letters near the beginning of the Roman alphabet such as $A,B,C$.
We denote finite lists of linear objects by the Greek letters $\Gamma,\Delta$.
If $(A_1,\dots, A_n)$ is such a list and $\tau : \{1,\dots,n\} \toiso \{1,\dots,n\}$ is a permutation, we write $\tau : (A_1,\dots, A_n)\toiso (A_{\si 1},\dots, A_{\si n})$ and call it a structural permutation.

* For each $\Theta$ and $\Gamma,\Delta$, a linear hom-set $\Pl(\Theta|\Gamma;\Delta)$ containing linear morphisms,
with a functorial action by a structural map $\si : \Theta' \to \Theta$ and structural permutations $\tau : \Gamma'\to \Gamma$ and $\rho : \Delta' \to \Delta$:

\[ \act{\rho}{-}{\si|\tau} : \Pl(\Theta|\Gamma;\Delta) \to \Pl(\Theta'|\Gamma';\Delta'). \]

* For each $A$ an identity morphism $1_A \in \Pl(|A;A)$.

* Composition morphisms

∘_A    :  (Θ|Γ_1,A,Γ_2;Δ) ×(Θ'|Γ';Δ'_1,A,Δ'_2)

∘_X    : (Θ_1,X,Θ_2|Γ;Δ) ×(Υ;X)       (Θ_1,Υ,Θ_2|Γ;Δ)

that are associative, unital, and equivariant in all reasonable ways.
(Note that by equivariance, all the compositions are uniquely determined by those in which $\Theta_2,\Gamma_2,\Delta_2'$ are empty.)

A functor $H:\cP\to\cQ$ between polycategories consists of functions between their linear and nonlinear objects and morphisms, preserving domains, codomains, structural actions, identities, and composites.
A transformation $\al : H \Rightarrow K : \cP\to\cQ$ between functors consists of:

* For each nonlinear object $X$ of , a nonlinear morphism $\al_X \in \nonlinhom{\cQ}(H X; K X)$.

* For each linear object $A$ of , a linear morphism $\al_A \in \linhom{\cQ}(|H A ; K A)$.

* For each nonlinear $f\in \Pnl(\Theta;Y)$, we have $\al_Y \circ H f = K f \circ (\al_\Theta)$.[Here if $\Theta = (X_1,\dots,X_n)$ then $K f \circ (\al_\Theta)$ denotes $(\cdots(K f \circ_{X_1} \al_{X_1}) \circ_{X_2} \al_{X_2} \cdots )\circ_{X_n} \al_{X_n} $, and similarly elsewhere.]

* For each linear $f\in \Pl(\Theta|\Gamma;\Delta)$, we have $(\al_\Delta) \circ H f = K f \circ (\al_\Theta\mid \al_\Gamma)$.

This defines a strict 2-category $\lnlpoly$.

polycategories are such a rich structure that they include many better-known structures as special cases.
(The reader unfamiliar with any of the structures mentioned below is free to take the asserted characterization as a definition.)

* Symmetric polycategories can be identified with polycategories having no nonlinear objects (and hence no nonlinear morphisms).
These model the judgmental structure of classical multiplicative-additive linear logic.

* Symmetric multicategories can be identified with polycategories having no nonlinear objects and in which all (linear) morphisms are co-unary, i.e. have a codomain of length 1.
These model the judgmental structure of intuitionistic multiplicative-additive linear logic.

* Even more degenerately, ordinary categories can be identified with polycategories having no nonlinear objects and in which all (linear) morphisms are both unary and co-unary.

* Cartesian multicategories can be identified with polycategories having no linear objects and no linear morphisms (here the former does not quite imply the latter, as there are homsets $\Pl(\Theta|;\,)$).
These model the judgmental structure of intuitionistic (nonlinear) logic.

* By an multicategory we will mean an polycategory in which all linear morphisms are co-unary.
These model the judgmental structure of intuitionistic linear logic (with exponentials); they do not quite appear in the literature, though a structure like them is the goal of [24] (see <ref>).

In fact, each of the above five subcategories is a slice category $\lnlpoly/\cS$ for some subterminal object $\cS$.
The terminal object of $\lnlpoly$ has one linear object, one nonlinear object, and all hom-sets singletons; thus a subterminal object has at most one object of each sort and each hom-set a subsingleton.

The slice category $\lnlpoly/\cS$ over a subterminal is thus the full subcategory of $\lnlpoly$ consisting of those objects whose unique map to the terminal object factors through $\cS$.
This means that if has only objects of the sorts that does, and only morphisms of the arity and co-arity that does.

For example, let $\mathsc{sympoly}$ be the subterminal object with one linear object, no nonlinear objects, and all linear homsets singletons.
Then $\lnlpoly/\mathsc{sympoly}$ consists of polycategories with no nonlinear objects, i.e. symmetric polycategories.
We can argue similarly for the following suggestively-named subterminals:

* $\mathsc{symmulti}$, which has one linear object, no nonlinear objects, co-unary linear homsets singletons, and others empty.

* $\mathsc{cat}$, which has one linear object, no nonlinear objects, and only the identity morphism.

* $\mathsc{cartmulti}$, which has one nonlinear object, no linear objects, all nonlinear homsets singletons, and all linear homsets empty.

* $\mathsc{lnlmulti}$, which has one linear object, one nonlinear object, all nonlinear homsets and co-unary linear homsets singletons, and others empty.

For consistency, we may write the terminal object of $\lnlpoly$ as $\mathsc{lnlpoly}$.

The slice category over any subterminal object is coreflective, with coreflector $(-)\times \cS$.
Thus, all five of these subcategories are coreflective.
In particular, any polycategory has an underlying symmetric polycategory, which we denote $\Plin$, and an underlying cartesian multicategory, which we denote $\Pnonlin$.

There is also an multicategory $\mathsc{plmulti}$ such that the objects of the slice $\lnlpoly/\mathsc{plmulti}$ are equivalent to planar (i.e. non-symmetric) multicategories.
Specifically, let $\mathsc{plmulti}$ have one linear object, no nonlinear objects, and morphisms with arity $n$ and co-arity 1 labeled by permutations of $n$ objects.
Then we can map a planar multicategory to the symmetric multicategory it generates freely, with each $n$-ary morphism generating $n!$ such morphisms permuted by the symmetric action, and the projection to $\mathsc{plmulti}$ remembering the permutation.
Thus, planar multicategories can also be regarded as particular polycategories — although unlike the slices considered in <ref>, $\mathsc{plmulti}$ is not subterminal, so $\lnlpoly/\mathsc{plmulti}$ is not a full subcategory of $\lnlpoly$.

However, an analogous construction is not possible for planar polycategories; freely adding symmetric actions does not yield a symmetric polycategory, as not all composites are definable <cit.>.
Informally, the gap between planar and symmetric is wider in the classical case than in the intuitionistic one.
This is one reason that in this paper we focus on the symmetric case.

As noted in <ref>, polycategories are a semantic counterpart of “split-context” syntaxes such as [7, 4, 17].
It may thus be surprising that although we are modeling classical linear logic, we have nevertheless only split the left-hand context, as is done in intuitionistic linear syntaxes such as [7, 4], rather than splitting both contexts as in [17].
There are two reasons for this.

The first is that it is simpler and sufficient.
As we will see below, even with only one split context we can still characterize both modalities $\oc$ and $\wn$ by universal properties.
This is a polycategorical version of the observation that to model classical linear logic it suffices to have an adjunction (which models intuitionistic linear logic) whose linear category is $\ast$-autonomous; there is no need to add a second nonlinear category.
Moreover, most natural examples have this form anyway.

By the way, note that the apparent asymmetry in splitting the left-hand context, rather than the right-hand one, is really just an artifact of notation.
We could equally well write $\Pl(\Theta|\Gamma;\Delta)$ as ${\cP\big(\Gamma\mathbin{;} \Delta\mid\Theta\big)}$, reversing the direction of the nonlinear morphisms so they form a “co-cartesian co-multicategory”.
But splitting the left-hand context is more intuitive and remains closer to the natural examples.

The second reason is that “doubly-split” polycategories, at least for one definition of such, are actually a special case of singly-split ones.
Let $\mathsc{dblsplit}$ be the polycategory with one linear object, two nonlinear objects, and all homsets singletons.
Then an object of the slice category $\lnlpoly/\mathsc{dblsplit}$ is an polycategory equipped with a partition of its nonlinear objects into two subsets, which we may call the “left-hand objects” and the “right-hand objects”.
Accordingly, we can choose to denote its linear homsets by ${\cP\big(\Theta\mid \Gamma\mathbin{;} \Delta\mid\Upsilon\big)}$, where $\Theta$ consists of left-hand objects and $\Upsilon$ of right-hand objects.
Similarly, if $\Upsilon$ consists of right-hand objects and $Z$ is a right-hand object, we can write the nonlinear homset $\cP\big(\Upsilon \mathbin{;} Z\big)$ as $\cP\big(Z \mathbin{;} \Upsilon\big)$, thereby regarding the right-hand objects as forming a co-cartesian co-multicategory, which acts on the linear homsets ${\cP\big(\Theta\mid \Gamma\mathbin{;} \Delta\mid\Upsilon\big)}$ on the right.

The only possibly-surprising thing about this notion of “doubly-split polycategory” is that we also have “mixed nonlinear homsets” $\Pnl(\Theta,\Upsilon;X)$ (perhaps better written $\cP\big(\Theta \mathbin{;} X \mathbin{;} \Upsilon\big)$) where $\Theta$ consists of left-hand objects, $\Upsilon$ of right-hand objects, and $X$ could be of either sort.
However, such mixed morphisms arise naturally as the result of weakening a “pure” nonlinear morphism of either handedness by objects of the other handedness, and once we have these there is no reason there couldn't be other morphisms of the same sort as well (see, for instance, <ref>).

Note also that there is a morphism to $\mathsc{dblsplit}$ from the terminal object $\mathsc{lnlpoly}$ (in fact, two of them), so that our category $\lnlpoly$ is also equivalent to a slice category of this category $\lnlpoly/\mathsc{dblsplit}$ of doubly-split polycategories.
Thus, formally we could take either one as the primitive notion and define the other in terms of it.
We have chosen the singly-split notion as primitive, since it is, as noted above, simpler and sufficient.

We will see some more examples of polycategories in <ref>, but first we define the basic universal properties that appear therein.
Inspired by [10], we say that a morphism $\psi$ in an polycategory containing an object $R$ (linear or nonlinear) in its domain or codomain is universal in $R$ if composing along $R$ induces bijections on homsets of all possible types.
For the five possible combination of types for $\psi$ and $R$, this specializes to the following.

Let $X$ be a nonlinear object and $A$ a linear object.

* A nonlinear morphism $\psi\in\Pnl(\Theta;X)$ is universal in $X$ if composing with $\psi$ induces bijections

\begin{align*}
\Pnl(\Theta',X;Y) &\toiso \Pnl(\Theta',\Theta;Y)\\
\Pl(\Theta',X|\Gamma;\Delta) &\toiso \Pl(\Theta',\Theta|\Gamma;\Delta).
\end{align*}

* A nonlinear morphism $\psi\in\Pnl(\Theta,X;Y)$ is universal in $X$ if composing with $\psi$ induces bijections

\begin{align*}
\Pnl(\Theta';X) &\toiso \Pnl(\Theta,\Theta';Y).
\end{align*}

* A linear morphism $\psi \in \Pl(\Theta,X|\Gamma;\Delta)$ is universal in $X$ if composing with $\psi$ induces bijections

\begin{align*}
\Pnl(\Theta';X) &\toiso \Pl(\Theta,\Theta'|\Gamma;\Delta).
\end{align*}

* A linear morphism $\psi \in \Pl(\Theta|\Gamma;\Delta,A)$ is universal in $A$ if composing with $\psi$ induces bijections

\begin{align*}
\Pl(\Theta'|\Gamma',A;\Delta') &\toiso \Pl(\Theta',\Theta|\Gamma',\Gamma;\Delta',\Delta).
\end{align*}

* A linear morphism $\psi \in \Pl(\Theta|\Gamma,A;\Delta)$ is universal in $A$ if composing with $\psi$ induces bijections

\begin{align*}
\Pl(\Theta'|\Gamma';\Delta',A) &\toiso \Pl(\Theta',\Theta|\Gamma',\Gamma;\Delta',\Delta).
\end{align*}

A functor is said to preserve a certain kind of universal morphism it it takes any such morphism to a similarly universal morphism.

Universal morphisms are unique up to unique isomorphism:

If $\psi \in \Pl(\Theta|\Gamma;\Delta,A)$ and $\psi' \in \Pl(\Theta|\Gamma;\Delta,A')$ are universal in $A$ and $A'$ respectively, then there is a unique isomorphism $\phi : A\cong A'$ such that $\phi \circ_A \psi = \psi'$; and similarly for other kinds of universal morphism.

As usual, $\phi$ is determined by applying the universal property of $\psi$ to $\psi'$, and conversely for its inverse.

We now explore the most important cases of universality, starting with versions of the polycategorical representability conditions from [13, 10].
For clarity and conciseness, we indicate the object in which a universal morphism is universal by underlining it, e.g. $\psi \in \Pl(\Theta|\Gamma,\underline{A};\Delta)$.

Let $A,B$ be linear objects in an polycategory .

* A tensor product of $A,B$ is a universal morphism $\psi \in \Pl(|A,B;\underline{A\ten B})$.

* A cotensor product of $A,B$ is a universal morphism $\psi \in \Pl(|\underline{A\coten B}; A,B)$.

* A unit $\unit$ is a universal morphism $\psi\in \Pl(|;\,\underline{\unit})$.

* A counit $\counit$ is a universal morphism $\psi\in \Pl(|\underline{\counit};)$.

* A dual of $A$ is a universal morphism $\psi\in \Pl(|A,\underline{\d A};)$.

We say that “has $\ten$” if any $A,B$ have a tensor product, and so on.

A dual is equivalently a universal morphism $\psi\in \Pl(|;\,A,\underline{\d A})$;
see e.g. [10].

These universal properties specialize in the case $\Theta=\emptyset$ to the like-named ones in the symmetric polycategory $\Plin$.
Thus, as shown in [13, 10], if an polycategory has all $\ten,\coten,\unit,\counit$ then $\Plin$ is a linearly distributive category, and if it also has all $\duals$ then $\Plin$ is $\ast$-autonomous [2, 3, 13].

We similarly have tensors and units of nonlinear objects, but these turn out to coincide with cartesian products, by the following folklore analogue of the equivalence between positive and negative presentations of product types in structural logic.

The following are equivalent for objects $X,Y$ and $X\times Y$ of an polycategory.

* There is a universal morphism $\psi \in \Pnl(X,Y;\underline{X\times Y})$.
In other words, composing with $\psi$ induces bijections

\begin{align*}
\Pnl(\Theta,X\times Y;Z)&\toiso \Pnl(\Theta,X,Y;Z)\\
\Pl(\Theta,X\times Y|\Gamma;\Delta) &\toiso \Pl(\Theta,X,Y|\Gamma;\Delta).
\end{align*}

* There is a morphism $\psi \in \Pnl(X,Y;X\times Y)$ inducing bijections

\begin{align*}
\Pnl(\Theta,X\times Y;Z)&\toiso \Pnl(\Theta,X,Y;Z)
\end{align*}

* There are $\pi_1 \in \Pnl(X\times Y;X)$ and $\pi_2 \in \Pnl(X\times Y;Y)$ inducing bijections

\[ \Pnl(\Theta;X\times Y) \toiso \Pnl(\Theta;X) \times \Pnl(\Theta;Y). \]

* There are morphisms $\psi \in \Pnl(X,Y;X\times Y)$ and $\pi_1 \in \Pnl(X\times Y;X)$ and $\pi_2 \in \Pnl(X\times Y;Y)$ such that the composites

(X,Y) ψ X×Y π_1 X(X,Y) ψ X×Y π_2 Y(X×Y, X×Y) (π_1,π_2) (X,Y) ψ X×Y

are the image of identities under structural maps.

Of course <ref> implies <ref>, so it suffices to prove that <ref> and <ref> each imply <ref> and that <ref> implies <ref> and <ref>.

Assuming <ref>, let $\pi_1:X\times Y \to X$ be the image of $1_X$ under the composite

\[ \Pnl(X;X) \to \Pnl(X,Y;X) \toiso \Pnl(X\times Y;X), \]

of a structural map and the universal property of <ref>, and similarly for $\pi_2$.
The equations in <ref> hold by the universal property.

Assuming <ref>, $\psi : (X,Y) \to X\times Y$ is the image of $(1_X,1_Y)$ under the composite

\[ \Pnl(X;X) \times \Pnl(Y;Y) \to \Pnl(X,Y;X) \times \Pnl(X,Y;Y) \to \Pnl(X,Y;X\times Y) \]

of structural maps with the universal property of <ref>.
Again, the equations in <ref> hold by the universal property.

Conversely, assuming <ref>, the right-to-left directions of <ref> are composing with $(\pi_1,\pi_2)$ and a structural map, while the right-to-left direction of <ref> is composing with $\psi$ and a structural map.
These are inverses by the equations in <ref>.

We will refer to such an $X\times Y$ as a product of $X$ and $Y$.
There is an analogue for nullary products and terminal nonlinear objects, denoted $1$ (not to be confused with the linear $\unit$).
By <ref><ref>, if all $\times,1$ exist then $\Pnonlin$ is a cartesian monoidal category.
Note that these are essentially facts about cartesian multicategories, which extend automatically to an polycategory from $\Pnonlin$.

Any functor of polycategories preserves nonlinear products and terminal objects.

The equations in <ref><ref> are preserved by any functor.

If we changed notation as suggested in <ref> to regard the nonlinear objects (or the “right-hand” ones) as instead forming a co-cartesian co-multicategory, then the identical operations $\times$ and $1$ would instead behave like a coproduct and an initial object (and hence would be better denoted $+$ and $\varnothing$).

We now consider the storage modalities that relate linear and nonlinear objects.

Let $X$ be a nonlinear object and $A$ a linear one.

* An $\foc$-modality is a universal morphism $\psi\in\Pl(X|;\,\underline{\foc X})$.

* A $\uoc$-modality is a universal morphism $\psi\in\Pl(\underline{\uoc A}|;\,A)$.

* An $\fwn$-modality is a universal morphism $\psi\in\Pl(X|\underline{\fwn X};)$.

* A $\uwn$-modality is a universal morphism $\psi\in\Pl(\underline{\uwn A}|A;)$.

Thus, the storage modalities are characterized by natural bijections

(Θ,X|Γ;Δ)    ≅(Θ|Γ,X;Δ)        (Θ|; A)    ≅(Θ;A)

(Θ,X|Γ;Δ)    ≅(Θ|Γ;Δ,X)        (Θ|A;)    ≅(Θ;A).

Note that $\foc$ and $\uoc$ are covariant, while $\fwn$ and $\uwn$ are contravariant.
We will see below that these are adjoint in pairs, $\foc\adj\uoc$ and $\uwn\adj\fwn$, and induce the usual comonad $\oc = \foc\uoc$ and monad $\wn = \fwn\uwn$.

We can also consider internal-homs of various sorts.

Let $X,Y$ be nonlinear objects and $A,B$ be linear objects.

* A linear hom is a universal morphism $\psi\in\Pl(|\underline{A\hom B}, A; B)$.

* A linear co-hom is a universal morphism $\psi\in\Pl(|B; \underline{B\cohom A}, A)$.

* A nonlinear hom is a universal morphism $\psi\in\Pnl(\underline{X\to Y}, X; Y)$.

* A mixed hom is one of the following:[As notational mnemonics,
the arrowhead in $\to,\mixedhom,\mixedeechom$ indicates the domain object is nonlinear,
the open circle in $\hom,\mixedhom$ indicates the codomain object and hom-object are both linear,
and the closed circle in $\eechom,\mixedeechom$ indicates the codomain object is linear but the hom-object is nonlinear.]

* a universal morphism $\psi\in\Pl(X | \underline{X\mixedhom B}; B)$.

* a universal morphism $\psi\in\Pl(\underline{A\eechom B}| A ; B)$.

* a universal morphism $\psi\in\Pl(\underline{X\mixedeechom B} , X | ;\, B)$.

Thus, these various kinds of homs are characterized by bijections

\begin{align*}
\Pl(\Theta|\Gamma,A;\Delta,B) &\cong \Pl(\Theta|\Gamma;\Delta,A\hom B)\\
\Pl(\Theta|\Gamma,B;\Delta,A) &\cong \Pl(\Theta|\Gamma,B\cohom A;\Delta)\\
\Pnl(\Theta,X;Y) &\cong \Pnl(\Theta;X\to Y)\\
\Pl(\Theta,X | \Gamma ;\Delta, B) &\cong \Pl(\Theta|\Gamma;\Delta, X \mixedhom B)\\ %\label{eq:mixedhom}\\
\Pl(\Theta | A ; B) &\cong \Pnl(\Theta ; A \eechom B)\\ %\label{eq:eechom}
\Pl(\Theta,X | ;\, B) &\cong \Pnl(\Theta ; X \mixedeechom B).
\end{align*}

In particular:

* If $\ten,\unit,\hom$ exist then the monoidal structure $\ten$ on $\Plin$ is closed.

* If $\coten,\counit,\cohom$ exist then the monoidal structure $\coten$ on $\Plin$ is coclosed.

* If $\times,1,\to$ exist then $\Pnonlin$ is cartesian closed.

The mixed homs suggest analogous mixed tensor products, such as universal morphisms $\psi\in \Pl(X | A ; \underline{X\rtimes A})$,
or $\psi\in\Pl(X,Y | ; \, \underline{X\boxtimes Y})$.
However, lest we start to feel the zoo of universal properties is too large, we note that the more exotic sorts can be constructed from the simpler ones in the following sense.

If $\psi$ is universal in $R$, while $\phi$ contains $R$ in its domain or codomain and is universal in a different object $S$, then $\psi\circ_R \phi$ is universal in $S$.

There are a number of different versions of this statement depending on the types of $R,S,\psi,\phi$ and whether the objects occur in domain or codomain, but they all reduce to “the composite of bijections is a bijection”.
See <ref> for a more rigorous proof.

One instance of this is the associativity of tensors: given universal morphisms

ψ_1    ∈( | A,B; AB)        ψ_3    ∈( | AB, C; (AB)C)

ψ_2    ∈(| B,C; BC)        ψ_4    ∈( | A, BC; A(BC))

the two composites

\begin{align*}
\psi_3 \circ_{A\ten B} \psi_1 &\in \Pl(| A,B,C; \underline{(A\ten B)\ten C}) \\
\psi_4 \circ_{B\ten C} \psi_2 &\in \Pl(|A,B,C; \underline{A\ten (B\ten C)})
\end{align*}

are both universal, hence by <ref> there is an induced isomorphism $(A\ten B)\ten C \cong A\ten (B\ten C)$.
This is how $(\ten,\unit)$ is shown to be a monoidal structure, and similarly for $(\coten,\counit)$ and (if we like) $(\times,1)$.

Another familiar instance is that in a $\ast$-autonomous category, linear homs can be defined in terms of duals and cotensors if these exist.
Given universal morphisms

ψ_1 ∈(| Ạ,A;) ψ_2 ∈(| Ạ B; Ạ,B)

their composite $\psi_1 \circ_{\d A} \psi_2 \in \Pl(|\underline{\d A \coten B}, A;B)$ is universal in $\d A \coten B$, exhibiting it as $A\hom B$.
Similarly, we have $B \cohom A = \d A \ten B$, and De Morgan duality:

A B = (̣Ạ̣Ḅ̣)̣

X = (̣X̣)̣
A = (Ạ)

In particular, $\Plin$ is $\ast$-autonomous as soon as $\cP$ has $\ten,\unit,\duals$.
And as in a $\ast$-autonomous category, duals can be constructed by homming into the counit:

\[ \d A = A \hom \counit . \]

Less familiar instances of <ref> relate the modalities to the tensors and homs, particularly the mixed ones: we have

X B    = X B        X ⋊A    = X A

A B    = (AB)        X⊠Y    = (X×Y)

X B    = (X B)        X⊠Y    = X Y

X B    = X →B           = 1

A    = A        X    = X ⋊

A    = 1 A        X    = X ⊠1

whenever all the operations on the right-hand side exist.
In particular, since both $\foc(X\times Y)$ and $\foc X \ten \foc Y$ have the universal property of $X\boxtimes Y$, they are isomorphic if they both exist.
(This is, of course, closely related to Seely's characterization of the modality $\oc$; see <ref>.)
Thus, if $\ten,\unit,\times,1,\foc$ exist then $\foc$ is a strong monoidal functor.
Similarly, if both $\uoc (\foc X \hom B)$ and $X \to \uoc B$ exist they are isomorphic (which is related to Girard's embedding of nonlinear logic in linear logic); if $\fwn(X\times Y)$ and $\fwn X \coten \fwn Y$ exist they are isomorphic; and so on.

As a trivial instance, a unary co-unary linear morphism, i.e. one of the form $\psi \in \Pl( | A; B)$, is universal if and only if it is an isomorphism (and similarly in the nonlinear case).
Thus, <ref> also implies that universal morphisms are stable under composition with isomorphisms, conversely to <ref>.

We can also consider limits and colimits in polycategories.
In general, we require a limit of a diagram of linear or nonlinear objects (and unary co-unary morphisms) to induce bijections on all hom-sets where it appears in the codomain, and similarly for a colimit whenever it appears in the domain.
(In the case of products and coproducts, this definition appears in [38].)
The simplest case of this is that a limit of nonlinear objects satisfies

\[\Pnl(\Theta;\lim_i X_i)\cong \lim_i \Pnl(\Theta;X_i),\]

generalizing <ref><ref> and reducing to an ordinary limit in the cartesian monoidal $\Pnonlin$ if $\times,1$ exist.
However, a colimit of nonlinear objects satisfies both

\begin{align}
\Pnl(\Theta,\colim_i X_i;Y) &\cong \lim_i \Pnl(\Theta,X_i;Y)\label{eq:nlcolim1}\\
\Pl(\Theta,\colim_i X_i|\Gamma;\Delta) &\cong \lim_i \Pl(\Theta,X_i|\Gamma;\Delta)\label{eq:nlcolim2}
\end{align}

induced by the same universal cocone.
This implies that the colimit is

* preserved in each variable by $\times$, insofar as it exists;

* sent by $\foc$ to a colimit in $\Plin$ that is preserved in each variable by $\ten$, insofar as $\foc,\ten$ exist; and

* sent by $\fwn$ to a limit in $\Plin$ that is preserved in each variable by $\coten$, insofar as $\fwn,\coten$ exist.

Moreover, if all $\times,\foc,\fwn,\ten,\coten$ exist, then a colimit in the ordinary category $\Pnonlin$ is a colimit in $\cP$ if and only if it preserved in these ways.

Similarly, a colimit of linear objects satisfies

\begin{equation}
\Pl(\Theta|\Gamma,\colim_i A_i;\Delta) \cong \lim_i \Pl(\Theta|\Gamma,A_i;\Delta)\label{eq:lcolim}
\end{equation}

which implies that it is preserved by $\ten$ in each variable and sent by $\uwn$ to a limit in $\Pnonlin$, insofar as $\ten,\uwn$ exist.
If all $\ten,\coten,\counit,\foc$ exist, then a colimit in the ordinary category $\Plin$ is a colimit in if and only if it is preserved by $\ten$.
Dually, a limit of linear objects satisfies

\begin{equation}
\Pl(\Theta|\Gamma;\Delta,\lim_i A_i) \cong \lim_i \Pl(\Theta|\Gamma;\Delta,A_i)\label{eq:llim}
\end{equation}

which implies that it is preserved by $\coten$ in each variable and sent by $\uoc$ to a limit in $\Pnonlin$, insofar as $\coten,\uoc$ exist.
And if all $\coten,\ten,\unit,\foc$ exist, a colimit in $\Plin$ is a colimit in if and only if it is preserved by $\coten$.
Note also that $\ten$ preserves all colimits if $\hom$ exists, $\foc$ preserves all colimits if $\uoc$ exists, and so on.

We will write $X+Y$ for the coproduct of nonlinear objects and $\varnothing$ for the initial nonlinear object, and we denote finite products and coproducts of linear objects with Girard's notation for the linear logic additive connectives: $A\with B$ for the product, $A\oplus B$ for the coproduct, $\top$ for the terminal object, and $0$ for the initial object.
Thus the above preservation properties state that

X×(Y+Z)    ≅(X×Y) + (X×Z)       X ×∅   ≅∅

(X+Y)    ≅X ⊕Y       ∅   ≅0

(X+Y)    ≅X Y       ∅   ≅⊤

A (B⊕C)    ≅(AB) ⊕(AC)       A0    ≅0

(A⊕B)    ≅A ×B       0    ≅1

A (BC)    ≅(AB) (AC)       A ⊤   ≅⊤

(AB)    ≅A ×B       ⊤   ≅1

If we specialize the above universal properties to symmetric polycategories, symmetric multicategories, cartesian multicategories, or multicategories, there are three possible results.
Some universal properties make sense unmodified, such as $\ten,\coten$ in polycategories or $\times,\to$ in cartesian multicategories.
Others make no sense at all, such as $\coten,\counit$ in multicategories or $\foc,\uoc$ in symmetric polycategories.

A third group can only have a restricted universal property.
Specifically, limits and colimits in a symmetric multicategory or multicategory can only induce bijections of hom-sets with unary codomain: instead of (<ref>)–(<ref>) we assert only

\begin{align*}
\Pl(\Theta,\colim_i X_i|\Gamma;B) &\cong \lim_i \Pl(\Theta,X_i|\Gamma;B)\\
\Pl(\Theta|\Gamma,\colim_i A_i;B) &\cong \lim_i \Pl(\Theta|\Gamma,A_i;B)\\
\Pl(\Theta|\Gamma;\lim_i A_i) &\cong \lim_i \Pl(\Theta|\Gamma;A_i).
\end{align*}

Since the left- and right-hand sides of (<ref>)–(<ref>) have the same codomain arity, these apparently-weaker universal properties are equivalent to (<ref>)–(<ref>) for limits and colimits are over nonempty domain categories.
But the limit of the empty diagram of copies of the empty set is no longer empty, so an initial or terminal object in an multicategory (in the above sense) need not be initial or terminal in qua polycategory.

In fact, an multicategory cannot have a terminal linear object, or an initial linear or nonlinear object, in the -polycategorical sense.
For example, if $\top$ is a terminal linear object, we must have $\Pl(\Theta | \Gamma ; \Delta,\top) = 1$ for all $\Delta$, whereas in an multicategory we have $\Pl(\Theta | \Gamma ; \Delta,\top) = \emptyset$ if $|\Delta|>0$.
This is already the case for ordinary multicategories and polycategories.

The categorization of universal properties in these four subcategories into these three groups is shown in <ref>.

Unmodified     Nonsensical     Modified

symm. multi.
cart. multi.

Universal properties in subcategories

§ RELATION TO THE LITERATURE

By our observations in <ref>,

the following categorical structures can be identified with certain polycategories:

* Symmetric monoidal categories.

* Symmetric monoidal categories with any desired limits, and any desired colimits that are preserved in each variable by the tensor product.

* Closed symmetric monoidal categories, with any desired limits and colimits (the latter automatically preserved by the tensor product, due to closedness).

* Cartesian monoidal categories.

* Cartesian monoidal categories with any desired limits, and any desired colimits that are preserved in each variable by the cartesian product.

* Cartesian closed categories, with any desired limits and colimits.

* Symmetric linearly distributive categories.

* Symmetric linearly distributive categories with any desired colimits that are preserved in each variable by the tensor product, and any desired limits that are preserved in each variable by the cotensor product.

* (Symmetric) $\ast$-autonomous categories, with any desired limits and colimits.

The “strong” morphisms between these structures (those that preserve all the asserted categorical structure up to coherent isomorphisms) can also be identified with functors of polycategories that preserve the relevant universal properties, and similarly for the transformations.
In other words, the standard 2-categories of the above structures are equivalent to locally full sub-2-categories of .

We now add the modalities, starting with the “intuitionistic” case of multicategories.
These are designed to model split-context intuitionistic linear logic syntaxes such as [7, 4], without necessarily assuming that any connectives exist.
But if enough connectives do exist, they reduce to a better-known notion of model for intuitionistic multiplicative-exponential linear logic:

An multicategory in which the modality $\foc$ exists is uniquely determined by a functor of symmetric multicategories

\[ \foc : \Pnonlin \to \Plin \]

where $\Pnonlin$ is a cartesian multicategory and $\Plin$ a symmetric one.

* The modality $\uoc$ also exists if and only if the functor $\foc$ has a right adjoint (in the 2-category of symmetric multicategories).

* If $\times,1,\ten,\unit$ exist, then $\foc$ is equivalently a strong symmetric monoidal functor from a cartesian monoidal category to a symmetric monoidal one.

* Thus, an multicategory with $\times,1,\ten,\unit,\foc,\uoc$ is equivalently an adjunction [7, 35]: a symmetric monoidal adjunction from a cartesian monoidal category to a symmetric monoidal one.

Given the modality $\foc$, we make it a functor by composing with $(Y\mid\,) \to \foc Y$ and applying its universal property:

\[ \Pnl(X_1,\dots,X_n;Y) \to \Pl(X_1,\dots,X_n|{};\, \foc Y) \toiso \Pl(| \foc X_1,\dots,\foc X_n ; \foc Y). \]

Conversely, given a functor $\foc$, we define the general linear hom-sets by

\[\Pl(X_1,\dots,X_n | \Gamma;B) = \Plin(\foc X_1,\dots,\foc X_n,\Gamma\mathbin{;}B).\]

Statement <ref> is then a multicategorical version of the standard equivalence between adjunctions defined with bijections of hom-sets and with unit and counit.
We have already noted <ref>,

and <ref> follows immediately.

Benton [7] assumed $\Pnonlin$ cartesian closed and $\Plin$ symmetric monoidal closed, but later authors have observed that this is unnecessary for the bare definition.
If both categories are closed we will speak of a closed adjunction.

Since left adjoints preserve colimits and right adjoints preserve limits, the following structures also form locally full sub-2-categories of :

* adjunctions.

* adjunctions with any desired limits and colimits in either category, such that colimits are preserved by the product or tensor product in each variable.

* Closed adjunctions, with any desired limits and colimits in either category.

The notion of adjunction does depend on having both $\otimes$ and $\times$, whereas multicategories can specify the correct behavior of $\foc$ and $\uoc$ even if $\otimes,\times$ may not exist.
As evidence for this correctness, we note that $\times,1$ are not necessary for the induced comonad on $\lin\cP$ to coincide with a structure also existing in the literature.

If is an multicategory with $\ten,\unit,\foc,\uoc$, the symmetric monoidal category $\Plin$ admits a linear exponential comonad [5, 23], i.e. it is a linear category in the sense of [7].

Let $\oc$ be the comonad $\foc\uoc$.
To give the map $\oc A \ten \oc B \to \oc (A\ten B)$, we act on the $\ten$-universal morphism $(\,\mid A,B) \to A\ten B$ as follows.
The two noninvertible maps are composition with the $\uoc$-universal morphisms $(\uoc A\mid\,) \to A$ and $(\uoc B\mid\,) \to B$ and with the $\foc$-universal morphism $(\uoc(A\ten B) \mid\, ) \to \foc\uoc(A\ten B)$:

→        (A, B | ;   AB)

(A, B;(AB))

→        (A,B | ;  (AB))

(|A, B ; (AB))

(|A B ; (AB)).

Similarly, to give the map $\oc A \to \oc A \ten \oc A$ we act on the $\ten$-universal morphism $(\oc A, \oc A) \to \oc A \ten \oc A$ as follows.
The two noninvertible maps are composition with the $\foc$-universal morphism $(\uoc A \mid \,) \to \foc\uoc A = \oc A$ and a structural map.

(|A, A;A A)
=        (|A, A; A A)

→        (A, A| ;  A A)

→        (A| ;  A A)

(|A; A A).

The nullary cases are similar, and the axioms follow by universal properties.

This implication for adjunctions was observed in <cit.>; multicategories give a way to state and prove it even in the absence of $\times,1$.

The Eilenberg–Moore adjunction of any linear exponential comonad $\oc$ determines an multicategory with $\times,1,\ten,\unit,\foc,\uoc$, whose underlying linear exponential comonad recovers the given $\oc$.

Such an Eilenberg–Moore adjunction is an adjunction (see <cit.> and <cit.>), hence an multicategory with $\times,1,\ten,\unit,\foc,\uoc$.

Moreover, since any subset of objects of a multicategory determines a sub-multicategory (in stark contrast to the situation for monoidal categories), we still obtain an multicategory with $\ten,\unit,\foc,\uoc$ if we restrict to any subset of the $\oc$-coalgebras containing the cofree ones.
The smallest choice, of course, consists of exactly the cofree coalgebras, so we have:

The Kleisli adjunction of any linear exponential comonad $\oc$ determines an multicategory with $\ten,\unit,\foc,\uoc$, whose underlying linear exponential comonad recovers the given $\oc$.

To incorporate the Kleisli adjunction in the purely monoidal case, one has to assume that cofree coalgebras are closed under products.
This follows for instance if the monoidal category has products <cit.>, in which case we recover the notion of Seely comonad, characterized by $\oc A \ten \oc B \cong \oc (A\with B)$.
But polycategories allow us to include the Kleisli case even when $\with$ doesn't exist.

There are also intermediate choices between the Eilenberg–Moore category (all coalgebras) and Kleisli category (cofree coalgebras), such as the category of finite products of cofree coalgebras (if has finite products), or category of exponentiable coalgebras (if is closed monoidal), as discussed in <cit.>.

Here is another situation that polycategories allow us to treat more generally.

Let be a symmetric multicategory; we can enhance it to an multicategory with $\foc$ by taking the nonlinear objects to be the commutative comonoids in .
It may not be immediately obvious how to define a comonoid in a multicategory that lacks $\ten$, but it is possible: $C$ is a comonoid when it is equipped with operations

\begin{align*}
\nonlinhom\cE(\Theta_1,C,C,\Theta_2;B) &\to \nonlinhom\cE(\Theta_1,C,\Theta_2;B)\\
\nonlinhom\cE(\Theta_1,\Theta_2;B) &\to \nonlinhom\cE(\Theta_1,C,\Theta_2;B)
\end{align*}

that are appropriately natural and equivariant.
Such cocommutative comonoids form a cartesian multicategory with a forgetful multicategory functor to , so by <ref> it yields an multicategory.

If is symmetric monoidal, then cocommutative comonoids form a cartesian monoidal category, so this multicategory has $\times,1,\ten,\unit,\foc$.
Thus, if $\foc$ has a right adjoint $\uoc$, i.e. if cofree cocommutative comonoids exist, then it is an adjunction, known as a Lafont category [28] or a free exponential modality [37].
But we get an multicategory even without these assumptions.

In general, given a category with a linear exponential comonad, we prefer to regard it as an multicategory via the Kleisli construction rather than the Eilenberg–Moore construction.
The reason for this is the following folklore observation, showing that Kleisli adjunctions can be detected by a purely intrinsic condition:

An adjunction $F : \cA \toot \cB : G$ is equivalent to the Kleisli adjunction of the monad $GF$ if and only if its left adjoint $F$ is essentially surjective on objects, and isomorphic to that Kleisli adjunction if and only if $F$ is bijective on objects.

The “only if” direction is clear, so suppose $F$ is essentially surjective on objects, and let $F_T : \cA \toot \cA_T : G_T$ be the Kleisli adjunction of the monad $T=GF$.
Thus the objects of $\cA_T$ are formal copies “$A_T$” of the objects $A\in \cA$, with $\cA_T(A_T,B_T) = \cA(A,T B)$.
There is a unique comparison functor $H:\cA_T \to \cB$  defined by $H(A_T) = F A$, which is essentially surjective on objects since $F$ is (and bijective on objects if $F$ is).
But it is also fully faithful, since $\cB(F A, F B) \cong \cA(A, G F B) = \cA(A, T B) = \cA_T(A_T,B_T)$; hence it is an equivalence.

Thus, applying the Kleisli construction, we have the following locally full sub-2-categories of :

* Symmetric monoidal categories with linear exponential comonad.
This includes Seely comonads (if the category has finite products) and Lafont comonads (if cofree cocommutative comonoids exist).

* Symmetric monoidal categories with linear exponential comonad and any desired limits and any desired colimits preserved by the tensor product in each variable.

* Closed symmetric monoidal categories with linear exponential comonad and any desired limits and colimits.

In each case the “strong” morphisms, corresponding to functors of multicategories that preserve (among other things) the storage modalities $\foc,\uoc$, are those that preserve the monad up to coherent isomorphism: $F(\oc A) \cong \oc (F A)$.

Note that all of these polycategories have the following property.

An polycategory is of Kleisli type if it is equipped with a choice of $\uoc$ that is bijective on objects.

multicategories of Kleisli type correspond to syntaxes for intuitionistic linear logic that have only one class of type, such as [4, 18], rather than two syntactic classes for “linear types” and “nonlinear types”.

We conjecture that the Linear Non-Linear multicategories suggested by [24] are equivalent to multicategories of Kleisli type.
In addition, the IL-indexed categories of [34] are equivalent to multicategories of Kleisli type having $\ten,\unit,\with,\top,\hom$, and $\mixedhom$ (our $\mixedhom$ being written “$\to$”).

We can also attempt to induce an multicategory from a monad on a cartesian monoidal category or multicategory.
In fact this is quite easy: the 2-category of symmetric multicategories has Eilenberg–Moore objects, so any monad $T$ therein on a multicategory induces an adjunction of multicategories $\cE \toot \cE^T$.
If is cartesian, by <ref> this yields an multicategory with $\foc,\uoc$.
The interesting thing is that if is representable, hence a (cartesian) monoidal category, then a symmetric-multicategory-monad on it is the same as a lax symmetric monoidal monad, and hence by [26] the same as a commutative strong monad.

Any commutative strong monad $T$ on a cartesian monoidal category induces an multicategory having $\foc,\uoc,\times,1,\unit$, where $\Pnonlin =\cE$ and the $\Plin$ is the symmetric multicategory of $T$-algebras.

* If is cartesian closed with equalizers, then has $\to,\hom$.

* If and $T$ are such that the category of $T$-algebras has coequalizers (e.g. is locally presentable and $T$ is accessible, or is cartesian closed with reflexive coequalizers preserved by $T$) then also has $\ten$, and thus is an adjunction.

We have already observed the first statement, except for noting that $\unit = T1$.
Statements <ref> and <ref> follow by results in the literature [25, 40].

Of course, we can also restrict to any full sub-multicategory of the Eilenberg–Moore category, such as the Kleisli category, and still have an multicategory.
As in the comonad case, when given a commutative strong monad on a cartesian monoidal category we generally regard it as an multicategory via the Kleisli construction; thus we have the following locally full sub-2-categories of :

* Cartesian monoidal categories with a commutative strong monad.

* Cartesian monoidal categories with a commutative strong monad and any desired limits and any desired colimits preserved by the product in each variable.

* Cartesian closed categories with a commutative strong monad and any desired limits and colimits.

A non-commutative monad $T$ on a cartesian monoidal category does not induce a multicategory structure on its Eilenberg–Moore category $\cE^T$.
However, as long as $T$ is a strong monad, we can still combine with $\cE^T$ to produce an multicategory, albeit a rather degenerate one.
Specifically, if $A$ and $B$ are $T$-algebras and $X$ is an object of , we can define an $X$-indexed family of algebra maps $A\to B$ to be a morphism $f:X\times A \to B$ such that the following diagram commutes:

\[
\begin{tikzcd}
X\times T A \ar[r] \ar[d] & T(X\times A) \ar[r,"T f"] & T B \ar[d] \\
X \times A \ar[rr,"f"'] && B
\end{tikzcd}
\]

in which the map $X\times T A \to T(X\times A)$ is the monad strength.

Any strong monad $T$ on a cartesian monoidal category induces an multicategory with $\Pnonlin = \cE$, whose linear objects are the $T$-algebras, with

\begin{align*}
\Pl(\Theta| ; \, A) &= \cE(\Theta; A) \\
\Pl(\Theta| A;B) &= \big\{ (\bigtimes\Theta)\text{-indexed families of algebra maps } A\to B \big\}
\end{align*}

and all other linear homsets empty.

This multicategory is linearly subunary, i.e. all its linear morphisms have linear codomain of length 1 and linear domain of length $\le 1$.
It has $\times,1,\uoc$, and also an $\foc$ with a weaker universal property:

\begin{equation}
\Pl(\Theta,X|;\,B) \cong \Pl(\Theta|\foc X;B).\label{eq:cbpv-foc}
\end{equation}

This is similar to the restriction on $\top,0$ in multicategories from <ref>.
It implies there is a $\unit$ (namely $\foc 1$) with a similarly restricted universal property.
Conversely, from $\rtimes$ and a restricted $\unit$, we can construct a restricted $\foc$ as $\foc X = X \rtimes \unit$.

This sort of multicategories provide semantics for “call-by-push-value” [31] and related theories.
In this case, they are usually described as enriched adjunctions, analogously to the definition of adjunctions as monoidal adjunctions.
To explain this, recall that if is cartesian monoidal, its Yoneda embedding $\cE \into [\cE\op,\fSet]$ is fully faithful and preserves products; thus any -enriched category can be regarded as an $[\cE\op,\fSet]$-enriched one.
In addition, itself is always $[\cE\op,\fSet]$-enriched, with hom-presheaves $\underline{\cE}(A,B)(X) = \cE(X\times A,B)$.

A linearly subunary multicategory with $\times,1$ is uniquely determined by a CBPV pre-structure [31]: a cartesian monoidal category , a category enriched over $[\cE\op,\fSet]$, and an $[\cE\op,\fSet]$-enriched functor $R:\cL \to [\cE\op,\fSet]$.

* The modality exists if and only if $R$ lands inside .

* If exists, then exists with restricted universal property (<ref>) if and only if $R:\cL \to \cE$ has an $[\cE\op,\fSet]$-enriched left adjoint.

* The hom-objects of lie in if and only if $\eechom$ exists.

* has $[\cE\op,\fSet]$-enriched powers by representables if and only if $\mixedhom$ exists, and copowers by representables if and only if $\rtimes$ exists.

* has $[\cE\op,\fSet]$-enriched finite products if and only if $\with,\top$ exist with a restricted universal property respecting the arity restrictions.

* is distributive [12] and the hom-presheaves of preserve finite coproducts if and only if $+,\varnothing$ exist with a restricted universal property.

Of course, corresponds to $\Pnonlin$, which is cartesian monoidal if and only if $\times,1$ exist.
The arity restrictions then ensure that the linear hom-sets are uniquely determined by those of the form $\Pl(X|A;B)$ and $\Pl(X|;\,B)$.
The former assemble into an $[\cE\op,\fSet]$-enriched category , and the latter into the functor $R$.

To say that $R$ lands in is to say that each functor $X\mapsto \Pl(X|;\,B)$ is representable, which is to say that exists.
Given this, (<ref>) says exactly that $\foc$ is an $[\cE\op,\fSet]$-enriched left adjoint of $\uoc$.
The other claims follow by similar comparisons of universal properties.

A linearly subunary multicategory with $\times,1,\uoc,\eechom,\mixedhom,\rtimes$, and restricted $\foc$ (or equivalently $\unit$) is equivalent to a cartesian monoidal category , a -enriched category with powers and copowers, and an object $\unit\in\cL$.

<ref> implies exactly this characterization except that instead of $\unit$ we have a -enriched adjunction $\foc : \cE \toot \cL: \uoc$.
But this is uniquely determined by $\foc 1 \cong \unit$, since $\foc X \cong X \rtimes \unit$ and $\uoc A \cong \unit \eechom A$.

As before, the arity restrictions can be enforced by slicing: if $\mathsc{cbpv}$ is the subterminal with one nonlinear object, one linear object, all nonlinear homsets and co-unary subunary linear homsets singletons, and others empty, then the linearly subunary multicategories constitute the slice $\lnlpoly/\mathsc{cbpv}$.

By adding appropriate combinations of universal properties, we obtain various related structures in the literature.
Thus we have the following locally full sub-2-categories of :

* CBPV pre-structures, as in <ref>.

* CBPV adjunction models or EC+ models [15], which are CBPV pre-structures having $\uoc,\mixedhom$, and $\foc,+,\varnothing,\with,\top$ with restricted universal properties.

* EEC+ models [15], which are EC+ models having also $\to,\eechom,\rtimes$ as well as $\oplus,0$ with restricted universal properties.
Thus they are structures as in <ref> where and both have finite products and coproducts.

* MLJ$^\eta_p$ models [11], which are CBPV pre-structures having only $\uoc,\mixedhom$, and restricted $\foc$.

* LJ$^\eta_p$ models, which are MLJ$^\eta_p$ models having also restricted $+,\varnothing,\with,\top$.

* ECBV models [36], which are co-unary and linearly unary polycategories (that is, all linear morphisms have linear domain and codomain of length exactly 1) having $\times,1,\eechom,\rtimes$, but no $\foc$ or $\uoc$.
Of course, this arity restriction is given by slicing over a different object $\mathsc{ecbv}$.

We now consider the “classical” case: polycategories that are not co-unary.

An polycategory in which the modality $\foc$ exists is uniquely determined by a functor of symmetric multicategories

\[ \foc : \Pnonlin \to \Umulti(\Plin) \]

where $\Pnonlin$ is a cartesian multicategory, $\Plin$ a symmetric polycategory, and $\Umulti$ denotes the underlying symmetric multicategory of a symmetric polycategory.  Also:

* The modality $\uoc$ also exists if and only if the functor $\foc$ has a right adjoint $\Umulti(\Plin) \to \Pnonlin$ in the 2-category of symmetric multicategories.

* If $\times,1,\ten,\unit,\coten,\counit$ exist, then $\foc$ is equivalently a strong symmetric monoidal functor from a cartesian monoidal category to (the $\ten$ monoidal structure of) a symmetric linearly distributive one.

* Thus, an polycategory with $\times,1,\ten,\unit,\coten,\counit,\foc,\uoc$ is equivalently an adjunction $\cM \toot \cL$ in which is linearly distributive.
Moreover, it also has $\duals$ if and only if is $\ast$-autonomous.

Like <ref>, using the result of [13] that a symmetric polycategory with $\ten,\unit,\coten,\counit$ is equivalently a symmetric linearly distributive category.
The universal property of $\foc$ relative to linear morphisms with arbitrary codomain ensures that it is uniquely determined by its action on underlying multicategories, while $\uoc$ knows nothing about the non-co-unary morphisms at all.

Note that since $\fwn$ and $\uwn$ can be defined in terms of $\foc,\uoc,\duals$ by $\fwn X = \d{(\foc X)}$ and $\uwn A = \uoc(\d A)$, an adjunction with $\ast$-autonomous also has $\fwn,\uwn$.
Thus, we have the following locally full sub-2-categories of :

* Linearly distributive adjunctions and $\ast$-autonomous adjunctions, defined as in <ref><ref>.

* Linearly distributive adjunctions with any desired limits and colimits in either category, subject to the restrictions that colimits must be preserved by the product or tensor product in each variable, and limits in the linearly distributive category must be preserved by the cotensor product in each variable.

* $\ast$-autonomous closed adjunctions with any desired limits and colimits in either category.

On the other hand, if we add $\fwn$ and $\uwn$ without $\duals$, the induced structure on is also one that appears in the literature:

If is an polycategory with $\ten,\unit,\coten,\counit,\foc,\uoc,\fwn,\uwn$, then $\Plin$ is a (symmetric) linearly distributive category with storage [6].

Note that any polycategory has an underlying multicategory $\coun\cP$ containing all the objects, all the nonlinear morphisms, but only the co-unary linear morphisms.
It also has a linear opposite $\cP\lop$ in which the nonlinear morphisms are the same, but $\linhom{\cP\lop}(\Theta|\Gamma;\Delta) = \linhom{\cP}(\Theta|\Delta;\Gamma)$.

Thus, applying <ref> to $\coun\cP$ and $\coun{\cP\lop}$, we obtain a linear exponential comonad $\oc=\foc\uoc$ and a linear exponential monad $\wn = \fwn\uwn$, so it remains only to show that $\wn$ is a $\oc$-strong monad and dually.
We obtain the morphism $\wn A \ten \oc B \to \wn (A\ten \oc B)$ by acting on the $\uwn$-universal morphism of $(\uwn(A\ten \foc\uoc B)\mid \,) \to A\ten \foc\uoc B$ as follows.

((AB) | AB ; )
((AB) | A, B ; )

((AB), B | A ; )

((AB), B ; A)

→        ((AB), B|A ; )

(|A, B; (AB))

(|A B; (AB))

=         (|A B ; (AB)).

The noninvertible map above is composition with the $\fwn$-universal $(\uwn A \mid \fwn \uwn A) \to ()$.
It is straightforward to check the axioms.
(This is like the proof in <cit.> that proof nets with storage boxes form a linearly distributive category with storage.)

The converse of <ref> is subtler.
If is a symmetric linearly distributive category with storage, then it is in particular a symmetric monoidal category (under $\ten,\unit$) with a linear exponential comonad $\oc$.
Therefore, it gives rise to an adjunction $\cM\toot\cL$ as above, where is the Eilenberg–Moore category of the comonad $\oc$.
Hence, by <ref>, any subcategory of this (such as the Kleisli category) yields an polycategory with $\Plin = \cL$ and having $\ten,\unit,\coten,\counit,\foc,\uoc$.
Similarly, any subcategory of the the opposite of the Eilenberg–Moore category of the monad $\wn$ yields an polycategory with $\Plin=\cL$ and having $\ten,\unit,\coten,\counit,\fwn,\uwn$.

If has duals, hence is $\ast$-autonomous, then by <cit.> the modalities $\oc$ and $\wn$ are dual, in that $\wn A \cong \d{(\oc(\d A))}$.
This implies that their Eilenberg–Moore and Kleisli categories are dual to each other, by equivalences that lie over the self-duality $\duals$; hence these two polycategories coincide and
are a $\ast$-autonomous adjunction that induces the given $\oc$ and $\wn$.
However, if does not have duals, then the Eilenberg-Moore categories of $\oc$ and $\wn$ need not be dual:

Let be a distributive lattice that is not a Boolean algebra.
As in [13], we can regard as a linearly distributive category with $\mathord{\ten}=\mathord{\wedge}$ and $\mathord{\coten}=\mathord{\vee}$.
Since $\wedge$ is the cartesian product and $\vee$ the cartesian coproduct, we can equip with storage modalities $\oc$ and $\wn$ that are both just the identity.
(Thanks to Robin Cockett for pointing out this example.)
The Eilenberg–Moore categories of this $\oc$ and $\wn$ are then both just $\cL$ itself, which may not be self-dual.

In fact this cannot occur as $\Plin$ for any polycategory with $\foc,\uoc,\fwn,\uwn$ such that its (identity) modalities $\oc$ and $\wn$ are recovered as $\foc\uoc$ and $\fwn\uwn$ respectively.
To see this, note that for any nonlinear object $X$ in an polycategory, if $\foc X$ and $\fwn X$ both exist, then they are dual to each other.
Thus, if $\foc,\fwn$ both exist, then any object of the form $\foc X$ or $\fwn X$ has a dual — and hence if $\oc = \foc\uoc$ is the identity, then every object has a dual.
But this would imply that is a Boolean algebra.

Thus, if we want to embed a general linearly distributive category with storage into an polycategory, we have to give up on having all $\foc,\uoc,\fwn,\uwn$.
But we can get away with something slightly less:

A linearly distributive category admits storage modalities if and only if it can occur as $\Plin$ for an polycategory having $\ten,\unit,\coten,\counit,\uoc,\uwn$ along with $\foc$ defined on the image of $\uoc$ and $\fwn$ defined on the image of $\uwn$.

For “if”, just note that the proof of <ref> uses only this weaker hypothesis.
For “only if”, let be a symmetric linearly distributive category with storage, and define an polycategory $\bkll$ as follows.
Its linear objects are the objects of , while its nonlinear objects consist of two copies of the objects of denoted $A^\oc$ and $A^\wn$.
Its homsets are defined by:

\begin{multline*}
\linhom{\bkll}(A_1^\oc,\dots,A_p^\oc,B_1^\wn,\dots,B_q^\wn | C_1,\dots,C_m ; D_1,\dots, D_n)\\
= \cL(\oc A_1\ten \cdots \ten \oc A_p \ten C_1\ten\cdots \ten C_m\,,\, \wn B_1 \coten \cdots \coten \wn B_q \coten D_1 \coten\cdots\coten D_n)
\end{multline*}

\begin{align*}
\nonlinhom{\bkll}(A_1^\oc,\dots,A_p^\oc,B_1^\wn,\dots,B_q^\wn  ; C^\oc )
&= \cL(\oc A_1\ten \cdots \ten \oc A_p\,,\, \wn B_1 \coten \cdots \coten \wn B_q \coten C)\\
\nonlinhom{\bkll}(A_1^\oc,\dots,A_p^\oc,B_1^\wn,\dots,B_q^\wn  ; C^\wn )
&= \cL(\oc A_1\ten \cdots \ten \oc A_p\ten C\,,\, \wn B_1 \coten \cdots \coten \wn B_q)
\end{align*}

In particular, we have

(A^; C^)    = (A, C)        (A^; C^)    = (AC, )

(B^; C^)    = (C, B)        (B^; C^)    = (, B C).

That is, the category of nonlinear objects and unary morphisms consists of a copy of the Kleisli category of $\oc$ (the objects $A^\oc$) and a copy of the opposite of the Kleisli category of $\wn$ (the objects $B^\wn$), with the morphisms between the two defined in a twisted way using the linearly distributive structure.

Composition of two linear morphisms is defined just as in the ordinary symmetric polycategory underlying .
To compose a nonlinear morphism with either a linear or nonlinear morphism, we make use of the “generalized Kleisli lift”: given

\[ f : \oc A_1\ten \cdots \ten \oc A_p \too \wn B_1 \coten \cdots \coten \wn B_q \coten C \]

we can construct the composite

\begin{align*}
\oc A_1\ten \cdots \ten \oc A_p
&\to \oc \oc A_1\ten \cdots \ten \oc \oc A_p\\
&\to \oc (\oc A_1\ten \cdots \ten \oc A_p)\\
&\xto{\oc f} \oc(\wn B_1 \coten \cdots \coten \wn B_q \coten C)\\
&\to \wn B_1 \coten \cdots \coten \wn B_q \coten \oc C
\end{align*}

where the first map is composed of the comultiplications $\oc A_i \to \oc\oc A_i$ of $\oc$, the second map is the lax monoidal structure of $\oc$, the third in $\oc f$, and the fourth is $q$ applications of the strength $\oc(\wn B \coten C ) \to \wn B \coten \oc C$.
By first applying this construction to a nonlinear morphism with codomain $C^\oc$, or the dual construction to one with codomain $C^\wn$, we can then compose it along this object with any other morphism as usual in the underlying polycategory of .

Of course this polycategory has $\ten,\unit,\coten,\counit$.
By construction it has $\uoc A = A^\oc$ and $\uwn A = A^\wn$, and partially defined $\foc A^\oc = \oc A$ and $\fwn A^\wn = \wn A$.
Note that this is very similar to the proof in <cit.> that proof nets with storage are sound for linearly distributive categories with storage.

This “double Kleisli category” construction is functorial, and lands inside the slice category $\lnlpoly/\mathsc{dblsplit}$ from <ref>.
Moreover, if is $\ast$-autonomous, then $A^\wn \cong (\d{A})^\oc$ in $\nonlin{(\bkll)}$.
Thus in this case $\bkll$ is equivalent (though not isomorphic) to the Kleisli adjunction of $\oc$ and also to the Kleisli adjunction of $\wn$.

This gives us the following locally full sub-2-categories of :

* Linearly distributive categories with storage.

* $\ast$-autonomous categories with storage.

* Linearly distributive or $\ast$-autonomous categories with storage, any desired colimits preserved by the tensor product in each variable, and any desired limits preserved by the cotensor product in each variable.

§ UNIFYING UNIVERSALITY

In defining doctrines, we will want to work generally with classes of universal arrows and colimits in polycategories.
Unfortunately, the different kinds of objects and morphisms in an polycategory make such a general treatment quite cumbersome.
For instance, we already saw in <ref> that there are formally five different kinds of “universal morphism” in an polycategory, which has the consequence that a fully formal proof of <ref> (universal morphisms compose) would have on the order of 25 different cases to consider.[Not exactly 25, of course, since some pairs of universal morphisms will not be composable.]
Similarly, there are four different kinds of limits and colimits, and so on.
We can't even use duality to simplify the situation, since an polycategory does not have an “opposite” polycategory.
Nevertheless, there is a clear intuition that this technical multiplicity is in some sense “inessential”: all the cases behave similarly.
In this section we give an alternative definition of polycategories that enables us to formally unify these cases.

Given a set of objects partitioned into linear and nonlinear ones, by a signed object we mean an object together with an element of $\{-,+\}$, written $R^+$ or $R^-$, where $R$ is a (linear or nonlinear) object.
We denote general signed objects by letters towards the middle of the Roman alphabet such as $K,L,M,\dots$, and lists of signed objects by the Greek letters $\Phi,\Psi$.
If $K$ is a signed object we write $K\D$ for the result of flipping its sign: $(R^+)\D = R^-$ and $(R^-)\D = R^+$.

A list of signed objects is admissible if

* it contains at most one positive nonlinear object, and

* if it does contain one such, then it contains no linear objects.

If $(\Phi,K)$ and $(K\D,\Psi)$ are admissible, so is $(\Phi,\Psi)$.

If a positive nonlinear object $X^+$ appears in $\Phi$, then $K$ and all other objects in $\Phi$ must be negative nonlinear.
Hence $K\D$ is positive nonlinear, so all objects in $\Psi$ are also negative nonlinear.
We can argue similarly if $\Psi$ contains $X^+$.

By a structural map we mean a morphism $\si : (K_1,\dots, K_m)\to (K_{\si 1},\dots, K_{\si n})$ where $(K_1,\dots, K_m)$ is a list of signed objects and $\si : \{1,\dots,n\} \to \{1,\dots,m\}$ is a function with the property that for any $j$ with $1\le j\le m$, if $|\si^{-1}(j)|\neq 1$ then $K_j$ is negative and nonlinear.

An entries-only polycategory consists of:

* A set of objects partitioned into linear and nonlinear ones.

* For any admissible list of signed objects $(K_1,\dots,K_n)$, a hom-set $\cP(K_1,\dots,K_n)$, with functorial actions $\cP(\Psi)\to\cP(\Phi)$ by structural maps $\si : \Phi\to\Psi$.

* For any object $R$ (linear or nonlinear), an identity $1_R \in \cP(R^-,R^+)$.

* Whenever $(\Phi,K)$ and $(K\D,\Psi)$ are admissible, a composition map

\[ \circ_K : \cP(K\D,\Psi)\times \cP(\Phi,K) \to \cP(\Phi,\Psi) \]

that is associative, unital, and equivariant with respect to the structural actions and permutations that swap the two inputs.

A functor between entries-only polycategories consists of functions between their linear and nonlinear objects and morphisms, preserving entries, structural actions, identities, and composites.

The category of entries-only polycategory is equivalent to that of polycategories.

By structural permutations, the hom-sets of an entries-only polycategory are uniquely determined (up to isomorphism) by those of the form

\begin{gather*}
\cP(X_1^-,\dots,X_m^-,Y^+) \\
\cP(X_1^-,\dots,X_m^-,A_1^-,\dots,A_n^-,B_1^+,\dots,B_p^+)
\end{gather*}

for nonlinear objects $X_i,Y$ and linear objects $A_j,B_k$.
We can identify these with the hom-sets

\begin{gather*}
\Pnl(X_1,\dots,X_m;Y) \\
\Pl(X_1,\dots,X_m|A_1,\dots,A_n;B_1,\dots,B_p)
\end{gather*}

in an ordinary polycategory, and the identities, compositions, and structural actions correspond.

Henceforth, we will pass freely back and forth between the two definitions, using whichever notation for homsets is more convenient.
We can now define a general notion of universal morphism that encompasses all five cases described in <ref>.

A morphism $f\in \cP(\Phi,K)$ in an entries-only polycategory is universal in $K$ if for any list of signed objects $\Psi$ such that $(K\D,\Psi)$ is admissible, the composition map $(-\circ_K f) : \cP(K\D,\Psi) \to \cP(\Phi,\Psi)$ is bijective, i.e. for any $h\in \cP(\Phi,\Psi)$ there exists a unique $g\in \cP(K\D,\Psi)$ such that $g\circ_K f = h$.

In fact, following [20, 32, 10], it is useful to generalize from universal morphisms in one multi- or poly-category to cartesian ones relative to a functor.

Given a functor $\pi:\cP\to\cQ$ of entries-only polycategories, a morphism $f\in \cP(\Phi,K)$ is $\pi$-cartesian in $K$ if for any list of signed objects $\Psi$ of such that $(K\D,\Psi)$ is admissible, the following square is a pullback:

\begin{equation}
\begin{tikzcd}[column sep=huge]
\cP(K\D,\Psi) \ar[r,"-\circ_K f"] \ar[d,"\pi"'] & \cP(\Phi,\Psi) \ar[d,"\pi"]\\
\cQ(\pi K\D, \pi\Psi) \ar[r,"-\circ_{(\pi K)} (\pi f)"'] & \cQ(\pi\Phi,\pi\Psi)
\end{tikzcd}\label{eq:cartesian}
\end{equation}

In other words, for any $h\in \cP(\Phi,\Psi)$ and $\ell\in \cP(\pi K\D,\pi \Psi)$ such that $\ell \circ_{\pi K} \pi f = \pi h$, there exists a unique $g\in \cP(K\D,\Psi)$ such that $g\circ_K f = h$ and $\pi g = \ell$.

Note that if $\cQ$ is terminal, both sets on the bottom row of (<ref>) are singletons; so the square is a pullback just when the morphism on top is a bijection.
Thus, $f$ is universal in $K$ precisely when it is $\pi$-cartesian in $K$ for the unique functor $\pi : \cP\to \mathsc{lnlpoly}$ to the terminal object.

Cartesian morphisms specialize to various notions in the literature:

* For symmetric multicategories, cartesian morphisms with $K$ positive specialize to the “strongly cocartesian” morphisms of <cit.>.

* For cartesian multicategories, cartesian morphisms specialize to the cartesian and opcartesian morphisms of [32].

* For symmetric polycategories, cartesian morphisms specialize to the cartesian and opcartesian morphisms of [10].

* For categories, cartesian morphisms specialize to the traditional notion of cartesian and opcartesian morphism.

Cartesian morphisms can express restricted universal properties.
For instance, in <ref> let $\cQ = \mathsc{cbpv}$, and let $f\in \cP(X^-,A^+)$ for a nonlinear $X$ and linear $A$, with vertex $K = A^+$.
Then the hom-set $\cQ(\pi K\D,\pi\Psi)$ is empty unless $\Psi$ contains exactly one positive linear object and the rest nonlinear.
Thus, $f$ is cartesian just when it exhibits $A$ as $\foc X$ with the universal property of (<ref>).

Cartesian morphisms can also express adjunctions that behave similarly to $\foc\adj\uoc$ but stay inside the linear or nonlinear world.
For instance, let $\mathsc{smadj}$ be the multicategory with two objects $\mathsc{p},\mathsc{n}$, both linear, a unique morphism $\Gamma \to \mathsc{p}$ when $\Gamma$ consists entirely of $\mathsc{p}$'s, and a unique morphism $\Gamma \to \mathsc{n}$ for any $\Gamma$.
Then an object of $\lnlpoly/\mathsc{smadj}$ is a symmetric multicategory with a partition of its objects into “positive” and “negative” ones, such that any morphism with a negative object in its domain has a negative codomain.
By an argument like that of <ref>, if it has cartesian liftings in both directions along the morphism $\mathsc{p}\to \mathsc{n}$ in $\mathsc{smadj}$, then it is uniquely determined by an adjunction of symmetric multicategories.
Further cartesian liftings can specialize this to an adjunction of symmetric monoidal categories, with strong left adjoint and lax right adjoint.

As an example of the value of the entries-only framework, we can now prove (a generalization of) <ref> without a division into 25-odd cases:

Given $\pi:\cP\to\cQ$, if $f\in \cP(\Phi_1,K)$ is $\pi$-cartesian in $K$ and $g\in\cP(K\D,\Phi_2,L)$ is $\pi$-cartesian in $L$, then their composite $g\circ_K f\in \cP(\Phi_1,\Phi_2,L)$ is $\pi$-cartesian in $L$.

In the following diagram:

\[
\begin{tikzcd}[column sep=huge]
\cP(L\D,\Psi) \ar[r,"-\circ_L g"] \ar[d,"\pi"'] &
\cP(K\D,\Phi_2,\Psi) \ar[r,"-\circ_K f"] \ar[d,"\pi"'] &
\cP(\Phi_1,\Phi_2,\Psi) \ar[d,"\pi"]\\
\cQ(\pi L\D, \pi\Psi) \ar[r,"-\circ_{(\pi L)} (\pi g)"'] &
\cQ(\pi K\D,\pi\Phi_2,\pi\Psi) \ar[r,"-\circ_{(\pi K)} (\pi f)"'] &
\cQ(\pi \Phi_1,\pi\Phi_2,\pi\Psi)
\end{tikzcd}
\]

both squares are pullbacks since $f$ and $g$ are $\pi$-cartesian, hence so is the rectangle.

Following [32, 10], we define:

A functor $\pi:\cP\to\cQ$ is a bifibration if for any list $\Phi$ of signed objects in and any morphism $g\in \cQ(\pi\Phi,L)$ there exists a $\pi$-cartesian morphism $f\in \cP(\Phi,K)$ such that $\pi(f) = g$.

When $\cQ$ is one of our distinguished subterminal objects (including the terminal object $\mathsc{lnlpoly}$), bifibrations $\pi:\cP\to\cQ$ reduce to more familiar structures:

Subterminal $\cS$     Universal properties     Equivalent structure
$\mathsc{lnlpoly}$     $\times,1,\to,\ten,\unit,\duals,\foc,\uoc$     $\ast$-autonomous closed adjunction
$\mathsc{lnlmulti}$     $\times,1,\to,\ten,\unit,\hom,\foc,\uoc$     closed adjunction
$\mathsc{sympoly}$     $\ten,\unit,\duals$     $\ast$-autonomous category
$\mathsc{symmulti}$     $\ten,\unit,\hom$     closed symmetric monoidal category
$\mathsc{cartmulti}$     $\times,1,\to$     cartesian closed category
$\mathsc{cbpv}$     $\times,1,\to,\mixedhom,\eechom,\rtimes,\unit^\dagger,\foc^\dagger,\uoc$     structure of <ref>

$^\dagger$ with restricted universal property.

Bifibrations over subterminals

For each row in <ref>, with subterminal object $\cS$ listed in the first column, the following structures are equivalent:

* A bifibration $\pi:\cP\to \cS$.

* An object of $\lnlpoly/\cS$ with the universal properties in the second column.

* The categorical structure indicated in the third column.

Clearly <ref>$\Rightarrow$<ref>, while <ref>$\Leftrightarrow$<ref> follows from <ref>.
The remaining direction <ref>$\Rightarrow$<ref> is similar to the universal characterization of $\ast$-autonomous categories in [10].
By $\bigtimes\Theta$, $\bigotimes\Gamma$, or $\bigparr\Delta$ we mean the result of combining all the objects in a list with the given binary operation; if the list contains only one object the result is that object (in which case the binary operation doesn't even need to exist), while if the list is empty the result is the corresponding nullary operation $1$, $\unit$, or $\counit$.
Now we construct the five possible types of morphism universal in $X$ or $A$ as follows:

* For $\psi\in\Pnl(\Theta;X)$ we take $X = \bigtimes \Theta$.

* For $\psi\in\Pnl(\Theta,X;Y)$ we take $X = \bigtimes\Theta\to Y$.

* For $\psi \in \Pl(\Theta,X|\Gamma;\Delta)$ we take $X = \bigtimes\Theta \to (\bigotimes\Gamma\eechom \bigparr\Delta)$.

* For $\psi \in \Pl(\Theta|\Gamma;\Delta,A)$ we take $A = \bigtimes\Theta \rtimes \bigotimes (\Gamma,\d\Delta)$.

* For $\psi \in \Pl(\Theta|\Gamma,A;\Delta)$ we take $A = \bigtimes\Theta \mixedhom \bigparr(\d\Gamma,\Delta)$.

We leave it to the reader to check that whenever a particular type of universal morphism exists in one of our subterminals $\cS$, the requisite universal operations are among those assumed by <ref> or can be constructed from them.
(When $\cS = \mathsc{cbpv}$, we discussed the restricted universal property of $\foc$ in <ref>.)

We refer to a bifibration over a subterminal as birepresentable.
For instance, a birepresentable polycategory is a $\ast$-autonomous closed adjunction, a birepresentable polycategory is a $\ast$-autonomous category, a birepresentable cartesian multicategory is a cartesian closed category, and so on.[In the literature, sometimes “representable” means only that “covariant” universal arrows exist, e.g. a “representable symmetric multicategory” is a not-necessarily-closed symmetric monoidal category.  But other times it means that all universal arrows exist, e.g. a “representable polycategory” is a $\ast$-autonomous category.  Our “birepresentable”, in analogy to “bifibration”, avoids ambiguity.]

Similarly, we can define a general notion of limit that encompasses all four cases.
In fact, we can define a general notion that encompasses both universal morphisms and (weighted) limits and colimits!

An abstract cone is a small entries-only polycategory $\cC$ equipped with a specified signed object $K$ called the vertex, such that $\cC(\Phi)$ is empty if $\Phi$ contains any copies of $K\D$ or contains more than one copy of $K$, except that $\cC(K\D,K)=\{1_K\}$.
Nonidentity morphisms containing $K$ (necessarily exactly once) are called abstract projections, while morphisms not containing $K$ are called abstract transitions.
Note that no two abstract projections can be composable.
The reduct of an abstract cone is its subcategory $\cC'$ obtained by removing the underlying object of $K$, its identity morphism, and all the abstract projections.

An expansion of an abstract cone is determined by a finite number of new objects (each linear or nonlinear) and a sign for each of them, yielding a signed list $\Omega$, such that $(K\D,\Omega)$ is admissible.
The expansion itself is an entries-only polycategory $\cC_\Omega$ (which is not itself an abstract cone) obtained by adding the new objects to along with one new morphism $\ftil\in \cC_\Omega(\Phi,\Omega)$ for each abstract projection $f\in \cC(\Phi,K)$, called the expanders, and an additional new morphism $\chi \in \cC_\Omega(K\D,\Omega)$ called the factorization.
Composition is defined by $\chi \circ_K f = \ftil$, and by $\ftil \circ g = \widetilde{f\circ g}$ when $g$ is an abstract transition.
The corresponding pre-expansion is the subcategory $\cC_\Omega'\subseteq \cC_\Omega$ obtained by omitting the morphism $\chi$.

By a concrete cone we mean a functor whose domain is an abstract cone.
Let $\pi :\cP\to \cQ$ a functor of (entries-only) polycategories, and $G:\cC\to \cP$ a concrete cone.
We say that $G$ is $\pi$-extremal if for any expansion $\cC_\Omega$ of , any commutative square as shown below such that the composite $\cC\to\cC_\Omega'\to\cP$ is $G$ has a unique diagonal filler.

\[
\begin{tikzcd}
\cC \ar[r] \ar[rr,bend left,"G"] & \cC_\Omega' \ar[r] \ar[d] & \cP \ar[d,"\pi"] \\
& \cC_\Omega \ar[r] \ar[ur,dashed,"\exists!"] & \cQ
\end{tikzcd}
\]

If $\cQ=\mathsc{lnlpoly}$ is terminal, instead of $\pi$-extremal we say that $G$ is universal.

The most important examples of extremal cones are the following, which show that the notion includes both cartesian/universal morphisms and limits and colimits.

Given a finite list of abstract objects, each linear or nonlinear and with a chosen sign, and with one of these signed objects $K$ distinguished and the remaining signed list denoted $\Phi$, there is an abstract cone with precisely these objects and precisely one nonidentity morphism $f\in \cC(\Phi,K)$, with $K$ the vertex.
Then a concrete cone $G:\cC\to \cP$ picks out a single morphism in , and it is $\pi$-extremal for some $\pi$ precisely when that morphism is $\pi$-cartesian in $K$.

Given a small category , we define an abstract cone as follows.
It has no nonlinear objects, and its linear objects are the objects of $\cA$ together with an additional one $B$.
Each morphism $f\in \cA(A_1,A_2)$ yields a morphism $\fhat\in \cC(A_1^-,A_2^+)$, and for each object $A\in \cA$ we add a morphism $p_A \in \cC(A^-,B^+)$, with composition defined by $p_{A_2} \circ_{A_2} \fhat = p_{A_1}$.
The vertex is $B^+$.
Then a concrete cone $G:\cC \to \cP$ is just a cocone under an -shaped diagram in the ordinary category of linear objects of , and it is universal precisely when that cocone is a colimit.
This includes the strong universal property discussed in <ref>, since the signed objects added in an expansion $\cC_\Omega$ may be linear or nonlinear and positive or negative.
Similarly, we can characterize limits of linear objects, and limits and colimits of nonlinear objects.

If $H:\cC\to\cQ$ is a concrete cone, we say that $\pi:\cP\to\cQ$ has extremal lifts of $H$ if for any lift $G:\cC'\to \cP$ of the reduct of $\cC$ to $\cP$, there exists a compatible lift of $H$ that is $\pi$-extremal:

\[
\begin{tikzcd}[column sep=large]
\cC' \ar[r,"G"] \ar[d] & \cP \ar[d,"\pi"]\\
\cC \ar[r,"H"'] \ar[ur,dashed,"\pi\text{-}\mathrm{ext}" description] & \cQ
\end{tikzcd}
\]

If $\cQ$ is terminal, we say that has universal -cones.

For instance, $\pi$ is a bifibration if and only if it has extremal lifts of all the abstract cones from <ref>.
Thus, is birepresentable if and only if it has universal -cones for all these abstract cones.

We say that $\pi:\cP\to\cQ$ is relatively bicomplete if it has extremal lifts of all the cones from <ref> (where is small).
If is terminal, we say that is bicomplete.

An polycategory has all small limits and colimits of both kinds of objects, in the sense described in <ref>, if and only if it is bicomplete in the sense of <ref>.

As noted in <ref>, an multicategory cannot have a terminal linear object or an initial linear or nonlinear object when considered as an polycategory.
However, while a concrete cone $G:\cC\to\cP$ of such a shape in an multicategory cannot be universal, it can be $\pi$-extremal for the unique functor $\pi:\cP\to\mathsc{lnlmulti}$ (see <ref>).
This yields the correct “modified” notion of initial and terminal object in an multicategory as discussed in <ref>, since not all expansions of this cone factor through $\mathsc{lnlmulti}$.
Similar remarks apply to symmetric polycategories, cartesian multicategories, symmetric multicategories, and CBPV pre-structures.

While our general notion of “extremal cone” also includes examples that don't fall into either <ref> or <ref>, our main purpose in introducing it is to give a common language to talk about these two examples.
To this end, we note that together these two examples suffice to reconstruct all universal cones.

For any functor $\pi:\cP\to\cQ$, the following are equivalent.

* is a relatively bicomplete bifibration.

* has an extremal lift of any cone $H:\cC\to\cQ$.

<ref> show that <ref>$\Rightarrow$<ref>.
So let us assume <ref> and let $H:\cC\to\cQ$ be a cone and $G:\cC'\to \cP$ a lift of its reduct to .
For any abstract projection $f\in \cC(\Phi,K)$, let $\ftil\in\cP(G\Phi,K_f)$ be $\pi$-extremal in $K_f$ and such that $\pi(\ftil) = H(f)$ and hence $\pi(K_f) = H(K)$, where the sign and linearity of $K_f$ are the same as that of $K$.
Such a morphism exists because $\pi$ is a bifibration.

Now for any abstract transition $g\in \cC(\Psi,L)$ and any abstract projection $f\in \cC(L\D,\Phi,K)$ that it is composable with, producing an abstract projection $f\circ_L g \in \cC(\Psi,\Phi,K)$, the composite $\ftil \circ G g \in \cP(G\Psi,G\Phi,K_f)$ satisfies

\[\pi(\ftil\circ G g) = \pi(\ftil) \circ \pi(G g) = H(f) \circ H(g) = H(f\circ g) .\]

Thus, by the universal property of $\widetilde{f\circ_L g} \in \cP(G\Psi,G\Phi,K_{f\circ_L g})$ it induces a unique morphism $\gtil \in \cP(K_{f\circ_L g}\D,K_f)$ such that $\pi(\gtil) = 1_K$.

Now these objects $K_f$ and morphisms $\gtil$ form a small diagram of objects of (linear or nonlinear according as $K$ is such) lying in the fiber over $K$.
In particular, therefore, the image of this diagram under $\pi$ admits a specified cone (if $K$ is negative) or cocone (if $K$ is positive) with vertex $H(K)$, consisting entirely of identity maps.
Thus, since $\pi$ is relatively bicomplete, this cone of identity maps has a $\pi$-extremal lift.
Composing the projections of this lift with the morphisms $\ftil$ yields a $\pi$-extremal concrete cone $\cC\to\cP$ extending $G$ and lifting $H$.

Of course, there are analogous results in which set-theoretic size of the limits and colimits and of the abstract cones are limited in chosen ways.
We also have a version of <ref> and its converse.

Given $\pi:\cP\to\cQ$ and an abstract cone with vertex $K$, if $F,G:\cC \to \cP$ coincide on the reduct $\cC'$ and are both $\pi$-extremal, then there is a unique isomorphism $\phi:F(K) \cong G(K)$ such that $\pi(\phi)$ is an identity and such that $\phi \circ_K F(f) = G(f)$ for all abstract projections $f$ in .

Given $\pi:\cP\to\cQ$, an abstract cone with vertex $K$, a concrete cone $G:\cC\to \cP$, and an isomorphism $\phi:G(K) \cong K'$, there is a concrete cone $G_\phi : \cC\to \cP $ that agrees with $G$ on the reduct $\cC'$, sends the vertex to $K'$, and the abstract projections $f$ to $G_\phi(f) = \phi\circ G(f)$.

If in the above construction $G$ is $\pi$-extremal, so is $G_\phi$.

And a composition property for functors:

Suppose $\pi_1:\cP_1\to \cP_2$ and $\pi_2:\cP_2\to\cP_3$, and a concrete cone $G:\cC\to \cP_1$.
If $G$ is $\pi_1$-extremal and $\pi_1G$ is $\pi_2$-extremal, then $G$ is $\pi_2\pi_1$-extremal.

In the following diagram:

\[
\begin{tikzcd}
\cC \ar[r] \ar[rr,bend left,"G"] & \cC_\Omega' \ar[r] \ar[dd] & \cP_1 \ar[d,"\pi_1"] \\
& & \cP_2 \ar[d,"\pi_2"] \\
& \cC_\Omega \ar[r] \ar[uur,dashed,"\exists!"] \ar[ur,dashed,"\exists!"'] & \cP_3
\end{tikzcd}
\]

to find a unique lift in the rectangle, we first find a unique lower diagonal lift and then a unique upper one.

§ DOCTRINES AND SKETCHES

In <ref> we encountered a long list of categorical structures that form locally full sub-2-categories of .
In this section and the next we will define a general class of such sub-2-categories, which we call (sorted, ) doctrines.
Inspecting the examples in <ref>, we see that each is characterized by three kinds of data:

* Restrictions on the kinds of objects (e.g. no nonlinear objects) and the arities of morphisms (e.g. all linear morphisms are co-unary).
We have already remarked that these restrictions can be detected by slicing over subterminals such as $\mathsc{symmulti}$, $\mathsc{cbpv}$, etc.
More generally, we can equip the objects or morphisms with structure by slicing over a non-subterminal object, such as $\mathsc{plmulti}$, $\mathsc{dblsplit}$, and $\mathsc{smadj}$ in <ref>.

* Existence of universal cones, for all cones in some family (e.g. existence of tensors, internal-homs, modalities, or limits or colimits).

Sometimes the universal property of these cones has to be restricted to respect the allowed arities of morphisms, which corresponds to asking for cartesian lifts over the base objects in <ref>.

* Requirements that certain adjunctions are of some “Kleisli type”, hence determined by a monad, a comonad, or both.

In this section we define doctrines, which encapsulate <ref> and <ref>.
In the next section we extend these to “sorted doctrines” that incorporate <ref> as well.

An doctrine $\dD$ is an polycategory $\abs{\dD}$ equipped with a family of concrete cones $G:\cC\to\abs{\dD}$, called the -cones.
We say is small if $\abs{\dD}$ is small and the family of cones is also small.

Given such a doctrine, a -category is an polycategory equipped with a functor $\pi:\cP\to\abs{\dD}$ that has extremal lifts of all -cones:

\[
\begin{tikzcd}[column sep=large]
\cC' \ar[r] \ar[d] & \cP \ar[d,"\pi"] \\
\cC \ar[r,"G"'] \ar[ur,dashed,"\exists","\pi\text{-ext}"'] & \abs{\dD}
\end{tikzcd}
\]

A -functor between -categories is a morphism in $\lnlpoly/\abs{\dD}$ that preserves $\pi$-extremal lifts of -cones, and a -transformation between -functors is a 2-cell in $\lnlpoly/\abs{\dD}$.
This defines a locally full sub-2-category $\dcat\subseteq \lnlpoly$.

Let $\abs{\dD} = \mathsc{lnlpoly}$ be terminal, and let the -cones contain one representative from each isomorphism class constructed in <ref>.
Then by <ref>, a -category is a birepresentable polycategory.

Similarly, if $\abs{\dD}=\mathsc{lnlpoly}$ and the -cones contain one representative of each isomorphism class of cones, by <ref> a -category is a bicomplete birepresentable polycategory.
(Note that this doctrine is not small.)
We can include more restricted classes of limits as well by combining the cones from <ref> with some of those from <ref>; e.g. there is a (small) doctrine for birepresentable polycategories with finite products and coproducts (additives).

Taking $\abs{\dD}$ to be one of the subterminals $\mathsc{sympoly}$, $\mathsc{symmulti}$, $\mathsc{cat}$, $\mathsc{cartmulti}$, $\mathsc{lnlmulti}$ from <ref>, we can equip it with a family of cones that specify desired universal morphisms and/or limits and colimits with the appropriately restricted universal properties for the corresponding subclass of polycategories, which as noted in <ref> can be characterized by saying that certain cones are $\pi$-extremal rather than globally universal.
For instance, there is a doctrine with $\abs{\dD}=\mathsc{symmulti}$ for which the -categories are bicomplete closed symmetric monoidal categories, a doctrine with $\abs{\dD} = \mathsc{lnlmulti}$ for which the -categories are adjunctions, and so on.

Similarly, taking $\abs{\dD} = \mathsc{cbpv}$ or $\mathsc{ecbv}$ as in <ref>, we have doctrines for CBPV adjunction models, EEC+ models, and ECBV models.

Non-subterminal examples can incorporate further adjunctions.
For instance, based on <ref> we can formulate a doctrine for symmetric monoidal adjunctions.
By combining this idea with arity restrictions as in <ref> (CBPV structures), we obtain doctrines for models of polarized linear calculi as in [11].

Let $\mathsc{linpol}$ be the multicategory with two objects $\mathsc{p},\mathsc{n}$, both linear, a unique morphism $\Gamma \to \mathsc{p}$ when $\Gamma$ consists entirely of $\mathsc{p}$'s, and a unique morphism $\Gamma \to \mathsc{n}$ when $\Gamma$ contains no more than one $\mathsc{n}$.
If we equip it with the single-projection cones $(\mathsc{p},\mathsc{p}) \to \underline{\mathsc{p}}$ and $() \to \underline{\mathsc{p}}$ (with vertex underlined), we obtain a doctrine whose categories consist of a symmetric monoidal category , a category enriched over the Day convolution monoidal structure on $[\cE\op,\fSet]$, and an $[\cE\op,\fSet]$-enriched functor $R:\cL \to [\cE\op,\fSet]$.
As in <ref>, by adding the following cones we enforce additional universal properties:

* From $\underline{\mathsc{p}}\to\mathsc{n}$ we make $R$ land inside .

* From ${\mathsc{p}}\to\underline{\mathsc{n}}$ we give $R:\cL \to \cE$ a left adjoint.

* From $(\mathsc{p},\underline{\mathsc{n}})\to \mathsc{n}$ we give powers by representables.

* From $(\mathsc{p},{\mathsc{n}})\to \underline{\mathsc{n}}$ we give copowers by representables.

* From $(\underline{\mathsc{p}},{\mathsc{n}})\to \mathsc{n}$ we make enriched over .

In particular, with <ref> we obtain a doctrine for the IMLL$^\eta_p$ models of [11].
And if we additionally include cones for $\oplus,0$ of positive objects and $\with,\top$ of negative ones, we obtain their IMALL$^\eta_p$ models.

Now let $\mathsc{lnlpol}$ have two linear objects $\mathsc{p},\mathsc{n}$ and one nonlinear object $\mathsc{x}$, with all nonlinear homsets singletons, a unique morphism $(\Theta \mid \Gamma) \to \mathsc{p}$ if $\Gamma$ consists entirely of $\mathsc{p}$'s, and a unique morphism $(\Theta\mid\Gamma) \to \mathsc{n}$ when $\Gamma$ contains no more than one $\mathsc{n}$.
With the above cones for an IMLL$^\eta_p$ model, cones for $\times,1$, and also the morphisms $\underline{\mathsc{x}}\to \mathsc{p}$ and $\mathsc{x}\to \underline{\mathsc{p}}$ representing a $\uoc$ defined on positive objects and an $\foc$ valued in positive objects,
this yields a doctrine for the IMELL$^\eta_p$ models of [11].
Adding $\oplus,0$ of positive objects, $\with,\top$ of negative ones, plus $+,\varnothing$, we obtain IMLL$^\eta_p$ models.

Note that the morphisms in $\dcat$ preserve the specified universal properties up to canonical isomorphism.
This is 2-categorically correct, but means that $\dcat$ is not well-endowed with strict limits and colimits.
Thus, following the philosophy of homotopy theory, we embed it in a larger but better-behaved category.

Given an doctrine , a -sketch is an polycategory together with a functor $\pi:\cP\to\abs{\dD}$, and for each -cone $G:\cC\to\abs{\dD}$ a set (perhaps empty) of lifts of $G$ to that we call proto-extremal:

\[
\left\{\begin{tikzcd}
& \cP \ar[d,"\pi"] \\
\cC \ar[r,"G"'] \ar[ur,dashed]  & \abs{\dD}
\end{tikzcd}\right\}.
\]

A morphism of -sketches is a functor in $\lnlpoly/\abs{\dD}$ that preserves proto-extremal cones; a transformation is an arbitrary 2-cell in $\lnlpoly/\abs{\dD}$.
This defines a 2-category $\dsketch$.

A -sketch is realized if every proto-extremal cone is in fact $\pi$-extremal.
It is saturated if whenever $H:\cC\to\cP$ is proto-extremal, where $K$ is the vertex of , and $\phi : H(K)\cong K'$ is an isomorphism in such that $\pi(\phi)$ is an identity, the cone $H_\phi : \cC\to \cP$ constructed before <ref> is also proto-extremal.
It is precomplete if for any -cone $G:\cC\to\abs{\dD}$, any lift of its reduct $\cC'\into \cC\to \abs{\dD}$ to can be extended to a proto-extremal cone:

\[
\begin{tikzcd}
\cC' \ar[r] \ar[d] & \cP \ar[d,"\pi"] \\
\cC \ar[r,"G"'] \ar[ur,dashed,"\exists","\text{p.e.}"'] & \abs{\dD}
\end{tikzcd}
\]

Finally, it is (-)complete if it is realized, saturated, and precomplete.

The 2-category of -complete sketches is equivalent, as a strict 2-category, to the 2-category $\dcat$ of -categories.

We regard a -category as a sketch by designating every $\pi$-extremal lift of a -cone as proto-extremal.
This defines a 2-functor $\dcat\to\dsketch$, which lands inside the -complete sketches (using <ref>) and is an isomorphism on hom-categories.
Moreover, precompleteness and realization make any -complete sketch into a -category, while in the presence of these properties saturation is equivalent (using <ref>) to saying that all $\pi$-extremal lifts of -cones are proto-extremal; hence the functor is essentially surjective as well.

is a complete and cocomplete strict 2-category, with limits and colimits created in .
If is small, is even locally presentable.
It is also better-endowed with adjunctions, particularly ones arising from doctrine morphisms.

Let $\dD_1,\dD_2$ be doctrines.
A doctrine map $\F:\dD_1\to\dD_2$ is a functor $\abs{\F}:\abs{\dD_1}\to\abs{\dD_2}$ together with, for each $\dD_1$-cone $G:\cC\to \abs{\dD_1}$, a $\dD_2$-cone $\cC_{\F} \to \abs{\dD_2}$ and an isomorphism of abstract cones $\cC\cong \cC_{\F}$ (preserving the vertex) making the evident square commute.

Any doctrine map $\F:\dD_1\to\dD_2$ induces a strict 2-adjunction (i.e. an adjunction of -enriched categories)

\[\ladj{\F} : \sketch{\dD_1}\toot \sketch{\dD_2} : \radj{\F}.\]

We have a 2-adjunction

\[ \ladj{\F} : \lnlpoly/\abs{\dD_1} \toot \lnlpoly/\abs{\dD_2} : \radj{\F} \]

given by composition with $\abs{\F}$ and pullback along it, so it suffices to lift this to sketches.
For the right adjoint $\radj{\F}$, we define a lift $\cC \to \radj{\F}\cP$ of some $\dD_1$-cone $\cC \to \abs{\dD_1}$ to be proto-extremal if the composite $\cC_F\cong \cC \to \radj{\F}\cP \to \cP$ is proto-extremal:

\[
\begin{tikzcd}
& \radj{\F}\cP \ar[rr] \ar[d] \drpullback && \cP \ar[d] \\
& \abs{\dD_1} \ar[rr] & {}& \abs{\dD_2} \\
\cC \ar[uur,dashed] \ar[ur] \ar[rr,"\cong",<->] && \cC_F \ar[ur] \ar[uur,dashed,crossing over]
\end{tikzcd}
\]

For the left adjoint $\ladj{\F}$, we define a lift $\cD\to \ladj{\F}\cP$ of some $\dD_2$-cone $\cD \to \abs{\dD_2}$ to be proto-extremal if the latter $\dD_2$-cone is the $F$-image of some $\dD_1$-cone $\cC \to \abs{\dD_1}$ and there is a proto-extremal lift $\cC\to \cP$ making the evident diagram commute:

\[
\begin{tikzcd}
& \cP \ar[rr,equals] \ar[d] \drpullback && \ladj{\F}\cP \ar[d] \\
& \abs{\dD_1} \ar[rr] & {}& \abs{\dD_2} \\
\cC \ar[uur,dashed] \ar[ur] \ar[rr,"\cong",<->] && \cC_F= \cD \ar[ur] \ar[uur,dashed,crossing over]
\end{tikzcd}
\]

It is straightforward to check that these constructions lift the 2-adjunction.

We really want an analogous adjunction $\cat{\dD_1} \toot \cat{\dD_2}$, but this can only be expected to be a pseudo 2-adjunction, satisfying its universal property up to equivalence.[A pseudo 2-adjunction is traditionally called a “biadjunction”, but this seems inadvisable here since we are using the prefix “bi-” with a different connotation in “bifibration” and “bicomplete”.]
We will construct this in <ref>, using the above strict 2-adjunction.

§ SORTED DOCTRINES

In <ref> we chose to represent monads and comonads as their Kleisli adjunction rather than their Eilenberg–Moore adjunction (or any other), due to <ref>.
Thus, to impose the third kind of “Kleisli type” condition mentioned in <ref>, it suffices to assert essential-surjectivity properties for some of the modalities.

An arrow-type abstract cone is determined by two signed objects $K,L$ (each linear or nonlinear).
Its vertex is $K$, and its only nonidentity morphism is an abstract projection in $\cC(L,K)$.

If a cone belonging to a doctrine is arrow-type determined by $K,L$, then by choosing extremal lifts, any -category can be equipped with a functor from the fiber over $L$ to the fiber over $K$.
This functor is contravariant if $K$ and $L$ have the same sign and covariant if they have different signs.
Of the cones from <ref> representing the basic universal properties from <ref>, $\foc,\uoc,\fwn,\uwn,\duals$ are arrow-type.

A sorted doctrine is an doctrine together with:

* A partition of the objects of $\abs{\dD}$ (which we call sorts) into primitive sorts and derived sorts.

* For each derived sort $R$, there is exactly one -cone $G_R : \cC_R \to \abs{\dD}$ whose concrete vertex $G(K)$ is $R^-$ or $R^+$, and this is an arrow-type cone whose other vertex $G(L)$ is a primitive sort.
We call it the sorting cone for $R$.

Let be a sorted doctrine and $\pi :\cS\to\abs{\dD}$ a -sketch.

* is well-sorted if for every derived sort $R$ and every object $\Rtil \in \pi^{-1}(R)$, there exists a proto-extremal lift of $G_R$ that maps the vertex to $\Rtil$.

* is strictly well-sorted if for every derived sort $R$ with corresponding primitive sort $S$, there is a specified bijection between the objects of $\pi^{-1}(R)$ and $\pi^{-1}(S)$ and, for each $\Rtil$ and $\Stil$ that correspond under this bijection, a specified proto-extremal lift of $G_R$ with entries $\Rtil$ and $\Stil$.

We write $\dscat$ for the 2-category of well-sorted -complete sketches (-categories).

Thus a -category is well-sorted if and only if the functor induced by each sorting cone is essentially surjective on objects, and strictly well-sorted if a particular choice of this functor has been made that is bijective on objects.
We are “really” interested in the strictly well-sorted sketches, but the non-strictly well-sorted ones are more convenient to work with technically.
Fortunately we have the following:

For a sorted doctrine , every well-sorted -category is equivalent in to a strictly well-sorted one.

Given a well-sorted $\pi:\cS\to\abs{\dD}$, for each derived sort $R$ with corresponding primitive sort $S$ we have an essentially surjective functor $\pi^{-1}(S) \to \pi^{-1}(R)$.
Thus, we can replace $\pi^{-1}(R)$ by an equivalent category whose objects are those of $\pi^{-1}(S)$, making the functor bijective on objects.
These equivalences on fibers extend to an equivalence of -categories.

Thus, $\dscat$ is equivalent to its subcategory of strictly well-sorted -categories.

Any doctrine can be made sorted with all sorts primitive, so that all -sketches are (vacuously) strictly well-sorted.

Let be any doctrine for which $\abs{\dD}$ has exactly one nonlinear object $\mathsc{x}$ and one linear object $\mathsc{a}$, such as $\mathsc{lnlmulti}$ or the terminal object $\mathsc{lnlpoly}$.
Suppose furthermore that the only -cone with vertex $\mathsc{x}^{\pm}$ is an arrow-type cone with vertex $\mathsc{x}^-$ and abstract projection in $\cC(\mathsc{a}^+,\mathsc{x}^-)$ (that is, a $\uoc$-cone).
Then we can make a sorted doctrine where $\mathsc{a}$ is primitive, $\mathsc{x}$ is derived, and this cone is the sorting cone.

We call this a Kleisli sorted doctrine.
Then a -category is strictly well-sorted just when it is of Kleisli type (<ref>).
If also contains $\foc$, then by <ref> this is equivalent to its being the Kleisli adjunction of the comonad $\oc = \foc\uoc$.
Thus, the 2-category of symmetric monoidal categories with a linear exponential comonad, and its variants with internal-homs and/or limits and colimits, are equivalent to for some sorted doctrine .
Similarly, by taking an $\foc$-cone as sorting we can represent cartesian monoidal categories with a commutative strong monad.

Let be the sorted doctrine defined as follows.
We take $\abs{\dD} = \mathsc{dblsplit}$, as in <ref>; thus a functor $\pi:\cP \to \abs{\dD}$ partitions the nonlinear objects of into left-hand and right-hand ones.
We equip with cones for $\ten,\unit,\coten,\counit$, as well as $\foc$ defined on left-hand objects, $\uoc$ taking values in left-hand objects, $\fwn$ defined on right-hand objects, and $\uwn$ taking values in right-hand objects.
And we take the $\uoc$ and $\uwn$ cones as sorting.
Then a -category is strictly well-sorted just when it has a choice of $\uoc$ and $\uwn$ that are bijective onto the left-hand and right-hand objects respectively.
A straightforward extension of <ref> now shows that this is the same as its being the double-Kleisli adjunction of <ref> constructed from the linearly distributive category with storage $\Plin$.
Thus, the 2-categories of linearly distributive or $\ast$-autonomous categories with storage, and their variants with limits and colimits, are equivalent to for some sorted doctrine .

By making one of the sorts in $\mathsc{smadj}$ (<ref>) derived from the other, we obtain sorted doctrines for lax symmetric monoidal monads or comonads.

Recall the multicategory $\mathsc{linpol}$ from <ref>.
We now rechristen it $\mathsc{symskew}$, calling its two linear objects $\mathsc{l}$ and $\mathsc{t}$; thus there is a unique morphism $\Gamma \to \mathsc{l}$ when $\Gamma$ consists entirely of $\mathsc{l}$'s, and a unique morphism $\Gamma \to \mathsc{t}$ when $\Gamma$ contains no more than one $\mathsc{t}$.
We make this a sorted doctrine with $\mathsc{t}$ primitive, $\mathsc{l}$ derived, sorting cone $\mathsc{l} \to \mathsc{t}$ (with vertex $\mathsc{l}$), and no other cones.

A strictly well-sorted -category is determined by the objects over $\mathsc{t}$ and the morphisms with target over $\mathsc{t}$.
Every object over $\mathsc{l}$ is the image of one over $\mathsc{t}$ by a functor that we may either leave implicit or denote $\mathsf{G}$.
We call a morphism over $\Gamma \to \mathsc{t}$ loose if $\Gamma$ consists entirely of $\mathsc{l}$'s, and tight if $\Gamma$ contains a $\mathsc{t}$; the latter are uniquely determined by those where the first element of $\Gamma$ is $\mathsc{t}$.
This yields a doctrine for the symmetric skew multicategories of <cit.>.
We can combine this with <ref> to obtain a sorted doctrine for non-symmetric skew multicategories as in [8].

In a skew multicategory, a tight unit $\done$ (with restricted universal property) is a “left universal nullary map classifier”, while a tensor product $\mathsf{G} A\ten B$ is a “left universal tight binary map classifier” (see <cit.>), and a hom $\mathsf{G} A \hom B$ corresponds to the notion of “closedness” from <cit.>.
Thus, by [8, 9], we have sorted doctrines for (symmetric) skew monoidal categories and (symmetric) skew closed categories.
In particular, the “noninvertible associator” of a skew monoidal category is represented as a comparison map

\[ \mathsf{G} A \ten (\mathsf{G} B \ten C) \too \mathsf{G}(\mathsf{G} A \ten B) \ten C \]

whose noninvertibility is unsurprising due to the different placements of $\mathsf{G}$.
(However, a symmetric closed skew-monoidal category is not a bifibration over $\mathsc{symskew}$; it lacks some universal properties, such as a tensor product of two loose objects.)

Unlike -completeness, well-sortedness is a coreflective property.

For any sorted doctrine , the 2-category of well-sorted -sketches is coreflective in , and the coreflector preserves -completeness.

The coreflection of a -sketch is its full subcategory $\cS'$ containing all objects of that lie over primitive sorts, and precisely those objects lying over derived sorts that are the vertex of a proto-extremal lift of the sorting cone.
Its proto-universal cones are precisely those of that land in this subcategory.

If is -complete, $\cS'$ is clearly still realized and saturated.
To see that $\cS'$ is also still precomplete, note that by construction it still has proto-universal lifts of the sorting cones.
But by definition, any non-sorting -cone must have a primitive vertex, and therefore the proto-universal lifts of such cones in still lie in $\cS'$.

Over a Kleisli sorted doctrine, the well-sorted coreflection of an adjunction is the Kleisli adjunction of its comonad.
Similarly, over the doctrine of linearly distributive categories with storage from <ref>, the well-sorted coreflection of a linearly distributive adjunction (<ref><ref>) is the double-Kleisli adjunction of its induced monad/comonad pair (<ref>).

Finally, we remark on what it takes for a doctrine map to preserve well-sortedness.

Let $\dD_1$ and $\dD_2$ be sorted doctrines.
A doctrine map $\F:\dD_1\to\dD_2$ is sorted if it preserves primitive sorts, derived sorts, and sorting cones, and moreover for any derived sort $R$ of $\dD_1$, any sorting $\dD_2$-cone with vertex $F(R)$ is the image of some sorting $\dD_1$-cone with vertex $R$.

If $\F:\dD_1\to\dD_2$ is a sorted doctrine map, then $\ladj{\F}$ and $\radj{\F}$ from <ref> preserve well-sortedness.

For $\ladj{\F}$, let $\pi :\cS \to \abs{\dD_1}$ be a well-sorted $\dD_1$-sketch, let $R$ be a derived $\dD_2$-sort, and let $S \in (F\pi)^{-1}(R)$.
Then $\pi(S)$ is a derived $\dD_1$-sort.
So since is well-sorted, there is a proto-extremal lift of its sorting cone $G_R$ that maps the vertex to $S$.
But by assumption, $F G_R$ is the sorting $\dD_2$-cone of $F(R)$, while by definition this lift of it is also proto-extremal in $\ladj{\F}(\cS)$.
Thus, $\ladj{\F}(\cS)$ is well-sorted.

For $\radj{\F}$, let $\pi:\cS\to\abs{\dD_2}$ be a well-sorted $\dD_2$-sketch and $R$ a derived $\dD_1$-sort.
An object of $\radj{\F}(\cS)$ over $R$ is an object $S\in \pi^{-1}(F(R))$.
Since $F(R)$ is a derived $\dD_2$-sort and $\cS$ is well-sorted, there is a proto-extremal lift of its sorting cone $G_{F(R)}$ that maps the vertex to $S$.
By assumption, $G_{F(R)}$ is the image of the sorting $\dD_1$-cone $G_R$, and this proto-extremal lift of $G_{F(R)}$ induces a proto-extremal lift of $G_R$ to $\radj{\F}(\cS)$ mapping the vertex to $S$.
Thus, $\radj{\F}(\cS)$ is well-sorted.

§ THE DOCTRINAL COMPLETION OF A SKETCH

We will now show that any -sketch can be completed to a -category in a universal way.

Recall (see e.g. [1]) that an object of a category is said to be injective with respect to a set of morphisms if for any morphism $\cA\to\cB$ in , any morphism $\cA\to\cP$ can be extended to (not necessarily uniquely):

\[
\begin{tikzcd}
\cA \ar[r] \ar[d] & \cP\\
\cB \ar[ur,dotted]
\end{tikzcd}
\]

The class of all -injective objects is called a small-injectivity class (“small-” since $\cI$ is a set rather than a proper class).
If we require the extensions to be unique, we obtain the related notions of orthogonal object and small-orthogonality class.
In a category with pushouts, is orthogonal to $\cA\to\cB$ if and only if it is injective with respect to $\cA\to\cB$ and its codiagonal $\cB+_\cA \cB \to\cB$; thus every small-orthogonality class is also a small-injectivity class.

If is small, then the -complete sketches are a small-injectivity class in $\dsketch$.

Given any -cone $G:\cC\to \abs{\dD}$, we regard it as a -sketch in which the only proto-extremal cone is $G$ itself.
We also regard its reduct as a -sketch via the composite $\cC'\into \cC \to \abs{\dD}$, with no proto-extremal cones at all.
Then a -sketch is precomplete if and only if it is injective to the inclusions of -sketches $\cC'\into \cC$.

Similarly, given any -cone $G:\cC\to \abs{\dD}$, any expansion of it (<ref>), and any extension of $G$ to $G_\Omega : \cC_\Omega \to \abs{\dD}$, we regard $\cC_\Omega$ and its corresponding pre-expansion $\cC_\Omega'$ as -sketches via $G_\Omega$ and its restriction to $\cC'_\Omega$, in which the only proto-extremal cone is $G$.
Then a -sketch is realized if and only if it is orthogonal to the set of inclusions of -sketches $\cC'_\Omega\into \cC_\Omega$, indexed over all $G$, $\Omega$, and $G_\Omega$.

Finally, given an abstract cone $\cC$ with vertex $K$, let $\cC_{\cong}$ denote the polycategory that is with an additional signed object $K'$ isomorphic to $K$.
There is a fold map $\cC_{\cong} \to \cC$ that collapses $K$ and $K'$ both to $K$, which has two sections $s,s':\cC\to\cC_{\cong}$ sending $K$ to $K$ and $K'$ respectively.
If $G:\cC\to \dD$ is a -cone, we can regard $\cC_{\cong}$ as a -sketch via the composite $\cC_{\cong} \to \cC\to \abs{\dD}$, in which both $s,s'$ are proto-extremal.
We can also regard it as a -sketch in which only $s$ is proto-extremal; we denote this sketch by $\cC_{\cong}'$.
Then a -sketch is saturated if and only if it is injective with respect to the set of inclusions of -sketches $\cC_{\cong}' \into \cC_{\cong}$.

Let $\cI_\dD$ denote the set of all the morphisms $\cC'\into\cC$, $\cC'_\Omega \into \cC_\Omega$, $\cC_\Omega +_{(\cC'_\Omega)}\cC_\Omega \to \cC_\Omega$, and $\cC_{\cong}' \into \cC_{\cong}$.
Then a sketch is -complete if and only if it is injective to $\cI_\dD$.

The proof shows that realized -sketches are actually a small-orthogonality class.
Saturated -sketches are also a small-orthogonality class, since the inclusions $\cC_{\cong}' \into \cC_{\cong}$ are epimorphic (being the identity on underlying polycategories).

If is small, then every -sketch has a weak -reflection, i.e. a map $\cS \to \sdhat$ such that $\sdhat$ is -complete and any map from to a -complete sketch factors through .

This is a standard construction applying to any small-injectivity class, known as Quillen's small object argument; see e.g. <cit.> or <cit.> or <cit.>.
Let $\cS_0 = \cS$.
Given $\cS_n$, define inductively $\cS_{n+1}$ as the pushout

\[
\begin{tikzcd}
\coprod_{\iota,u} \cA_{\iota} \ar[r] \ar[d] & \cS_n \ar[d] \\
\coprod_{\iota,u} \cB_{\iota} \ar[r] & \cS_{n+1} \ulpullback
\end{tikzcd}
\]

where the coproducts are over all $\iota:\cA\to\cB$ in the generating set $\cI_\dD$ and all $u:\cA \to \cS_n$.
Continue the iteration into transfinite ordinals $n$ by taking colimits at limit stages.
Then since $\dsketch$ is locally presentable, there is a sufficiently large ordinal $\ka$ such that any map $\cA \to \cS_\ka$, for any $i:\cA\to\cB$, factors through $\cS_n$ for some $n<\ka$, and hence extends to $\cB$ through $\cS_{n+1}$.
Thus, if we define $\sdhat = \cS_\ka$, it is -complete.
Moreover, given a -complete sketch $\cT$, we can extend a map $\cS\to \cT$ to each stage $\cS_n$ inductively, using the completeness of at successor stages.

The factorization $\sdhat \to \cT$ constructed in <ref> is not in general unique,

but we will show that it is

unique up to unique isomorphism.

There is an additional wrinkle, however: if $\dD$ contains operations such as $\hom,\duals$ that are contravariant in some arguments, then -completion cannot be expected to behave well with respect to noninvertible 2-cells.
Thus we have to formulate its universal property with respect to $\dsketch_g$, where $\sK_g$ denotes the underlying (2,1)-category af a 2-category $\sK$, containing only the invertible 2-cells.

For any small doctrine and -sketch , there is a -complete sketch and a map $\cS\to \sdhat$ such that for any -complete sketch $\cP$, the precomposition functor $\dsketch_g(\sdhat,\cP) \to \dsketch_g(\cS,\cP)$ is a surjective equivalence of categories.
In particular, the sub-2-category of -complete sketches in $\dsketch_g$ (which, recall, is equivalent to $\dcat_g$) is pseudo-reflective.

In <ref>, $\sdhat$ was constructed as a transfinite composite of pushouts of the generators.
Since surjective equivalences are closed under pullbacks and inverse transfinite composites, it suffices (see e.g. <cit.>) to show that for any -complete sketch $\pi:\cP\to\abs{\dD}$ and any morphism $\iota : \cA \to \cB$ in $\cI_\dD$, the induced map $\dsketch_g(\cB,\cP) \to \dsketch_g(\cA,\cP)$ is a surjective equivalence.
Since it is always surjective on objects, it remains to prove that it is fully faithful.
Referring to the construction of $\cI_\dD$, there are four cases we need to consider.

When $\iota$ is an inclusion $\cC'\into \cC$ for some -cone $G:\cC\to\abs{\dD}$, we must show that given two $\pi$-extremal lifts $H,K:\cC\to\cP$ of $G$, any isomorphism $\al:H'\cong K'$ between their reducts $H',K' : \cC'\to\cP$ can be uniquely extended to a compatible isomorphism $H\cong K$.
By composing the transitions of $K$ with the components of $\al$ and their inverses (depending on the sign of the relevant signed object), we obtain the data for an pre-expansion of $H$ by a single object, namely the vertex of $K$.
Thus, extremality of $H$ induces a map between the vertices of $H$ and $K$ (with direction depending on the sign of that vertex).
Similarly, we obtain a map in the other direction, and the two are inverses.

When $\iota$ is an inclusion $\cC'_\Omega\into\cC_\Omega$, we must show that given two expansions $H,K:\cC_\Omega \to \cP$ of $\pi$-extremal lifts, any isomorphism $\al:H'\cong K'$ between their corresponding pre-expansions $H',K': \cC_\Omega' \to \cP$ is also an isomorphism $H\cong K$.
Since the inclusion $\cC_\Omega'\into \cC_\Omega$ is bijective on objects, this is just an extra naturality condition with respect to the factorization morphism.
But the two sides of this desired naturality square each fit into an expansion of $H$ whose expanders are those of $K$ composed with components of $\alpha$ or their inverses; hence they are equal.

Finally, when $\iota$ is a codiagonal $\cC_\Omega +_{(\cC'_\Omega)} \cC_\Omega \to \cC_\Omega$ or an inclusion $\cC_{\cong}'\into\cC_{\cong}$, full-faithfulness is automatic since these $\iota$'s are bijective on objects and full.

For any sorted doctrine and any well-sorted -sketch , the completion is also well-sorted.

Let be well-sorted, and let $(\sdhat)' \to \sdhat$ be the well-sorted coreflection of .
Since is well-sorted, the map $\cS \to\sdhat$ factors through $(\sdhat)'$.
But by <ref>, $(\sdhat)'$ is -complete, so the universal property of induces a map $\sdhat \to (\sdhat)'$ that is a section of the coreflection, up to isomorphism.
This implies that is also well-sorted.

§ THE SEQUENT CALCULUS OF A DOCTRINE

Let be an doctrine and an polycategory with a map $\pi : \cS \to \abs{\dD}$, which we regard as a -sketch with no proto-extremal cones.
Then <ref> implies that generates a free -category $\sdhat$.
We now extract a sequent calculus that presents such free -categories from the proof of <ref>.

For simplicity, for now we suppose that

is unsorted,

$\abs{\dD}$ is subterminal, and

all the cones of are discrete (have no nonidentity abstract transitions) and also finite.
The latter includes cones for universal morphisms, as in <ref>, and also for finite products and coproducts, as in <ref>.
These are the primary universal properties that are traditionally considered in logic.

Under these assumptions, we can replace the construction of <ref> by the following simplified version.

* First perform the small object argument starting at $\cS_0 = \cS$, using only the inclusions $\cC'\into\cC$ for -cones , and when $n>0$ restricting the coproduct to include only the morphisms $u:\cC'\to\cS_n$ that do not factor through $\cS_{n-1}$.
After a countable iteration, this produces a precomplete sketch $\cS_\om$.

* Next perform the small object argument starting at $\cS_\om$, using only the inclusions $\cC'_\Omega\into\cC_\Omega$ and their codiagonals $\cC_\Omega +_{(\cC'_\Omega)} \cC_\Omega \to \cC_\Omega$.
After a further countable iteration, this produces a realized sketch $\cS_{\om+\om}$.
Moreover, since these inclusions and codiagonals are bijective on objects and each $\cC'$ is discrete, $\cS_{\om+\om}$ is still precomplete.

* Finally, perform one step of the small object argument using the map $\cC_{\cong}'\into\cC_{\cong}$.
This is sufficient to produce a saturated sketch $\sdhat = \cS_{\om+\om+1}$, which is still precomplete and realized, and hence -complete.

In particular, these changes make the argument completely constructive.
(The negation in <ref> may not seem constructive, but the inclusion of $\cS_{n-1}$ into $\cS_{n}$ is decidable on objects because each $\cC'\into\cC$ is.)

A ∈^τA

a -cone
' = {r_1^τ_1,…, r_n^τ_n}

R_1 τ_1
R_n τ_n
[R_1,…,R_n] τ_

Type-forming rules

R ⊢R^-, R^+
⊢Φ, K
⊢K, Ψ⊢Φ,Ψ
: Φ→Ψ a structural map⊢Φ

Structural rules

f ∈(Φ)⊢Φ

Generator rule

a -cone with vertex  r^
' = {r_1^τ_1,…, r_n^τ_n}

R_1 τ_1
R_n τ_n

f∈(r_i_1^_1,…,r_i_ℓ^_ℓ,r^)  an abstract projection

⊢R_i_1^_1, …,  R_i_ℓ^_ℓ,  [R_1,…,R_n]^

Noninvertible logical rule

a -cone with vertex  r^ of class $\tau_\cC$
' = {r_1^τ_1,…, r_n^τ_n}

R_1 τ_1
R_n τ_n

S_1 σ_1
S_m σ_m

(τ_^-, σ_1^η_1,…, σ_m^η_m) ≠∅

{⊢R_i_1^_1, …,  R_i_ℓ^_ℓ,  S_1^η_1, …,  S_m^η_m }_f∈(r_i_1^_1,…,r_i_ℓ^_ℓ,r^)  an abstract projection
⊢[R_1,…,R_n]^-, S_1^η_1,…, S_m^η_m

Invertible logical rule

LNL Sequent calculus

We can now describe $\sdhat$ using a sequent calculus, defined formally in <ref>.

There are two classes of types, linear and nonlinear, written $A\ltype$ and $X\nltype$.
Generically, we write $R \ttype$ for an arbitrary class $\tau \in \{\mathrm{L},\mathrm{NL}\}$.
The first rule in <ref> says that every object of determines a type of the appropriate class.

By assumption, the reduct $\cC'$ of each -cone is a discrete polycategory with finitely many objects.
We assume the objects of each $\cC'$ are ordered as $\{r_1^{\tau_1},\dots,r_n^{\tau_n}\}$, the notation meaning that $r_i$ is of class $\tau_i$, and the vertex $k$ of class $\tau_\cC$.
The second rule in <ref> says that every such cone induces an operation on types.
The notation $\boc[R_1,\dots,R_n]$ is chosen to be generic over the cone , but for particular choices of we use the notations of <ref>, e.g. $A\ten B$, $\foc X$, $X \rtimes A$, $A \with B$, etc.

There is a bijection between the valid judgments $R \ttype$ and the $\tau$-objects of $\sdhat$.

Define the height of $R \ttype$ recursively: the height of an object of is zero, while that of $\boc[R_1,\dots,R_n]$ is one more than the maximum height of $R_1,\dots, R_n$.
(If $n=0$, the height of $\boc[\,]$ is 1.)
I claim that there is a bijection between the valid judgments $R \ttype$ of height $\le n$ and the $\tau$-objects of $\cS_n$.
This is true for $n=0$.
The objects of $\cS_{n+1}$ are those of $\cS_n$ plus a new vertex for each $u:\cC'\to \cS_n$ not factoring through $\cS_{n-1}$.
But the latter are the applications of the $\boc$-rule with at least one premise of height $n$, hence whose conclusion has height $n+1$.

We denote the sequents in entries-only style as $\vdash \Phi$, where $\Phi$ is an admissible list of signed types, defined analogously to the semantic case in <ref>.
The structural rules are shown in <ref>.
The first is the identity rule and the second is the cut rule.
The third incorporates exchange for all types, plus contraction and weakening for nonlinear types, as in <ref>.
Similarly, the generator rule in <ref> says that every morphism of induces a derivation of a sequent.

We may write $\Th \mid \Gm \vdash \De$ for $\vdash \Th^-, \Gm^-, \De^+$, and $\Theta\vdash X$ for $\vdash \Th^-,X^+$.
In this notation, the identity and cut rules multifurcate into linear and nonlinear versions:

A·|A ⊢AX X ⊢XΥ⊢X
Θ,X ⊢YΘ,Υ⊢Y

Θ'|Γ' ⊢Δ',A
Θ|Γ,A⊢ΔΘ,Θ' |Γ,Γ' ⊢Δ,Δ'Υ⊢X

We divide the logical rules into invertible (right rules for negative types and left rules for positive types) and noninvertible (left rules for negative types and right rules for positive types).
The generic noninvertible rule is in <ref>.
Here $\ep$ and the $\ep_j$'s are signs $+,-$.
For instance, if is the cone for $\ten$, with objects $a,b$ and vertex $c$, there is one abstract projection $f\in \cC(a^-,b^-,c^+)$ and the rule becomes

\[\infer{A \ltype \\ B\ltype}{\cdot\mid A,B\vdash A\ten B}. \]

If is the cone for $\with$,

with objects $a,b$ and vertex $c$, there are two abstract projections $f\in \cC(a^+,c^-)$ and $g\in \cC(b^+,c^-)$, and the rule becomes two:

B·|AB ⊢AA
B·|AB ⊢B.

The rules for the modalities are

X X |·⊢XA A|·⊢A X X |X ⊢· A A|A ⊢·

Unlike noninvertible rules in most common sequent calculi, ours does not build in a cut.
But we can always apply a cut afterwards, since the latter is primitive in our system.
(We leave cut-elimination for future study.)
Since the modalities are the most novel aspect of this calculus, we list their derived cut-containing rules:

Θ⊢XΘ|·⊢XΘ|Γ,A ⊢ΔΘ,A|Γ⊢Δ Θ⊢XΘ|X ⊢· Θ|Γ⊢Δ,AΘ,A|Γ⊢Δ.

If $\abs{\dD}=\mathsc{lnlmulti}$, so $\Delta$ is a singleton, these rules for $\foc$ and $\uoc$ specialize to the noninvertible rules of [7].
If instead $\abs{\dD}=\mathsc{cbpv}$, so $\Delta$ is a singleton and $\Gamma$ is empty, we obtain the rules of [31].

There is a surjection from the derivations of $\vdash \Phi$ using only the structural, generator, and noninvertible rules to the hom-set $\cS_\om(\Phi)$.

Such a function is defined by induction on derivations: the structural rules use that $\cS_\om$ is an polycategory, the generator rule uses the functor $\cS \to \cS_\om$, and the noninvertible rule uses the images of abstract projections under the proto-extremal cones of $\cS_\om$, which exist (by construction, in fact uniquely) since it is precomplete.
We show inductively that it is surjective onto morphisms in $\cS_n$.

For $n=0$ this follows from the generator rule.
Since $\cS_{n+1}$ is a pushout, its morphisms are generated by the operations in an polycategory (identities, composition, and structural actions) from those of $\cS_n$ and those of the cones .
The latter arise from the noninvertible rules, while the polycategory operations are reflected by the structural rules.

Finally, the generic invertible rule is shown in figure <ref>, where $-\ep$ reverses a sign.
The requirement $\abs{\dD}(\tau_\cC^{-\ep}, \sigma_1^{\eta_1},\dots, \sigma_m^{\eta_m}) \neq \emptyset$ ensures that we do not produce sequents not allowed by $\abs{\dD}$, e.g. the universal properties of limits and colimits are restricted as necessary in an multicategory.
(Recall we are assuming $\abs{\dD}$ to be subterminal, so its nonempty homsets are singletons.)

For instance, if is the cone for $\ten$ as above, the rule becomes

\[\infer{\vdash A^-,B^-,\Omega}{\vdash (A\ten B)^-,\Omega} \qquad = \qquad
\infer{\Theta \mid \Gamma, A,B \vdash \Delta}{\Theta \mid \Gamma, A\ten B \vdash \Delta}
\]

while if is the cone for $\with$ as above, the rule becomes

\[\infer{\vdash A^+,\Omega \\ \vdash B^+,\Omega}{\vdash (A\with B)^+, \Omega}
\qquad = \qquad
\infer{\Theta \mid \Gamma \vdash \Delta,A \\ \Theta\mid\Gamma\vdash\Delta,B}{\Theta\mid\Gamma\vdash\Delta,A\with B.}
\]

the rules for other common connectives such as $\hom,\oplus,\unit,\counit,\coten,\times,\to,1$ specialize to the usual ones for classical or intuitionistic multiplicative-additive linear logic or intuitionistic nonlinear logic.

For the modalities, the invertible rules are:

Θ,X |Γ⊢ΔΘ|Γ,X ⊢ΔΘ|·⊢AΘ⊢AΘ,X |Γ⊢ΔΘ|Γ⊢Δ,XΘ|A ⊢·Θ⊢A
As before, if $\abs{\dD}=\mathsc{lnlmulti}$ or $\abs{\dD}=\mathsc{cbpv}$, these rules for $\foc$ and $\uoc$ specialize to those of [7] or [31] respectively.
Similarly, the rules for $\eechom$ and $\rtimes$, with appropriate cuts added:

Θ'|Γ⊢AΘ,Θ' |Γ⊢BΘ|A ⊢BΘ⊢AB

Θ'|Γ⊢AΘ,Θ' |Γ⊢X⋊AΘ|Γ⊢X⋊A
Θ',X |Γ', A ⊢ΔΘ,Θ' |Γ, Γ' ⊢Δ
specialize when $\abs{\dD}=\mathsc{ecbv}$ (so $\Gamma$ is a singleton and $\Gamma'=\emptyset$) to those of [36] (modulo changes of notation, and additive maintenance for the nonlinear context).

There is a surjection from derivations of $\vdash\Phi$, in the full sequent calculus of <ref>, to the hom-set $\sdhat(\Phi)$.