\(R\)  commutes with sifted colimits.

Given that adjunctions compose, this data yields a category \(\mathsf {Var}\) .
Let \(\mathsf {Prod}\)  be the 2-category whose objects are small cartesian categories, morphisms are cartesian functors and 2-cells are natural transformations. Then Observation REF  boils down to defining a 2-functor \(\mathsf {Mod}\colon \mathsf {Prod}^\text{op}\rightarrow \mathsf {Var}\) . The following captures the relationship between \(\mathsf {Law}\)  and \(\mathsf {Var}\) .
Theorem 2.34 ([1]})  
There exists a 2-adjunction whose unit is an equivalence:
\( \mathsf {Th}: \mathsf {Var} \leftrightarrows \mathsf {Prod}^{\text{op}} : \mathsf {Mod}\) 


Remark 2.35 One obtains the \(S\) -sorted version of Theorem REF  by slicing on both sides over the free category with products on \(S\) . This is given in more detail for partial Lawvere theories in §REF .

Equational theories as monoidal theories
Given that Lawvere theories are cartesian props, Theorem REF  suggests how to consider them as monoidal theories. We recall the recipe from [2]}: the idea is to characterise \(\Sigma \) -terms as certain string diagrams, and then—through this lens—turn any equational theory into a monoidal theory.
Recipe 2.36 
Fix a signature \(\Sigma \) . A \(\Sigma \) -term \(t: T_\Sigma ^{[n]}\)  is the same thing as
a string diagram \(n\rightarrow 1\)  in the prop induced by the monoidal theory
with

generators \(\Gamma \stackrel{\text{def}}{=}\Sigma + (\ref {eq:comonoidgenerators})\)

(REF ) together with equations that ensure naturality with respect to the comonoid structure. The latter
can be easily added as two additional equations for each \(\sigma : \Sigma \) :
\(\begin{tikzpicture}[xscale=.5, baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \sigma };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \sigma };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \sigma };\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\begin{scope}[xshift=9cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \sigma };\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node [left] at (0,2*0.25) {m};\node [left] at (4,2*0.25) {m};\node [left] at (9,2*0.25) {m};\node [left] at (13,2*0.25) {m};\node at (11.5,2*0.25) {=};\end{tikzpicture} \qquad \mathrm {(SN\sigma )}\) 



The Lawvere theory induced by equational theory \((\Sigma ,E)\)  can now be seen as the prop induced by
the monoidal theory \((\Gamma ,F)\)  where \(F\)  is the set of equations obtained by translating the equations in \(E\)  to string diagrams, together with (REF ), and (REF ) for each \(\sigma : \Sigma \) .
It is important to build an intuition behind this translation.
An obvious difference between terms and string diagrams is that the latter do not have named variables. The translation ensures that wires play the role of variables,
and the comonoid structure plays the role of “variable management”. We illustrate this with an example below.
Example 2.37 
The prop corresponding to the Lawvere theory induced by the equational theory of commutative monoids (Example REF ) is the same as the prop of commutative bialgebra. For example, the term \(m(m(x,x),y)\)  in the theory of commutative monoids can be depicted as
\(\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=1*0.25cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle m};\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle m};\end{scope}\end{scope}\end{tikzpicture}\) 
In the term we have considered, the variable \(x\)  appears twice. In the corresponding diagram, the wire corresponding to \(x\)  starts with a comultiplication that witnesses the “copying of \(x\) ”.


Algebra of partial maps
We have seen that finite products are central in classical universal algebra. It is therefore natural to begin our development of its partial analogue by identifying the corresponding universal property in the partial setting. We will see that this amounts to replacing the class of cartesian categories with the class of discrete cartesian restriction categories (DCR categories) [3]}. Next, we characterise DCR categories in terms of algebraic structure, analogous to REF  for cartesian categories.
Partial functions
The starting point of our journey is the (2-)category \(\mathsf {Par}\)  of sets and partial functions. Just as \(\mathsf {Set}\)  was the semantic universe for ordinary equational theories, \(\mathsf {Par}\)  is the semantic universe for partial equational theories.
We first recall an elementary, set theoretic presentation:
Definition 3.1 
\(\mathsf {Par}\)  has sets as objects and partial functions \(f\colon X\rightharpoonup Y\)  as arrows, where
a partial function \(f\)  is a pair \((\mathsf {dom}f,\,\mathsf {def}f)\)  where \(\mathsf {dom}f\subseteq X\)  is the domain of definition of \(f\)  and \(\mathsf {def}f\colon \mathsf {dom}f\rightarrow Y\)  is a (total) function.
Given a partial function \(f\colon X\rightharpoonup Y\) , and some \(X^{\prime }\subseteq X\)  we write \(f\!\!\mid _{X^{\prime }}\)  for the partial function \((\mathsf {dom}f\cap X^{\prime },\, f^{\prime })\)  where \(f^{\prime }\colon \mathsf {dom}f\cap X^{\prime }\rightarrow Y\)  is \(\mathsf {def}f\)  restricted to the (potentially smaller) domain of definition \(\mathsf {dom}f\cap X^{\prime }\) . Similarly, given \(Y^{\prime }\subseteq Y\) , write \(f^{-1}(Y^{\prime })=\lbrace x\in \mathsf {dom}f\;\mid \; \mathsf {def}f(x)\in Y^{\prime }\rbrace \) .
Given
\(f\colon X\rightharpoonup Y\)  and \(g\colon Y\rightharpoonup Z\) , their composite is defined by
\(f \mathop {\fatsemi }g = (f^{-1}(\mathsf {dom}g),\, (\mathsf {def}f\!\mid _{f^{-1}(\mathsf {dom}g)} \mathop {\fatsemi }\mathsf {def}g)\) . The identity on \(X\)  is \((X,\text{id}_X)\) .
There is a natural partial order between partial functions \(X\rightharpoonup Y\) :
\(f\le g \quad \stackrel{\text{def}}{=}\quad \mathsf {dom}f\subseteq \mathsf {dom}g \;\wedge \; g \!\mid _{\mathsf {dom}f}\, = f. \) 
It is straightforward to verify that this data makes \(\mathsf {Par}\)  a category, and with \(\le \) , a 2-category.

Categorifying partiality has long history (see e.g., [4]}, [5]}). We recall a classical approach:
Definition 3.2 
Suppose that \(\mybb {C}\)  has finite limits.
Its 2-category of partial maps, \(\mathsf {Par}(\mybb {C})\)  has:

objects are objects of \(\mybb {C}\) .

arrows are equivalence classes \([m,f] : X \rightarrow Y\)  of spans
\(X \xleftarrow{} A \xrightarrow{} Y\) 
where \(m\)  is monic. We equate \((m,f) \sim (m^{\prime },f^{\prime })\)  iff there is an isomorphism \(\alpha \)  s.t. the following diagram commutes:
\(\scriptsize \begin{tikzcd}& A [dl,"m"^{\prime }] [drr,"f"^{\prime }] [r,"\alpha "] & A^{\prime } [dll,"m^{\prime }"] [dr,"f^{\prime }"] \\X &&& Y.\end{tikzcd}\) 


2-cells: \([m,f]\le [m^{\prime },f^{\prime }]\)  when there exists any \(\alpha \)  that makes the diagram commute.

composition is defined by pullback. Explicitly, the composite of \((m,f) : A \rightarrow B\)  and \((m^{\prime },g) : B \rightarrow C\)  is the outer span of the diagram on the left
\(\begin{tikzcd}[row sep=small,column sep=small]&& X \wedge X^{\prime } [ld,"\pi _0"^{\prime }] [rd,"\pi _1"]\\& X [ld,"m"^{\prime }] [rd, "f"] && X^{\prime } [ld,"m^{\prime }"^{\prime }] [rd,"g"] \\A && B && C\end{tikzcd}\) 
where the square with top \(X\wedge X^{\prime }\)  is a pullback in \(\mybb {C}\) . Note that it doesn't matter which pullback, since any two choices will give isomorphic spans, and therefore equal morphisms.

Identities are diagonal spans \((1_A,1_A) : A \rightarrow A\) .


Given a morphism \((m,f) : A \rightarrow B\)  in \(\mathsf {Par}(\mybb {C})\) , we think of the monic \(m : X \rightarrow A\)  as a subobject, specifying which part of \(A\)  the morphism is defined on, and then \(f : X \rightarrow B\)  tells us what it does.
The following is a straightforward sanity check:
Observation 3.3 There is an isomorphism of (2-)categories \(\mathsf {Par}\cong \mathsf {Par}(\mathsf {Set})\) .

Just as a model of a total operation of arity \(n\)  is a function \(A^n\rightarrow A\)  (an arrow in \(\mathsf {Set}\) ), a model of a partial operation ought to be a partial function \(A^n\rightharpoonup A\)  (an arrow in \(\mathsf {Par}\) ). For this reason, it is important to understand the mathematical status of the cartesian product in \(\mathsf {Par}\) . Interestingly, \(\mathsf {Par}\)  has categorical products, but these do not correspond to the cartesian product of sets.The categorical product of \(A\)  and \(B\)  in \(\mathsf {Par}\)  is \((A+\lbrace \star \rbrace )\times (B+\lbrace \star \rbrace ) - \lbrace (\star ,\,\star )\rbrace \) . This can be seen via the equivalence \(1/\mathsf {Set}\simeq \mathsf {Par}\) . Limits in the coslice category \(1/\mathsf {Set}\)  are calculated pointwise,
and the functor \(1/\mathsf {Set}\rightarrow \mathsf {Par}\)  removes the point

Cartesian Restriction Categories
It is by focusing on the universal property of the cartesian product in \(\mathsf {Par}\)  that we are able to identify a generalisation of Lawvere's approach to partial operations. This is the goal of this section.
Restriction categories were devised to study partial phenomena in an axiomatic setting. Here we give a whirlwind tour, more details can be found in [5]}, [7]}, [3]}. In a restriction category, every arrow \(f : A \rightarrow B\)  has an associated idempotent \(\overline{f} : A \rightarrow A\) , thought of as the identity function restricted to the domain of definition of \(f\) . We call them domain idempotents.
Arrows where \(\overline{f} = 1_A\)  are called total, and form a subcategory. Further, we have:
Remark 3.4 
Any restriction category is poset-enriched, with the ordering defined by
\(f \le g \Leftrightarrow \overline{f}\mathop {\fatsemi }g = f\) 


Functors \(F\)  that preserve domain idempotents (\(F\overline{f} = \overline{Ff}\) ) are called restriction functors. Restriction categories and restriction functors form a category. This extends to a 2-category in which the 2-cells are lax transformations. A lax transformation \(\alpha : F \rightarrow G\)  of restriction functors \(F,G : \rightarrow \)  consists of a family of total maps \(\alpha _A : FA \rightarrow GA\)  in \(\)  indexed by the objects \(A\)  of \(\)  s.t. for every \(f : A \rightarrow B\)  of \(\)  the usual naturality square commutes up to inequality:
\(\scriptsize \begin{tikzcd}FA [d,"Ff"^{\prime }] [r,"\alpha _A"] & GA [d,"Gf"] \\FB [r,"\alpha _B"^{\prime }] [ur,phantom,"\le "] & GB\end{tikzcd}\) 
where \(\le \)  is the ordering introduced above. Call this 2-category \(\mathsf {RCat}^\le \) . Just as categories with finite products enjoy a universal property in the 2-category \(\mathsf {Cat}\) , those with finite restriction products have a universal property in \(\mathsf {RCat}^\le \) . In general, formal limits in \(\mathsf {RCat}^\le \)  are called restriction limits [7]}. A cartesian restriction (CR) category is a restriction category with finite restriction products.
Observation 3.5 ([5]}) 
\(\mathsf {Par}\)  is a CR category, with the cartesian product as restriction product.

CR categories have appeared in the literature under a variety of different names, including p-category with a one-element object [4]} and partially cartesian category [12]}. For our development, it is crucial that the data of CR categories can be equivalently captured as follows:
Theorem 3.6 ([7]}) 
A CR category is the same thing as a symmetric monoidal category where every object is equipped with a commutative comonoid structure that is (REF ) and
the comultiplication is natural. That is, for any \(f : A \rightarrow B\)  we have \(f \mathop {\fatsemi }\delta _B = \delta _A \mathop {\fatsemi }(f \otimes f)\) .

From this perspective a CR category is very close to a cartesian category viewed as a monoidal category through REF . The difference is that we do not ask for the counit of the comonoid to be natural. This has profound consequences: for instance, the same symmetric monoidal category may have more than one such chosen comonoid structure, thus definining different CR categories.
Given the algebraic data, the domain idempotent \(\overline{f} : A \rightarrow A\)  of an arrow \(f : A \rightarrow B\)  in a CR category is recovered as:
\(\begin{tikzpicture}[xscale=.5][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny f};\end{scope}\begin{scope}[xshift=2cm, yshift=0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1cm,xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\node [left] at (-1,2*0.25) {\overline{f}};\node [left] at (0,2*0.25) {=};\end{tikzpicture}\) 
and so in particular the subcategory of \(\)  for which the counit is natural is precisely the subcategory of total maps. Notice that this means the subcategory of total maps of a CR category is cartesian.
Definition 3.7 A CR functor between two CR categories \(F : \rightarrow \)  is a functor that preserves the algebraic structure. That is, \(F(A\otimes B) = FA \otimes FB\) , \(F1 = 1\) , \(F\delta _A = \delta _{FA}\)  and \(F\varepsilon _A = \varepsilon _{FA}\) .

Remark 3.8 
A lax transformation of CR functors may be equivalently specified as a family of maps \(\alpha _A : FA \rightarrow GA\)  indexed by the objects \(A\)  of \(\)  s.t. for every \(f : A \rightarrow B\)  we have \(Ff \mathop {\fatsemi }\alpha _B \le \alpha _A \mathop {\fatsemi }Gf\) . We do not need to ask that each \(\alpha _A\)  is total, since if \(F\)  and \(G\)  preserve the cartesian restriction structure, then they are automatically total. In particular the diagram on the left gives the inequality on the right, which gives that \(\alpha _A\)  is total:

\(\scriptsize \begin{tikzcd}FA [d,"F\varepsilon _A"^{\prime }] [r,"\alpha _A"] & GA [d,"G\varepsilon _A"] \\FI [r,"\alpha _I"^{\prime }] [ur,phantom,"\le "]& GI\end{tikzcd}\qquad \qquad \) 
[height=.3cm]graffles/totalleft.pdf\(\) 

\(\includegraphics [height=.5cm]{graffles/totalright.pdf}\)
\(\) 
Discrete Cartesian Restriction Categories
Restriction products do not quite capture all the properties of \(\mathsf {Par}\)  needed for partial universal algebra. In particular, we require CR categories with the following extra structure:
Definition 3.9 A CR category is said to be \(\emph {discrete}\)  (DCR category [3]}) if for each object \(A\)  there is an arrow \(\mu _A : A \otimes A \rightarrow A\)  that is partial inverse to \(\delta _A\) . That is, \(\delta _A \mathop {\fatsemi }\mu _A = \overline{\delta _A} = 1_A\)  and \(\mu _A \mathop {\fatsemi }\delta _A = \overline{\mu _A}\) .

We give a novel presentation of DCR categories, inspired by the work of [15]}. Central to our presentation is the notion of a commutative special Frobenius algebra in which the monoid does not have a unit, which we call a partial Frobenius algebra. More precisely:
Definition 3.10 A partial Frobenius algebra \((A,\delta _A,\mu _A,\varepsilon _A)\)  in a symmetric monoidal category consists of a commutative comonoid \((A,\delta _A,\varepsilon _A)\)  and a commutative semigroup \((A,\mu _A)\)  s.t. \((A,\delta _A,\mu _A)\)  is a semi-Frobenius algebra. Diagramatically, this is the comonoid structure we have already seen together \(\mu _A\) , which we depict as \(\raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\)  in our string diagrams, subject to the following equations:
\(  \raisebox {.5em}{\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[yshift=0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=black] at (2*0.25,2*0.25) {};\end{scope}[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm,yshift=0.25cm]\begin{scope}[yshift=-0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=black] at (2*0.25,2*0.25) {};\end{scope}[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (2.5,2*0.25) {\qquad \mathrm {(MCA)}=};\end{tikzpicture}}\hspace{20.0pt}\raisebox {.5em}{\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}}\) 

\( \begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}[wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};\begin{scope}[xshift=1 cm]\begin{scope}[yshift=0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=black] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[yshift=-0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=8cm, xscale=-1]\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}[wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};\begin{scope}[xshift=1 cm]\begin{scope}[yshift=0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=black] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[yshift=-0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\end{scope}\end{scope}\node at (2.5,2*0.25) {\qquad \mathrm {(SFROB)}=};\node at (5.5,2*0.25) {=};\begin{scope}[xshift=10cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\node at (2.5,2*0.25) {=};\end{scope}\end{tikzpicture}\) 


Note that there is some redundancy in the equational presentation above, as discussed in [16]}.
We now extend the characterisation of CR categories given in Theorem REF  to DCR categories:
Theorem 3.11 
A DCR category is the same thing as a symmetric monoidal category where every object \(A\)  is equipped
with a coherent partial Frobenius algebra structure \((A,\delta _A,\varepsilon _A,\mu _A)\)  s.t. the comultiplication is natural. That is, for any \(f : A \rightarrow B\)  we have \(f \mathop {\fatsemi }\delta _B = \delta _A \mathop {\fatsemi }(f \otimes f)\) .

DCR categories are intimately connected to categories with finite limits [3]}. In particular:
Proposition 3.12 If \(\)  is a category with finite limits, \(\mathsf {Par}()\)  is a DCR category.

Definition 3.13 (the 2-category \(\mathsf {DCRC}^\le \) ) 
It follows that for any CR functor \(F : \rightarrow \)  between DCR categories, we have \(F\mu _A = \mu _{FA}\) . CR functors therefore give the notion of morphism between DCR categories. We consider the strict 2-category of DCR categories, restriction functors, and lax transformations, which we call \(\mathsf {DCRC}^\le \) .


Partial Lawvere theories
In this section we develop a Lawvere-style approach to partial algebraic theories, where operations may be partial. Ordinary Lawvere theories are determined by the free cartesian category on a single object \(^\text{op}\) ; we are thus interested in the analogue of \(^\text{op}\)  in the world of DCR categories.
The free DCR category on one object
Given Theorem REF , we have an explicit description for the DCR category on one object: it
is the prop \(\)  induced from the monoidal theory of partial Frobenius algebras. That is, it
has generators \(\lbrace \,\raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\; , \; \raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\; , \; \raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\,\rbrace \) 
and equations (REF ), (REF ) and (REF ).
It turns out that one can gain a precise intuition on what \(\)  looks like by mimicking the way in which the props \(\)  and its opposite \(^\text{op}\)  describe familiar algebraic structures. In fact, the prop \(\)  of commutative monoids is isomorphic to the prop \(\)  (see Observation REF ), and similarly, the prop \(\)  of commutative comonoids is isomorphic to \(^\text{op}\)  (Observation REF ).
The prop \(\)  of partial Frobenius algebras that we want to describe here can be given a similar “combinatorial” characterisation relying on the insights of Lack [18]}.
First, we note that the prop \(\)  induced by the monoidal theory of commutative semigroups (\(\lbrace \,\raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\,\rbrace \)  and equations (REF )) is isomorphic to sub-prop \(_s\subset \)  of finite sets and surjective functions.
Observation 4.1 
As props, \(\cong _s\) .

This is intuitive: as observed in Remark REF , string diagrams of \(\)  allow one to “draw” all functions \([m]\rightarrow [n]\) . Doing without the unit means that we can express exactly the surjective ones.
Next, we know from [18]} that the prop \(\)  induced by the monoidal theory of special Frobenius algebras with generators \(\lbrace \, \raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\; , \; \raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\; , \; \raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\; , \; \raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\,\rbrace \) 
and equations (REF ), (REF ) and (REF ) is isomorphic to the prop of cospans of finite sets \(\mathsf {Cospan}()\) . An arrow \(m\rightarrow n\)  here is (an isomorphism class of) a cospan of functions
\([m] \xrightarrow{} [k] \xleftarrow{} [n]\) , and composition is by pushout.
Proposition 4.2 ([18]}) 
As props, \(\cong \mathsf {Cospan}()\) .

Given that surjective functions are closed under composition and pushouts in \(\) ,
we can consider the subprop \(\mathsf {Cospan}_s()\)  of \(\mathsf {Cospan}()\)  with arrows those cospans where the left leg is surjective. Now, combining Observation REF  and Proposition REF  yields:
Proposition 4.3 As props, \(\cong \mathsf {Cospan}_s()\) .

This gives us a combinatorial characterisation of \(\) . But there is a more familiar and satisfactory way of describing \(\mathsf {Cospan}_s()\) . Given that cospans in \(\)  are spans in \(^\text{op}\) , and epimorphisms in \(\)  are monomorphisms in \(^\text{op}\) , we see that \(\mathsf {Cospan}_s() = \mathsf {Par}(^\text{op})\) ,
since a cospan in \(\)  with left leg surjective is the same thing as a span in \(^{\text{op}}\)  with left leg a monomorphism.
Therefore, we obtain:
Proposition 4.4 
As props, \(\cong \mathsf {Par}(^\text{op})\) .


Partial Lawvere theories
We have seen that \(^\text{op}\)  is central to the definition of Lawvere theories, being the free cartesian category on one object. The prop \(\mathsf {Par}(^\text{op})\) , being the free DCR on one object, plays the corresponding role in the definition of partial Lawvere theories.
Definition 4.5 
A partial Lawvere theory \(\)  is a DCR prop.

Spelled out, a partial Lawvere theory is a DCR category \(\)  for which there is an identity-on-objects CR functor \(\mathsf {Par}(^\text{op}) \rightarrow \) . A morphism of partial Lawvere theories is a functor \(h : \rightarrow \)  s.t. the following triangle commutes:
\(\scriptsize \begin{tikzcd}& \mathsf {Par}(^\text{op}) [dr, "q"] [dl, "p"^{\prime }] & \\[rr, "h"^{\prime }] && .\end{tikzcd}\) 
This defines the category \(\mathsf {pLaw}\)  of partial Lawvere theories.
Mimicking also the definition of model of a Lawvere theory, we obtain at once the notion of model of a partial Lawvere theory:
Definition 4.6 (Model of a partial Lawvere theory) 
A model for a partial Lawvere theory \(\)  is a CR functor \(L \colon \rightarrow \mathsf {Par}\) .
A homomorphism \(L \rightarrow L^{\prime }\)  is a lax natural transformation \(\alpha \colon L \Rightarrow L^{\prime }\) .

Definition 4.7 
The category of models and homomorphisms of a partial Lawvere theory \(\)  is denoted
\(\mathsf {pMod}_\) . As explained in Remark REF , the homomorphisms are total functions.


Partial equational theories
In order to consider interesting examples of partial Lawvere theories, we need to introduce the notion of partial equational theory. For partial structures, these are the syntactic analogue of equational theories, and yield partial Lawvere theories in a similar way to how equational theories yield Lawvere theories.
Monoidal signatures (Definition REF ) \(\Gamma \)  have unrestricted arities and coarities.
Instead, a signature \(\Sigma \)  of an equational theory (Definition REF ) has function symbols of arbitrary arities, but—considered as a monoidal signature—all coarities are 1. Partial signatures are an intermediate concept: as for equational theories, coarities \(>1\)  are redundant, but we need to admit symbols of coarity 0.
Definition 5.1 A partial signature \(\Delta \stackrel{\text{def}}{=}\Delta _0+\Delta _1\) , where \(\Delta _0\)  is the set of operations of coarity 0, and \(\Delta _1\)  is the set of operations of coarity 1. Each \(\delta : \Delta _i\)  comes with an arity \(\text{ar}(\delta ) : \) .

Differently from ordinary equational theories, we cannot use classical terms, which—as discussed in Remark REF —are tied to an underlying cartesian structure.
Instead, we adapt Recipe REF  to DCR categories, obtaining partial terms as particular string diagrams. Before we launch into formal definitions, and illustrate them with a variety of examples, let us establish some intuitions for how to read the string diagrams.

string diagrams represent partial terms, obtained through composing partial operations,

equalities and inequalities between them are understood in the sense of Kleene,

the comonoid structure \(\lbrace \raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} },\,\raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\rbrace \)  plays a similar role to that described
§

Recipe 5.2 Given a partial signature \(\Delta \) , the free DCR prop \(_\Delta \)  on \(\Delta \)  is the prop induced from the monoidal theory with

generators \((\Delta + \lbrace \raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} },\,\raisebox {.25em}{\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} },\,\raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }\rbrace )\)

equations (REF ), (REF ) and (REF ), together with
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3.5cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };\end{scope}\node [left] at (0,2*0.25) {m};\end{scope}\node [left] at (0,2*0.25) {m};\node [above] at (2.5,0.25) {=};\end{tikzpicture}\) 
for each \(\delta : \Delta _1\) , where \(\text{ar}(\delta )=m\) .


Definition 5.3 (Partial Equational Theory) 
A partial equation is a pair \((s,t)\)  where \(s,t : _\Delta (m,n)\) 
for some \(m,n:\) ; we usually write `\(s=t\) '.
A partial equational theory is a pair \((\Delta ,G)\)  where \(\Delta \)  is a partial signature and \(G\)  is a set of partial equations.

We first return to a familiar example.
Example 5.4 ((Partial) Commutative Monoids) 
We start with the monoidal theory of commutative monoids (Example REF ), where the multiplication and unit generators are re-coloured to red to avoid a clash. In models, the multiplication operation may be partially defined and the unit may be undefined. To define the partial theory of total commutative monoids, we'd need to add equations:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4cm]{\begin{scope}[yshift=1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\node at (2.75,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope} \begin{scope}[xshift=3cm]\node at (0,2*0.25) {\raisebox {.25em}{\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{tikzpicture} }};\end{scope}\node at (2.25,2*0.25) {=};\end{tikzpicture}\) 


Example 5.5 (Equational Theories) 
Any equational theory \((\Sigma ,E)\)  is an example.
One follows Recipe REF , adding equations analogous to (REF ) to specify that every generator in \(\Sigma \)  is total. The category of models of this partial theory then agrees with that of the Lawvere theory \(_{(\Sigma ,E)}\) .

The following elementary examples illustrate the novel features of partial Lawvere theories, highlighting the way in which they differ from classical (i.e., total) Lawvere theories.
Example 5.6 (Equivalence Relations) 
Consider the partial Lawvere theory consisting of a single binary operation \(R\)  with coarity 0, together with equations expressing symmetry and reflexivity:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\begin{scope}[xshift=3cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\begin{scope}[xshift=3cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture} \) 
Note that inequations of terms, as in Remark REF , do not add expressivity. As such, we may use them freely when specifying partial Lawvere theories. Transitivity is intuitively captured by the inequation on the left, which, unfolding the definition of \(\le \) , is precisely the equation on the right:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}}{\begin{scope}[yshift=-2*0.25cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}}\end{scope}{\begin{scope}[yshift=1*0.25cm]\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1 cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-2*0.25cm][wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}}\end{scope}\end{scope}\end{scope}}\node at (2.5,2*0.25) {\le };\end{tikzpicture}\hspace{71.13188pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}}{\begin{scope}[yshift=-2*0.25cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}}\end{scope}\begin{scope}[xshift=3cm]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=2*0.25cm][rounded corners=3, line width=.5pt] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (4*0.25,3*0.25);\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\begin{scope}[yscale=2.5]{\begin{scope}[yshift=-1.4*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}\end{scope}[rounded corners=3, line width=.5pt] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (4*0.25,3*0.25);{\begin{scope}[yshift=-1*0.25cm][rounded corners=3, line width=.5pt] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (4*0.25,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]\begin{scope}[yshift=1.125cm, yscale=.5][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\end{scope}\begin{scope}[xshift=2 cm]\begin{scope}[yshift=.375cm, yscale=.5][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\end{scope}\begin{scope}[xshift=2 cm]\begin{scope}[yshift=-.625cm, yscale=.5][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\) 
A model \(\mathcal {A}\)  of this theory consists of a set \(A\)  together with an equivalence relation \(=_A \subseteq A \times A\)  corresponding to the domain of definition of \(\mathcal {A}(R)\) . A morphism \(F : \mathcal {A} \rightarrow \mathcal {B}\)  is a function \(F : A \rightarrow B\)  with \(a =_A b \Rightarrow Fa =_B Fb\) , which arises from the requirement that \(F\)  is a lax transformation:
\(\begin{tikzpicture}[baseline=(current bounding box.center)][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}\begin{scope}[xshift=2cm]\begin{scope}[xscale=.75][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny F};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny F};\end{scope}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}\begin{scope}[xshift=.75 cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\tiny R};\end{scope}\end{scope}\node at (1.25,2*0.25) {\le };\end{tikzpicture}\) 
Thus, the variety corresponding to this theory is the category of Bishop sets (setoids) [21]}.

Example 5.7 (Partial Combinatory Algebras) 
A partial combinatory algebra (PCA) is a set \(A\)  with a binary partial operation \(\_\bullet \_ : A \times A \rightarrow A\) , and elements \(\mathsf {s},\mathsf {k} \in A\)  s.t. for any \(x,y,z \in A\) :

\((\mathsf {k} \bullet x) \bullet y = x\)

\(((\mathsf {s} \bullet x) \bullet y) \bullet z = (x \bullet z) \bullet (y \bullet z)\)

\((\mathsf {s} \bullet x) \bullet y\)  is defined

where “=” is Kleene equality. The partial Lawvere theory of PCAs has three generators:
\(\begin{tikzpicture}[draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny k};\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\begin{scope}[xshift=6cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{tikzpicture}\) 
and equations that ensure the totality of \(k,s\) , i.e. they define elements of the carrier, and \((iii)\) :
\(\begin{tikzpicture}[baseline=(current bounding box.center)]\begin{scope}[xscale=.75][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny k};\begin{scope}[xshift=1cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=2.5cm][densely dotted] (0,0) rectangle (1,1);\end{scope}\node at (1.75,2*0.25) {=};\end{tikzpicture}\qquad \begin{tikzpicture}[baseline=(current bounding box.center)]\begin{scope}[xscale=.75][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\begin{scope}[xshift=1cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=2.5cm][densely dotted] (0,0) rectangle (1,1);\end{scope}\node at (1.75,2*0.25) {=};\end{tikzpicture}\qquad \begin{tikzpicture}[baseline=(current bounding box.center),xscale=.75,yscale=-1][wire] (2*0.25,0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[yshift=.75cm,xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=2cm,yshift=.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm,yshift=.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=5cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[yshift=.5cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (4.25,3*0.25) {=};\end{tikzpicture}\) 
as well as equations for \((i)\)  and \((ii)\) :
\(\begin{tikzpicture}[xscale=.75,yscale=-1,baseline=(current bounding box.center)][wire] (2*0.25,0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny k};[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[yshift=.75cm,xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=2cm,yshift=.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4.5cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\begin{scope}[yshift=.25cm,xshift=4.5cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (3.75,2*0.25) {=};\end{tikzpicture}\qquad \qquad \qquad \begin{tikzpicture}[xscale=.5,yscale=-1,baseline=(current bounding box.center)][wire] (2*0.25,0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=2cm, yshift=.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm, yshift=.5cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[yshift=.5cm,xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\begin{scope}[yshift=.75cm,xscale=3][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\begin{scope}[xshift=6cm, xscale=1.25][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[yshift=1cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1cm,yshift=.5cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=1cm,yshift=1cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\begin{scope}[xshift=2cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=2cm,yshift=1cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm,yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (5,1) {=};\end{tikzpicture}\) 
The variety here is the category of PCAs and homomorphisms preserving the applicative structure.

Example 5.8 (Pairing Functions) 
Consider the partial Lawvere theory with two operations which we think of as pairing and unpairing respectively, subject to the equation on the right:
\(\begin{tikzpicture}[baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1.5 cm][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=6cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1cm][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\node at (2.5,2*0.25) {=};\end{scope}\end{tikzpicture}\) 
Models are sets equipped with a pairing function, and model morphisms map pairs to pairs. For example, \(\mathbb {N}\)  and Cantor's pairing function, or \(\Lambda \)  – the set of untyped \(\lambda \) -terms – with the usual pairing and projection functions. Note that our equation makes pairing a section, and so it is total.


Multi-Sorted Equational Theories
In this section we present a progression of multi-sorted partial Lawvere theories for categories with different kinds of structure. While our development of partial Lawvere theories has thus far focused on the single-sorted case, the move to multi-sorted theories contains no surprises, so we omit the details. The short version is that props are replaced with coloured props, and the sorting discipline changes accordingly. The examples that follow are developed incrementally: Each step adds more categorical structure to the models by adding the appropriate operations and equations to the theory, culminating in the partial Lawvere theory of cartesian closed categories.
Example 6.1 (Directed Graphs) 
We begin with the partial Lawvere theory of directed graphs, which has a sort \(O\)  of vertices and a sort \(A\)  of edges, together with source and target operations:
\(\begin{tikzpicture}[baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\node [left] at (0,2*0.25) {\scriptscriptstyle A};\node [right] at (1,2*0.25) {\scriptscriptstyle O};\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\node [left] at (0,2*0.25) {\scriptscriptstyle A};\node [right] at (1,2*0.25) {\scriptscriptstyle O};\end{scope}\begin{scope}[xshift=6cm]\begin{scope}[xscale=.5][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=1.625cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (1.25,2*0.25) {=};\node [left] at (0,2*0.25) {\scriptscriptstyle A};\node [left] at (1.75,2*0.25) {\scriptscriptstyle A};\end{scope}\begin{scope}[xshift=10cm]\begin{scope}[xscale=.5][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=1.625cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (1.25,2*0.25) {=};\node [left] at (0,2*0.25) {\scriptscriptstyle A};\node [left] at (1.75,2*0.25) {\scriptscriptstyle A};\end{scope}\end{tikzpicture}\) 
The associated variety is the category of directed graphs, as model morphisms \(F\)  must satisfy:
\(\begin{tikzpicture}[scale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny F};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny F};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\begin{scope}[xshift=6cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny F};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny F};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{scope}\end{tikzpicture}\) 

Example 6.2 (Reflexive Graphs) 
Extending Example REF , we ask that each vertex has a self-loop:
\(\begin{tikzpicture}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\node [left] at (0,2*0.25) {\scriptscriptstyle O};\node [right] at (1,2*0.25) {\scriptscriptstyle A};\begin{scope}[xshift=2.5cm]\begin{scope}[xscale=.5][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=2cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (1.25,2*0.25) {=};\node [left] at (0,2*0.25) {\scriptscriptstyle O};\node [left] at (2,2*0.25) {\scriptscriptstyle O};\end{scope}\begin{scope}[xshift=7cm,xscale=.5][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\node [left] at (0,2*0.25) {\scriptscriptstyle O};\node [right] at (1.75,2*0.25) {\scriptscriptstyle O};\begin{scope}[xshift=4.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [left] at (0,2*0.25) {\scriptscriptstyle O};\node [right] at (1,2*0.25) {\scriptscriptstyle O};\end{scope}\node at (3,2*0.25) {=};\node at (6.5,2*0.25) {=};\begin{scope}[xshift=8cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\node [left] at (0,2*0.25) {\scriptscriptstyle O};\node [right] at (2,2*0.25) {\scriptscriptstyle O};\end{scope}\end{scope}\end{tikzpicture}\) 
then morphisms of models are required to preserve the self-loop, so the associated variety is the category of reflexive graphs. Notice that along with Example REF , this could also be presented as a (total) 2-sorted Lawvere theory, since all the operations are total.

Example 6.3 (Categories) 
To capture categories we extend Example REF  with a composition operator, which is defined when the target of the first arrow matches the source of the second:
\(\begin{tikzpicture}[xscale=.8,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\node [left] at (0,0.25) {\scriptscriptstyle A};\node [left] at (0,3*0.25) {\scriptscriptstyle A};\node [right] at (1,2*0.25) {\scriptscriptstyle A};\begin{scope}[xshift=3cm,xscale=.75][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny t};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}\begin{scope}[xshift=6cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (5.5,2*0.25) {=};\end{tikzpicture}\) 
and equations insisting composition is associative and unital, with identities given by the self-loops:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[yshift=0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=red!40] at (2*0.25,2*0.25) {};\end{scope}[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3.5cm,yshift=0.25cm]\begin{scope}[yshift=-0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [cdot=red!40] at (2*0.25,2*0.25) {};\end{scope}[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node [left] at (0,2*0.25) {\scriptstyle A};\node [left] at (0,4*0.25) {\scriptstyle A};\node [left] at (0,0.25) {\scriptstyle A};\node [right] at (2,2*0.25) {\scriptstyle A};\node at (2.625,2*0.25) {=};\node [left] at (3.5,0.25) {\scriptstyle A};\node [left] at (3.5,3*0.25) {\scriptstyle A};\node [left] at (3.5,4*0.25) {\scriptstyle A};\node [right] at (5.5,3*0.25) {\scriptstyle A};\end{tikzpicture}\hspace{28.45274pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny s};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \text{id}};{[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}\begin{scope}[xshift=6cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\begin{scope}[xshift=9cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};{[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}\end{scope}\node [left] at (0,2*0.25) {\scriptstyle A};\node [right] at (4,2*0.25) {\scriptstyle A};\node [left] at (6,2*0.25) {\scriptstyle A};\node [right] at (7,2*0.25) {\scriptstyle A};\node [left] at (9,2*0.25) {\scriptstyle A};\node [right] at (13,2*0.25) {\scriptstyle A};\node at (5,2*0.25) {=};\node at (8,2*0.25) {=};\end{tikzpicture}\) 
Model morphisms are precisely functors. It is worth noting that this involves an inequality:
\(\begin{tikzpicture}[scale=.75]\begin{scope}[xshift=12cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny F};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny F};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny F};\begin{scope}[xshift=1cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (2.5,2*0.25) {\le };\end{scope}\end{tikzpicture}\) 
This states that if \(f\)  and \(g\)  are composable then so are \(Ff\)  and \(Fg\) , and in particular \(F (f \mathop {\fatsemi }g) = Ff \mathop {\fatsemi }Fg\) . If this were an equality, it would insist also that if \(Ff\)  and \(Fg\)  are composable, then so are \(f\)  and \(g\) , which is not always the case. Of course, the associated variety is the category of small categories.

Example 6.4 (blackStrict Monoidal Categories) 
Next, we extend Example REF  by asking for a functorial binary operation \(\otimes \)  on \(O\)  and \(A\)  together with a unit constant \(\top \)  of \(O\) :
\(\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\node [right] at (1,2*0.25) {\tiny O};\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm,xscale=2][densely dotted] (0,0) rectangle (1,1);\end{scope}\node at (2.25,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\node [left] at (0,3*0.25) {\tiny O};\node [left] at (0,0.25) {\tiny O};\node [right] at (1,2*0.25) {\tiny O};\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\node [left] at (0,3*0.25) {\tiny O};\node [left] at (0,0.25) {\tiny O};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4.5cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};\node [left] at (0,3*0.25) {\tiny O};\node [left] at (0,0.25) {\tiny O};\end{scope}\node at (2.75,2*0.25) {=};\end{tikzpicture}\\\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=4.5cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\end{scope}\node at (2.75,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny O};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny s};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny O};\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\\\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny O};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny t};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny O};\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]{\begin{scope}[yshift=2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}{\begin{scope}[yshift=-2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=5cm,xscale=1.25]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\end{scope}}\end{scope}\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,5*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [left] at (0,-0.25) {\tiny A};\node [right] at (3,2*0.25) {\tiny A};\end{scope}\node [left] at (0,3*0.25) {\tiny A};\node [left] at (0,5*0.25) {\tiny A};\node [left] at (0,0.25) {\tiny A};\node [left] at (0,-0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny A};\node at (3.5,2*0.25) {=};\end{tikzpicture}\) 
Additionally, we require equations to the effect that \(\otimes \)  is associative and unital:
\(\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0.25) {\tiny O};\node [left] at (0,2*0.25) {\tiny O};\node [left] at (0,4*0.25) {\tiny O};\node [right] at (2,2*0.25) {\tiny O};{\begin{scope}[yshift=1*0.25cm]\begin{scope}[xshift=5cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0) {\tiny O};\node [left] at (0,2*0.25) {\tiny O};\node [left] at (0,3*0.25) {\tiny O};\node [right] at (2,2*0.25) {\tiny O};\end{scope}\end{scope}}\node at (3.5,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0.25) {\tiny A};\node [left] at (0,2*0.25) {\tiny A};\node [left] at (0,4*0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny A};{\begin{scope}[yshift=1*0.25cm]\begin{scope}[xshift=5cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0) {\tiny A};\node [left] at (0,2*0.25) {\tiny A};\node [left] at (0,3*0.25) {\tiny A};\node [right] at (2,2*0.25) {\tiny A};\end{scope}\end{scope}}\node at (3.5,2*0.25) {=};\end{tikzpicture}\\[3mm]\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0.25) {\tiny A};\node [right] at (3,2*0.25) {\tiny A};\node at (4.5,2*0.25) {=};\begin{scope}[xshift=6cm]{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\end{scope}}{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\end{scope}}{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,3*0.25) {\tiny A};\node [right] at (3,2*0.25) {\tiny A};\end{scope}\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\end{scope}}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,3*0.25) {\tiny O};\node [right] at (2,2*0.25) {\tiny O};\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [left] at (0,2*0.25) {\tiny O};\node [right] at (1,2*0.25) {\tiny O};\end{scope}\begin{scope}[xshift=9cm]{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\end{scope}}\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,0.25) {\tiny O};\node [right] at (2,2*0.25) {\tiny O};\end{scope}\node at (3.5,2*0.25) {=};\node at (7.5,2*0.25) {=};\end{tikzpicture}\) 
Now the associated variety is the category of strict monoidal categories and strict monoidal functors.

Example 6.5 (Symmetric blackStrict Monoidal Categories) 
To capture symmetric monoidal categories, we extend Example REF  with a binary operation \(\sigma : O \otimes O \rightarrow A\)  for the braiding maps, subject to:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xshift=1 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\node [right] at (1,2*0.25) {\tiny A};\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}[wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=3cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\end{scope}\node at (1.5,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xshift=1 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\begin{scope}[xshift=5cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\node [right] at (1,2*0.25) {\tiny O};\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\\\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xshift=1 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\begin{scope}[xshift=-1 cm]{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\end{scope}\node [right] at (1,2*0.25) {\tiny O};\end{scope}\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}{\begin{scope}[yshift=2*0.25cm]\begin{scope}[xshift=3 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xshift=4 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}\end{scope}}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}}{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\begin{scope}[xshift=4 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\node at (6,2*0.25) {=};\begin{scope}[xshift=7cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\end{scope}{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}\end{tikzpicture}\\\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\end{scope}}\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny t};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2]{\begin{scope}[yshift=-1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\end{scope}\begin{scope}[yshift=1cm,xshift=7cm,yscale=-1]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\end{scope}}\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny s};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};\end{scope}}{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2]{\begin{scope}[yshift=-1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\end{scope}\end{scope}\node at (6,2*0.25) {=};{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}\begin{scope}[xshift=4 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\begin{scope}[xshift=7 cm]{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}\begin{scope}[xshift=4 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}\end{tikzpicture}\) 
This gives the variety of strict monoidal categories and symmetric strict monoidal functors.

Example 6.6 (Cartesian Restriction Categories) 
In light of REF , we can capture CR categories by extending Example REF  with operations \(\delta : O \rightarrow A\)  and \(\varepsilon : O \rightarrow A\)  corresponding to the comultiplication and counit of the comonoid structure:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta }; \node [left] at (0,2*0.25) {\scriptstyle O}; \node [right] at (1,2*0.25) {\scriptstyle A};\end{tikzpicture}:\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=2cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\node at (1.25,2*0.25) {=};\end{tikzpicture}\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\\\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon }; \node [left] at (0,2*0.25) {\scriptstyle O}; \node [right] at (1,2*0.25) {\scriptstyle A};\end{tikzpicture}:\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon };\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=3cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node at (2.25,2*0.25) {=};\end{tikzpicture}\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\hspace{10.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\begin{scope}[xshift=3cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (2*0.25,2*0.25) -- ++(2*0.25,0);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \top };\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\) 
along with equations insisting that \(\delta \)  and \(\varepsilon \)  are coherent with respect to the monoidal structure:
\(\begin{tikzpicture}[xscale=.5][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\end{scope}\begin{scope}[xshift=3cm]{\begin{scope}[yshift=-1*0.25cm][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}}{\begin{scope}[yshift=1*0.25cm][wire] (4*0.25,2*0.25) -| (2*0.25,1) -- (1,1);[wire] (2*0.25,3*0.25) -- (0,3*0.25);\node [dot] at (2*0.25,3*0.25) {};\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=3.5*0.25cm]\begin{scope}[yscale=.5][wire] (4*0.25,2*0.25) -| (2*0.25,1) -- (1,1);[wire] (2*0.25,3*0.25) -- (0,3*0.25);\node [dot] at (2*0.25,3*0.25) {};\end{scope}\end{scope}}{\begin{scope}[yshift=1.5*0.25cm]\begin{scope}[yscale=.5][wire] (4*0.25,2*0.25) -| (2*0.25,1) -- (1,1);[wire] (2*0.25,3*0.25) -- (0,3*0.25);\node [dot] at (2*0.25,3*0.25) {};\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };\end{scope}}{\begin{scope}[yshift=.5*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=3.5*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]{\begin{scope}[yshift=3*0.25cm]\begin{scope}[yscale=.5]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]{\begin{scope}[yshift=.5*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};{\begin{scope}[yshift=2.75*0.25cm]\begin{scope}[yscale=.75][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\end{scope}}\end{scope}}{\begin{scope}[yshift=-2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=5 cm]{\begin{scope}[yshift=1.75*0.25cm][wire] (0,0.25-.0625) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=6 cm]{\begin{scope}[yshift=-1.5*0.25cm]\begin{scope}[yscale=1.75][wire] (0,0.25-.035) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}}\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\hspace{71.13188pt}\begin{tikzpicture}[xscale=.75][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon };\end{scope}\begin{scope}[xshift=3cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \varepsilon };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \varepsilon };\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\) 
And finally equations for the commutative comonoid axioms, and naturality of \(\delta \) :
\(\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}}\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=7cm]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \text{id}};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}\node at (6,4*0.25) {=};\end{tikzpicture}\hspace{56.9055pt} \begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \sigma };\end{scope}\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=6cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \delta };\end{scope}}\end{scope}\node at (5,4*0.25) {=};\end{tikzpicture}\\ \begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}}\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \varepsilon };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=7cm]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \text{id}};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \varepsilon };\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\end{scope}\node at (6,4*0.25) {=};\end{tikzpicture}\hspace{28.45274pt} \begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny s};\end{scope}}\end{scope}}\end{scope}\begin{scope}[xshift=2 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}\begin{scope}[xshift=7cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}}\end{scope}\node at (6,4*0.25) {=};\end{tikzpicture}\) 
The associated variety is the category of CR categories and CR functors.

Example 6.7 (Discrete Cartesian Restriction Categories) 
REF  makes it easy to capture DCR categories by extending Example REF  with \(\mu : O \rightarrow A\)  satisfying the Frobenius and special equations: there is a [xscale=.5,baseline=(current bounding box.center)]

[iden] (0,2*0.25) – (1,2*0.25);
draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) \(\mu \);
left] at (0,2*0.25) \(O\);
right] at (1,2*0.25) \(A\);

 such that
\(\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \mu };\begin{scope}[xshift=1 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=4cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\node [left] at (0,2*0.25) {\tiny O};\end{scope}\node at (2.5,2*0.25) {=};\end{tikzpicture}\hspace{90.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \mu };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\\\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \mu };\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\begin{scope}[xshift=5cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [left] at (0,2*0.25) {\tiny O};\node [right] at (1,2*0.25) {\tiny O};\end{scope}\node at (3.5,2*0.25) {=};\end{tikzpicture}\hspace{65.0pt}\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \mu };\end{scope}\begin{scope}[xshift=2 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=2 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\node at (4.5,2*0.25) {=};\begin{scope}[xshift=6cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\node [left] at (0,2*0.25) {\tiny O};\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{tikzpicture}\\\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=4*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \mu };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};{\begin{scope}[yshift=4*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \text{id}};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=4*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=4 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}}\begin{scope}[yshift=2*0.25cm, xshift=8cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \mu };\end{scope}\begin{scope}[xshift=2 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=2 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}\begin{scope}[xshift=14cm]\begin{scope}[yscale=2][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=4*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}[draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \text{id}};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \mu };{\begin{scope}[yshift=4*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,3*0.25) {\tiny \delta };[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};\end{scope}}\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };{\begin{scope}[yshift=4*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=2][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}{\begin{scope}[yshift=2*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\begin{scope}[xshift=4 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}}\end{scope}{\begin{scope}[yshift=2*0.25cm]\node at (6.5,2*0.25) {=};\node at (12.5,2*0.25) {=};\end{scope}}\end{tikzpicture}\) 
The variety is the category of strict DRC categories and strict CR functors (since they preserve \(\mu \) ).

Example 6.8 (Cartesian Categories) 
To capture cartesian categories instead, we can extend Example REF  with one equation, ensuring that \(\varepsilon \)  is natural:
\(\begin{tikzpicture}[xscale=.5,baseline=(current bounding box.center)][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};\end{scope}\begin{scope}[xshift=2 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \varepsilon };\end{scope}\begin{scope}[xshift=3 cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}\node [left] at (0,2*0.25) {\tiny A};\begin{scope}[xshift=3 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\begin{scope}[xshift=7cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\begin{scope}[xshift=1 cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \varepsilon };\end{scope}\node [left] at (0,2*0.25) {\tiny A};\begin{scope}[xshift=1 cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}\end{scope}\node at (5.5,2*0.25) {=};\end{tikzpicture}\) 
Then by Theorem REF , this gives the variety of strict cartesian categories and strict cartesian functors.

Example 6.9 (Cartesian Closed Categories) 
Finally, to capture cartesian closed categories we extend Example REF  with an operator \(\mathsf {exp} : O \otimes O \rightarrow O\) , the idea being that \(\mathsf {exp}(A,B)\)  is the internal hom \([A,B]\) , along with an operator \(\mathsf {ev} : O \otimes O \rightarrow O\)  that gives the corresponding evaluation map:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \exp };\end{scope}\begin{scope}[xshift=-1 cm]{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\end{scope}\begin{scope}[xshift=-1 cm]{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\end{scope}\begin{scope}[xshift=-1 cm]\node [right] at (1,2*0.25) {\tiny O};\end{scope}\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \exp };\end{scope}[wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=2cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}\node at (1.25,2*0.25) {=};\end{tikzpicture}\hspace{28.45274pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xshift=1 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}\end{scope}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}\node [right] at (1,2*0.25) {\tiny A};\end{tikzpicture}:\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}[wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\begin{scope}[xshift=2cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[wire] (0,0.25) -- (2*0.25,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}\node at (1.25,2*0.25) {=};\end{tikzpicture}\\\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\begin{scope}[xshift=2cm][wire] (4*0.25,2*0.25) -| (2*0.25,1) -- (1,1);[wire] (2*0.25,3*0.25) -- (0,3*0.25);\node [dot] at (2*0.25,3*0.25) {};{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=1*0.25cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \exp };\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=-1.5*0.25cm]\begin{scope}[yscale=1.5][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}\end{scope}}\end{scope}\end{scope}\node at (1.5,2*0.25) {=};\end{tikzpicture}\hspace{42.67912pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\begin{scope}[xshift=2cm][wire] (0,3*0.25) -- (2*0.25,3*0.25);\node [dot] at (2*0.25,3*0.25) {};[draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}\node at (1.5,2*0.25) {=};\end{tikzpicture}\hspace{30.0pt}\) 
along with an operation \(\lambda \)  and equations stating, intuitively, that \(\lambda (X,A,B,f)\)  is defined precisely in case \(f : X \times A \rightarrow B\) , and yields a map \(\lambda (X,A,B,f) : X \rightarrow [A,B]\)  as in:
\(\begin{tikzpicture}[yscale=.5,baseline=(current bounding box.center)][wire] (0,5*0.25) -| (2*0.25,7*0.25) -- (0,7*0.25);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);\begin{scope}[yscale=2][wire] (3*0.25,2*0.25) -- ++(0.25,0);[fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}{\begin{scope}[yshift=2*0.25cm]\node [right] at (1,2*0.25) {\tiny A};\end{scope}}{\begin{scope}[yshift=1*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=3*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=5*0.25cm]\node [left] at (0,2*0.25) {\tiny O};\end{scope}}{\begin{scope}[yshift=-1*0.25cm]\node [left] at (0,2*0.25) {\tiny A};\end{scope}}\end{tikzpicture}\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[yscale=.75,xscale=1.25][wire] (0,5*0.25) -| (2*0.25,7*0.25) -- (0,7*0.25);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);\begin{scope}[yscale=2][wire] (3*0.25,2*0.25) -- ++(0.25,0);[fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\begin{scope}[xshift=3cm,yshift=.5cm]{\begin{scope}[yshift=2*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[yscale=1]{\begin{scope}[yshift=-1*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}\end{scope}[rounded corners=3, line width=.5pt] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (4*0.25,3*0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-4*0.25cm]\begin{scope}[xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]{\begin{scope}[yshift=1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-3*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\end{scope}{\begin{scope}[yshift=1*0.25cm]\node at (2.25,2*0.25) {=};\end{scope}}\end{tikzpicture}\\\begin{tikzpicture}[baseline=(current bounding box.center),yscale=.75][wire] (0,5*0.25) -| (2*0.25,7*0.25) -- (0,7*0.25);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);\begin{scope}[yscale=2][wire] (3*0.25,2*0.25) -- ++(0.25,0);[fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny s};\end{scope}}\end{scope}\begin{scope}[xshift=3cm]{\begin{scope}[yshift=5*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}{\begin{scope}[yshift=3*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}{\begin{scope}[yshift=2*0.25cm]\node at (2.5,2*0.25) {=};\end{scope}}\end{tikzpicture}\hspace{40.0pt}\begin{tikzpicture}[baseline=(current bounding box.center),yscale=.75][wire] (0,5*0.25) -| (2*0.25,7*0.25) -- (0,7*0.25);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);\begin{scope}[yscale=2][wire] (3*0.25,2*0.25) -- ++(0.25,0);[fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny t};\end{scope}}\end{scope}\begin{scope}[xshift=3cm]{\begin{scope}[yshift=5*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=2*0.25cm]\begin{scope}[xshift=1 cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \exp };\end{scope}\end{scope}\end{scope}}{\begin{scope}[yshift=-1*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}{\begin{scope}[yshift=2*0.25cm]\node at (2.5,2*0.25) {=};\end{scope}}\end{tikzpicture}\) 
also equations insisting that if \(f : X \times A \rightarrow B\)  then \((\lambda (X,A,B,f) \times 1)\mathop {\fatsemi }\mathsf {ev} = f\)  holds:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}[wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};{\begin{scope}[yshift=-6*0.25cm][wire] (4*0.25,2*0.25) -| (2*0.25,1) -- (1,1);[wire] (2*0.25,3*0.25) -- (0,3*0.25);\node [dot] at (2*0.25,3*0.25) {};{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=1*0.25cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}{\begin{scope}[yshift=-7*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\begin{scope}[xshift=1 cm]\begin{scope}[xscale=2]{\begin{scope}[yshift=-7*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xscale=2]{\begin{scope}[yshift=1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-6*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-4*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,2*0.25) {\tiny \text{id}};\end{scope}}\end{scope}\end{scope}\end{scope}\end{scope}{\begin{scope}[yshift=-3*0.25cm]\begin{scope}[xshift=4cm][wire] (0,5*0.25) -| (2*0.25,7*0.25) -- (0,7*0.25);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);\begin{scope}[yscale=2][wire] (3*0.25,2*0.25) -- ++(0.25,0);[fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}\begin{scope}[yshift=-3.5*0.25cm, xshift=1cm,yscale=.5]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}\end{scope}\begin{scope}[xshift=1 cm]\begin{scope}[yscale=2]{\begin{scope}[yshift=-1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\end{scope}\end{scope}\end{scope}}\begin{scope}[xshift=5cm]{\begin{scope}[yshift=-6.5*0.25cm][wire] (0,0.25) -| ++(.625,2.5*0.25) -- ++(2*0.25,0);\end{scope}}\end{scope}\begin{scope}[xshift=6cm]{\begin{scope}[yshift=-4*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\end{tikzpicture}\hspace{15.0pt}=\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=1*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\begin{scope}[xscale=2]{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=1 cm]\begin{scope}[xscale=4,yshift=0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}{\begin{scope}[yshift=-4*0.25cm]{\begin{scope}[yshift=-1*0.25cm][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}}\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-4*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}\begin{scope}[xscale=5]{\begin{scope}[yshift=-6*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[yscale=1.5]{\begin{scope}[yshift=-3*0.25cm][rounded corners=3, line width=.5pt] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (4*0.25,3*0.25);\end{scope}}\end{scope}\end{scope}\begin{scope}[xshift=3 cm]{\begin{scope}[yshift=-5*0.25cm]\begin{scope}[xscale=2][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\end{scope}}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\begin{scope}[xshift=4 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};\end{scope}}\end{scope}\begin{scope}[xshift=5 cm]\begin{scope}[yshift=.5*0.25][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}{\begin{scope}[yshift=-4.5*0.25cm]\begin{scope}[yshift=.5*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=6 cm]{\begin{scope}[yshift=-.5*0.25cm]{\begin{scope}[yshift=.5*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-3.5*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}}\end{scope}\end{tikzpicture} \) 
and that if \(g : X \rightarrow [A,B]\)  then \(\lambda (X,A,B,(g \times 1)\mathop {\fatsemi }\mathsf {ev}) = g\)  holds:
\(\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]\begin{scope}[xscale=4][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}{\begin{scope}[yshift=-6*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-2*0.25cm]\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \rotatebox {90}{\XMLaddatt {origin}{c}\scriptscriptstyle \exp }};\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=-4.5*0.25cm]\begin{scope}[yscale=1.5][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}\end{scope}}\begin{scope}[xscale=5]{\begin{scope}[yshift=-6*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\begin{scope}[xscale=2]{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\end{scope}\begin{scope}[xshift=3 cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny s};{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny t};\end{scope}}\end{scope}\begin{scope}[xshift=4 cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};{\begin{scope}[yshift=-4.5*0.25cm]\begin{scope}[yshift=.5*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}\end{scope}}\end{scope}\begin{scope}[xshift=5 cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};{\begin{scope}[yshift=-4*0.25cm][wire] (0,2*0.25) -- (2*0.25,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}\end{scope}\end{tikzpicture}\hspace{15.0pt}=\hspace{15.0pt}\begin{tikzpicture}[xscale=.75,baseline=(current bounding box.center)]{\begin{scope}[yshift=4*0.25cm]\begin{scope}[xscale=6][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}\end{scope}}\begin{scope}[yscale=2][wire] (4*0.25,0) -| (2*0.25,2*0.25) -- (1,2*0.25);[wire] (2*0.25,0.25) -- (0,0.25);\node [dot] at (2*0.25,0.25) {};\end{scope}{\begin{scope}[yshift=-5*0.25cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\begin{scope}[xshift=1 cm]{\begin{scope}[yshift=2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xshift=2 cm]{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);\node [dot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-5*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}{\begin{scope}[yshift=2*0.25cm][iden] (0,0.25) -- (1,0.25);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=3 cm]\begin{scope}[xscale=3]{\begin{scope}[yshift=3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\end{scope}}{\begin{scope}[yshift=-3*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);{\begin{scope}[yshift=-2*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,0.25) -- (1,0.25);\node [draw, fill=white, inner sep=1.5pt] at (2*0.25,0.25) {\tiny \text{id}};\end{scope}}\end{scope}}\end{scope}\begin{scope}[xshift=4 cm]\begin{scope}[yscale=1.5]{\begin{scope}[yshift=-1.675*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}\end{scope}\begin{scope}[xscale=-1][wire] (4*0.25,0.25) -| (2*0.25,3*0.25) -- (1,3*0.25);[wire] (2*0.25,2*0.25) -- (0,2*0.25);[fill=white] (0.25,0.25-.1) rectangle (3*0.25,3*0.25+.1) node[pos=.5] {\scriptscriptstyle \text{ev}};\end{scope}{\begin{scope}[yshift=-5*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [fill=white,inner sep=-1.25pt,circle] at (2*0.25,2*0.25) { \otimes };\end{scope}}\end{scope}\begin{scope}[xshift=5 cm]{\begin{scope}[yshift=-4*0.25cm][draw=none] (0,0) rectangle (1,1);[wire] (0,0.25) -- (0.25,0.25) -- (3*0.25, 3*0.25) -- (1,3*0.25);[white,wire] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (1,0.25);\end{scope}}{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,3*0.25) -- (1,3*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=6 cm]{\begin{scope}[yshift=-4*0.25cm][wire] (0,0.25) -| (2*0.25,3*0.25) -- (0,3*0.25);[wire] (2*0.25,2*0.25) -- (1,2*0.25);\node [edot] at (2*0.25,2*0.25) {};\end{scope}}{\begin{scope}[yshift=-1*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}{\begin{scope}[yshift=2*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}{\begin{scope}[yshift=3*0.25cm][rounded corners=3, line width=.5pt] (0,3*0.25) -- (0.25,3*0.25) -- (3*0.25, 0.25) -- (4*0.25,0.25);\end{scope}}\end{scope}\begin{scope}[xshift=7 cm]{\begin{scope}[yshift=-1*0.25cm][draw=none] (0,0) rectangle (1,1);[iden] (0,2*0.25) -- (1,2*0.25);\end{scope}}\end{scope}\begin{scope}[xshift=6.75 cm]\begin{scope}[yshift=-.875cm,yscale=2.25][fill=white, thin] (0.25,0.25-.15) rectangle (3*0.25,3*0.25+.15) node[pos=.5,] {\scriptscriptstyle \lambda };\end{scope}\end{scope}\end{tikzpicture} \) 
Now the associated variety is the category of strict cartesian closed categories and strict cartesian closed functors: these preserve hom-objects and, when \(\lambda (X,A,B,f)\)  is defined, satisfy \(F\lambda (X,A,B,f) = \lambda (FX,FA,FB,Ff)\) .
This presentation of cartesian closed categories is essentially due to Freyd: a version of it is given immediately after the first appearance of the notion of essentially algebraic theory in [22]}, albeit somewhat informally, and using very different syntax.


The Variety Theorem for Partial Theories
Here we classify the categories of models of partial Lawvere theories. These turn out to be exactly the locally finitely presentable (LFP) categories [23]}.
LFP categories have an important position in categorical algebra, due to deep connections with model theory [23]} and [25]}, homotopy theory [26]}, and universal algebra [23]}.
Definition 7.1 In a category \(\) , an object \(C\)  is finitely presentable if the hom-functor \((C,\,\rule {}{}\,)\)  preserves directed colimits (see [23]} for the definition).

This notion might appear obscure to the reader unfamiliar with categorical logic; [23]} contains lots of examples to help the reader build their intuition: for instance, an object of the category of sets is finitely presentable if and only if it is finite, and a (commutative) monoid is finitely presentable if and only if it admits a presentation \(\langle G\mid R\rangle \)  where both \(G\)  (set of generators) and \(R\)  (set of relations) are finite sets: this happens for many other algebraic structures, and thus motivates the definition.
Definition 7.2 (Locally finitely presentable category) 
[23]} A locally finitely presentable (LFP) category \(\)  is a cocomplete category s.t. there is a small full subcategory \(\subset \)  of finitely presentable objects, and such that every object of \(\)  is a directed colimit of objects of \(\) .

As in the classical case (Remark REF ), the most crisp statement of the variety theorem is for the unsorted case. Just as an unsorted Lawvere theory is exactly a (small) cartesian category, we define an unsorted partial Lawvere theory to be a (small) DCR category, and the corresponding notion of morphism to be a CR functor. Then:
Categories of models of partial theories are exactly LFP categories.
Indeed, we have a similar contravariant adjunction to that of Theorem REF , if \(\mathsf {LFP}\)  is a 2-category having 1-cells \(R:\rightarrow ^{\prime }\)  the right adjoint functors \(R\)  preserving directed colimits, and 2-cells all natural transformations \(\alpha : R \Rightarrow R^{\prime }\) . A motivation for this apparently peculiar choice of 1-cells can be found in our Observation REF ; it is exactly as our Definition REF , provided one replaces “sifted” colimit with “directed”.
Theorem 7.3 
There is a 2-adjunction
\(\mathsf {Th}: \mathsf {LFP} \leftrightarrows (\mathsf {DCRC}^\le )^\text{op}: \mathsf {Mod},\) 
where \(\mathsf {DCRC}^\le \)  is the 2-category of DCR categories of our Definition REF  and \(\mathsf {LFP}\)  is the 2-category of LFP categories. Moreover, the unit
of this adjunction is an equivalence, namely there is a natural equivalence of categories between \(\in \mathsf {LFP}\)  and \(\mathsf {Mod}(\mathsf {Th}())\) ,
i.e. each LFP category is equivalent to the category of models of its induced theory.

The proof of Theorem REF  is split into two parts, as illustrated below:
\(\begin{tikzcd}(\mathsf {DCRC}^\le )^\text{op} [rr, shift right] [rd, dashed, shift right=2]& & (\mathsf {Lex})^\text{op} [ld, shift left] [ll, "\fcolorbox {gray!30}{white}{1}" description, shift right] \\& \mathsf {LFP} [ru, "\fcolorbox {gray!30}{white}{2}" description, shift left] [lu, dashed] &\end{tikzcd}\) 


we show that \(\mathsf {Lex}\)  –the 2-category of categories \(\)  with finite limits, functors \(\rightarrow ^{\prime }\)  preserving finite limits, and natural transformations– is reflective in the 2-category \(\mathsf {DCRC}^\le \) .
This is the original, technical core of Theorem REF .

we connect \(\mathsf {Lex}^\text{op}\)  and \(\mathsf {LFP}\)  with a contravariant biequivalence of 2-categories. This is a classical result called Gabriel-Ulmer duality.

Composing the two, we obtain Theorem REF .
We will start from the first of the two tasks, providing an adjunction of 2-categories as follows.
\( K_t : \mathsf {DCRC}^\le \leftrightarrows \mathsf {Lex}: \mathsf {Par}\) 
We first describe the left adjoint \(K_t\) , then the right adjoint \(\mathsf {Par}\) , and conclude by showing that they define an adjunction.
Splitting Domain Idempotents
The functor \(K_t\)  arises via a modified Karoubi envelope, also called Cauchy completion in [31]}.
Recall that an idempotent \(a : A \rightarrow A\)  in a category splits if there is a commutative diagram
\(\begin{tikzcd}& X [r,"s"] & A \\X [r,"s"^{\prime }] [ur,"1_X"] & A [u,"r"] [ur,"a"^{\prime }]\end{tikzcd}\) 
Restriction categories in which all of the domain idempotents split are called split restriction categories. An example is \(\mathsf {Par}()\) : for any arrow \((m,f) : A \rightarrow B\) , \(\overline{(m,f)} = (m,m) : A \rightarrow A\)  splits with \(s = (1,m)\)  and \(r = (m,1)\) . Notice that this means the domain of definition of \((m,f)\)  is a subobject of \(A\) . This is a good way to think of split domain idempotents in general: for \(\overline{f}\)  to be split in a restriction category is for the domain of definition of \(f : A \rightarrow B\)  to be a subobject of \(A\) .
For any restriction category \(\)  we can construct a split restriction category \(K()\)  that contains \(\)  as a subcategory.
Its subcategory of total maps \(K_t()\)  is of particular interest.
Definition 7.4 Let \(\)  be a DCRC. Then \(K_t()\)  is the category where

objects are pairs \((A,a)\)  with \(A\)  an object of \(\)  and \(a : A \rightarrow A\)  a domain idempotent in \(\) ;

arrows \(f : (A,a) \rightarrow (B,b)\)  are arrows \(f : A \rightarrow B\)  of \(\)  such that \(\overline{f} = a\)  and \(f\mathop {\fatsemi }b = f\) ;

composition is given by composition in \(\) ;

The identity on \((A,a)\)  is given by \(a\) .


It is routine to verify that this forms a category.
Crucially, if \(\)  is a DCRC, then the subcategory \(K_t()\)  of total maps of \(K()\)  has finite
limits [3]}:
Lemma 7.5 For any DCRC \(\) , \(K_t()\)  has finite limits.

We now show that this extends to a 2-functor \(K_t : \mathsf {DCRC}^\le \rightarrow \mathsf {Lex}\) . If \(\)  and \(\)  are DCRCs and \(F : \rightarrow \)  is a CR functor, then there is a functor \(K_t(F) : K_t() \rightarrow K_t()\)  defined by \(K_t(F)(A,a) = (FA,Fa)\)  on objects and \(K_t(F)(f) = f\)  on arrows. It follows from our characterization of CR functors in terms of the partial Frobenius algebra structure that \(K_t(F)\)  preserves finite limits, giving the action of our 2-functor \(K_t\)  on 1-cells. The action of \(K_t\)  on 2-cells is given as follows:
Lemma 7.6 If \(F,G : \rightarrow \)  are CR functors between DCR categories and \(\alpha : F \rightarrow G\)  is a lax transformation, define \(K_t(\alpha ) : K_t(F) \rightarrow K_t(G)\)  by letting \(K_t(\alpha )\)  at \((A,a)\)  in \(K_t()\)  be:
\( K_t(\alpha )_{(A,a)} = Fa\mathop {\fatsemi }\alpha _A : (FA,Fa) \rightarrow (GA,Ga) \) 
Then \(K_t(\alpha )\)  is a natural transformation.

At this point we need only show that \(K_t\)  preserves composition and identities for 1-cells and 2-cells, which in both cases is straightforward.
Lemma 7.7 \(K_t : \mathsf {DCRC}^\le \rightarrow \mathsf {Lex}\)  is a 2-functor.


Partial Functions Revisited
Here we show that the \(\mathsf {Par}\)  construction (§REF ) also extends to a 2-functor \(\mathsf {Par} : \mathsf {Lex} \rightarrow \mathsf {DCRC}^\le \) . If \(\mybb {C}\)  and \(\mybb {D}\)  are categories with finite limits and \(F : \mybb {C} \rightarrow \mybb {D}\)  is a finite-limit preserving functor, then we obtain a CR functor \(\mathsf {Par}(F) : \mathsf {Par}(\mybb {C}) \rightarrow \mathsf {Par}(\mybb {D})\) , defined on objects by \(\mathsf {Par}(F)(A) = F(A)\) , and on arrows by
\(\begin{tikzcd}& X [ld,"m"^{\prime }] [rd,"f"]\\A && B\end{tikzcd}\stackrel{\mathsf {Par}(F)}{\longmapsto }\begin{tikzcd}& FX [ld,"Fm"^{\prime }] [rd,"Ff"]\\FA && FB\end{tikzcd}\) 
Since \(F\)  preserves finite limits, we have that \(\mathsf {Par}(F)(\delta _A) = (F1_A,F\Delta _A) = (1_{FA},\Delta _{FA}) = \delta _{FA} = \delta _{\mathsf {Par}(F)(A)}\)  and \(\mathsf {Par}(F)(\varepsilon _A) = (F1_A, F!_A) = (1_{FA},!_{FA}) = \varepsilon _{\mathsf {Par}(F)(A)}\) , so \(\mathsf {Par}(F)\)  preserves the CR structure. This defines the action of \(\mathsf {Par}\)  on 1-cells. We present the action of \(\mathsf {Par}\)  on 2-cells as a lemma:
Lemma 7.8 If \(F,G : \mybb {C} \rightarrow \mybb {D}\)  are finite limit preserving functors between categories with finite limits and \(\alpha : F \rightarrow G\)  is a natural transformation, define \(\mathsf {Par}(\alpha ) : \mathsf {Par}(F) \rightarrow \mathsf {Par}(G)\)  by defining the component of \(\mathsf {Par}(\alpha )\)  at \(A\)  in \(\mybb {C}\)  to be:
\(\scriptsize \begin{tikzcd}& FA [d,phantom,"\tiny \mathsf {Par}(\alpha )_A"] [ld,"1_{FA}"^{\prime }] [dr,"\alpha _A"] \\FA &\text{}& GA\end{tikzcd}\) 
Then \(\mathsf {Par}(\alpha ) : \mathsf {Par}(F) \rightarrow \mathsf {Par}(G)\)  is a lax transformation.

It remains only show that \(\mathsf {Par}\)  preserves composition and identities at the level of 1-cells and 2-cells, which is immediate in both cases. We therefore have:
Lemma 7.9 \(\mathsf {Par}: \mathsf {Lex}\rightarrow \mathsf {DCRC}^\le \)  is a 2-functor.


Adjointness
The following result is original, and builds on [5]}; however, there the 2-cells of the categories involved are different.
Theorem 7.10 
There is a 2-adjunction \(K_t : \mathsf {DCRC}^\le \leftrightarrows \mathsf {Lex}: \mathsf {Par}\) .

It is worth describing the unit and counit of our adjunction. The unit \(\eta : 1 \rightarrow \mathsf {Par}\cdot K_t \)  is given by the canonical inclusion \(\eta _: \rightarrow \mathsf {Par}(K_t())\)  defined by
\(A \stackrel{f}{\rightarrow } B \hspace{28.45274pt} \stackrel{\eta _}{\longmapsto }\begin{tikzcd}& (A,\overline{f}) [ld,"\overline{f}"^{\prime }] [rd,"f"] \\(A,1_A) && (B,1_B)\end{tikzcd}\) 
The counit \(\varepsilon : K_t\cdot \mathsf {Par}\rightarrow 1\)  is defined in terms of the equivalence of categories \(K() \simeq \)  between any split restriction category \(\)  and the result of formally splitting its domain idempotents. In particular, since \(\mathsf {Par}()\)  is always split, we obtain an equivalence of categories \(K(\mathsf {Par}()) \simeq \mathsf {Par}()\) . Restricting this to the subcategories of total maps gives defines our counit \(\varepsilon _: K_t(\mathsf {Par}()) \simeq \) . In particular, the fact that the counit is a natural equivalence gives:
Lemma 7.11 \(\mathsf {Lex}\)  is a reflective (2-)subcategory of \(\mathsf {DCRC}^\le \) .


Gabriel-Ulmer duality
To complete the triangle (REF ), we recall a theorem first shown by P. Gabriel and F. Ulmer [34]}, establishing a contravariant equivalence between the 2-category \(\mathsf {LFP}\)  of locally finitely presentable categories and the 2-category \(\mathsf {Lex}\)  of categories with finite limits.
The duality asserts that a locally finitely presentable category \(\)  can be reconstructed from its subcategory \(_{\omega }\)  of finitely presentable objects. A good reference for the proof is [35]}.
Theorem 7.12 (Gabriel-Ulmer duality)  
There is a biequivalence of 2-categories
\(\mathsf {Lex}^\text{op}\leftrightarrows \mathsf {LFP}\) 
between \(\mathsf {Lex}\) , the 2-category of small categories with finite limits, where 1-cells are functors preserving finite limits and 2-cells are the natural transformations, and \(\mathsf {LFP}\) , the 2-category of locally finitely presentable categories, where 1-cells are right adjoints preserving directed colimits.


Sorted Gabriel-Ulmer duality
A similar version of the above theorem holds if, instead of considering theories of all possible sorts, we fix once and for all a single cardinality for the sorts \(\mathfrak {S}\) . Such “relative” version of Gabriel-Ulmer duality is useful to recover the classical Lawvere-style approach of single- and many-sorted theories.
Definition 7.13 
We call \(L\mathfrak {S}\)  the free category with finite limits over the discrete set \(\mathfrak {S}\) . When \(\mathfrak {S}\)  is the singleton we will use the shortened notation \(L1\) .

Definition 7.14 
A \(\mathfrak {S}\) -sorted category with finite limits \((, p)\)  is an object in \((\mathsf {Lex})^\text{op}{/L\mathfrak {S}}\)  whose specifying functor \(p: L\mathfrak {S}\rightarrow \)  is bijective on objects. \((\mathfrak {S}\text{-}\mathsf {Lex})^\text{op}\)  is the full 2-subcategory of \(\mathfrak {S}\) -sorted categories with finite limits.

Definition 7.15 
A \(\mathfrak {S}\) -sorted locally finitely presentable category \((, U)\)  is an object in \(\mathsf {LFP}{/[\mathfrak {S},\mathsf {Set}]}\)  whose specifying functor \(U: \rightarrow [\mathfrak {S},\mathsf {Set}]\)  is conservative. \((\mathfrak {S}\) -\(\mathsf {LFP})^\text{op}\)  is the full 2-subcategory of \(\mathfrak {S}\) -sorted locally finitely presentable categories.

Theorem 7.16 (Sorted Gabriel-Ulmer duality) 
There is a biequivalence of 2-categories
\(\mathsf {Mod}_{\mathfrak {S}}: (\mathfrak {S}\text{-}\mathsf {Lex})^\text{op}\leftrightarrows \mathfrak {S}\text{-}\mathsf {LFP}:\mathsf {Th}_\mathfrak {S}.\) 


Sorted partial variety theorem
We can use the sorted version of Gabriel-Ulmer duality to infer the sorted version of the syntax-semantics duality for multi-sorted partial Lawvere theories.
Theorem 7.17 There is an 2-adjunction, whose unit is an equivalence,
\( \mathfrak {S}\text{-}\mathsf {LFP} \leftrightarrows (\mathfrak {S}\text{-}\mathsf {pLaw})^\text{op},\) 
where \(\mathfrak {S}\text{-}\mathsf {pLaw}\)  is the 2-category of “\(\mathfrak {S}\) -sorted partial Lawvere theories”, understood as the analogue of Remark REF  for partial theories (see Definition REF ), and \(\mathfrak {S}\text{-}\mathsf {LFP}\)  is the 2-category of \(\mathfrak {S}\) -sorted locally finitely presentable categories.

The proof is divided into intermediate steps: each tag on the following two diagrams indicates the section where the proof of the adjunction, or equivalence, is given.
max width=0.925
\(\begin{tikzcd}[ampersand replacement=\&](\mathfrak {S}\text{-}\mathsf {pLaw})^\text{op}[rr, shift right] [rd, dashed, shift right] \& \& (\mathfrak {S}\text{-}\mathsf {Lex})^\text{op}[ll, "\scriptsize \fcolorbox {gray!30}{white}{\star }" description, shift right] [ld, shift left] \& \& (\mathsf {DCRC}^\le )^\text{op}[rr, shift right] [rd, dashed, shift right=2] \& \& (\mathsf {Lex})^\text{op}[ld, shift left] [ll, "\scriptsize \fcolorbox {gray!30}{white}{\ref {LexDCRC}}" description, shift right] \\\& \mathfrak {S}\text{-}\mathsf {LFP} [ru, "\scriptsize \fcolorbox {gray!30}{white}{\ref {sortedGU}}" description, shift left] [lu, dashed, shift right] \& \& \& \& \mathsf {LFP} [ru, "\scriptsize \fcolorbox {gray!30}{white}{\ref {GU}}" description, shift left] [lu, dashed] \&\end{tikzcd}\) 

The claim in \((\star )\)  is the only one that needs to be proven. Yet it is also the most trivial one. We will deduce it directly from REF . Indeed if \(\mathsf {Lex}\)  is reflective in \(\mathsf {DCRC}^\le \) , \((\mathsf {Lex})^\text{op}/L\mathfrak {S}\)  is coreflective in \((\mathsf {DCRC}^\le )^\text{op}/\mathsf {Par}(L\mathfrak {S}) \) , now observe that \(\mathsf {Par}(L\mathfrak {S})\)  is precisely the free discrete cartesian restriction category over \(\mathfrak {S}\) . The desired result follows passing to functors bijective on objects in the slice.
Observation 7.18 
In analogy with REF , we can show that sorted partial Lawvere theories have free models. For the single-sorted case, let \(p: \mathsf {Par}(^\text{op}) \rightarrow \)  be a partial Lawvere theory. Indeed we can look at it as a morphism in \(\mathsf {DCRC}^\le \) , then the previous theorem produces an adjunction \(F \dashv \mathsf {Mod}_{p}\)
\(F: \mathsf {Mod}_{\mathsf {Par}(^\text{op})} \leftrightarrows \mathsf {Mod}_{} : \mathsf {Mod}_{p}.\) 
The functor \(\mathsf {Mod}_{p}\)  coincides with the forgetful functor. Its left adjoint \(F\)  provides free objects.


Conclusions and future work
We introduced partial Lawvere theories and their associated notion of partial equational theory. Our definitions are guided by the appropriate universal property, replacing cartesian categories with discrete cartesian restriction categories. Knowing the right universal property determines our choice of syntax, isolating the correct class of string diagrams that replace classical terms. This enables the standard methodology of presenting a theory by means of a signature and equations, while avoiding ad-hoc notations and eliminating the subtleties of reasoning about partial structures.
The extension is conservative: every equational theory yields a partial equational theory such that the categories of models coincide, even though our models are in \(\mathsf {Par}\)  rather than in \(\mathsf {Set}\) . The recently proposed Frobenius theories [36]} take their models in the category of relations \(\mathsf {Rel}\) , and are guided by the structure of cartesian bicategories of relations [37]}. Every partial equational theory yields a Frobenius theory and again, the categories of models coincide. We feel that our notion is a sweet-spot. First, we have shown that our notion of partial theories is expressive, capturing a number of important examples. Second, we retain much of the richness of the semantic picture, via a canonical variety theorem and existence of free models.
There is much future work. The fact that the syntax introduced here is inherently partial makes it well-suited to applications in computing. In particular there is an evident notion of computable model for partial Lawvere theories, namely those models valued in the category of sets and partial recursive functions. The corresponding computable varieties seem to be interesting for programming language semantics, and therefore worthy of study. A further step would be the lifting of this situation to a more synthetic category of computable functions, such as a Turing category [38]} or monoidal computer [39]}.
An important part of categorical universal algebra is played by monads, a point of view that we have not considered here.
Indeed, Lawvere theories can be seen as finitary monads [40]}, with the category of algebras giving the associated variety. This connection has been a fruitful one, relating areas of research that are, on the surface, very different, see e.g. [41]}, [42]}, [43]}. A natural question is whether there is an analogous approach for partial algebraic theories. We conjecture that there is, with certain formal monads [44]} in the 2-category \(\mathsf {DCRC}^\le \)  playing the role of finitary monads.
We expect that other constructions of categorical universal algebra (e.g. [45]}, [46]}) will have corresponding partial accounts.
