& \mC(X, Y) \otimes \mC(Y, Y) \ar{u}[xshift=-1.5pc,yshift=0.0pc,rotate=-60]{\le}
\end{tikzcd}
\]

So although a hom-functor $\freccia{\mC}{\mC(A,-)}{\Rel}$ preserves binary composition strictly (by strict associativity), it preserves identities only laxly (by the lower triangle),
In general, let us say that $F : \mC \to \Rel$ is identity-lax, if it is a lax functor that preserves binary composition on the nose, and identities at least laxly,

\[
\id_{F(X)} \subseteq F(\id_X).
\]

Notice that Proposition <ref> can be generalized in the enriched case since, whenever $\mC$ is a preorder-enriched gs-monoidal category, every hom-functor $\mC(A,-) : \mC \to \Preord$ is a lax gs-monoidal 2-functor (where $\Preord$ denotes the (cartesian monoidal)  category of preordered sets).

For every preorder-enriched gs-monoidal category $\mC$ and parallel arrows $f, g : X \to Y$ in $\mC$, we have that

* $f = g$ if and only if $F(f) = F(g)$ for every lax gs-monoidal 2-functor $F : \mC \to \Preord$;

* $f \leq g$ if and only if $F(f) \leq F(g)$ for every lax gs-monoidal 2-functor $F : \mC \to \Preord$.

The first point follows from Proposition <ref>. Regarding the second point: if $F(f) \leq F(g)$ for every lax gs-monoidal 2-functor $F : \mC \to \Preord$,  then we have that $\mC(X,f)\leq \mC(X,g)$, i.e.  $\mC(X,f)(h)\leq \mC(X,g)(h)$ for every $h\in \mC(X,X)$. Therfore we can conclude that $f\leq g$ since $f=\mC(X,f)(\id_X)$ and $g=\mC(X,g)(\id_X)$.

For every preorder-enriched gs-monoidal category $\mC$ and parallel arrows $f, g : X \to Y$ in $\mC$, we have that $f \approx g$ if and only if $F(f) = F(g)$ for every lax gs-monoidal 2-functor $F : \mC \to \Preord$.

I have to finish to write this section

§.§ Completeness for preorder equivalence

I think that this subsection is redundant, since Proposition <ref> easily generalizes to a stronger result in the enriched case: $f \le g$ if and only if $F(f) \le F(g)$ for every lax gs-monoidal 2-functor into the (cartesian monoidal) category of preordered sets. This should work for preordered gs in general, not just oplax cartesian

The main goal of this section is to provide a completeness result for the notion of preorder equivalence. In particular, we show that for any oplax cartesian category $\mC$ two arrows $\freccia{A}{f,g}{B}$ are gs-monoidal equivalent if and only if for any lax gs-monoidal lax functor $\freccia{\mC}{F}{\Rel}$ we have that $F(f)=F(g)$.
Notice that with lax gs-monoidal lax functors we mean a lax monoidal lax functor $\freccia{\mC}{F}{\mA}$ such that $\nabla_{FA}\leq F(\nabla_A)$ and $!_{FA}\leq F(!_A)$ for every object $A$ of $\mC$.

For this purpose, let us consider an oplax cartesian category $\mC$. We define a  lax gs-monoidal lax functor $\freccia{\mC}{H_{\mC}}{\Rel}$ as follows

* for every object $A$ of $\mC$, $H(A):=\mC/ A$ (the set of arrows of $\mC$ whose codomain is $A$);

* for every arrow $\freccia{A}{f}{B}$, $\freccia{H(A)}{H(f)}{H(B)}$ is defined as  $h H(f)g\iff g\leq fh$.

For every oplax cartesian category $\mC$,  $\freccia{\mC}{H_{\mC}}{\Rel}$ is a lax gs-monoidal lax functor.

See Appendix <ref>.

The lax functor  $\freccia{\mC}{H_{\mC}}{\Rel}$ is used to provide a completeness result for preorder equivalence.

Let $\mC$ be an oplax cartesian category. Two arrows of $\mC$ are preorder equivalent if and only if for every lax gs-monoidal lax functor $\freccia{\mC}{F}{\mathsf{Rel}} $ we have $F(f)=F(g)$.

Let us consider two arrows $\freccia{A}{f}{B}$ and $\freccia{A}{g}{B}$. If $g$ and $f$ are preorder equivalent, then $F(g)=F(f)$ because a lax gs-functor preserves the order and $\mathsf{Rel}$ is poset-enriched.

Now suppose that  $F(g)=F(f)$ for every lax gs-functor $\freccia{\mC}{F}{\mathsf{Rel}} $. In particular, we have that $H_{\mC}(f)=H_{\mC}(g)$ where $\freccia{\mC}{H_{\mC}}{\mathsf{Rel}} $ is the canonical lax gs-monoidal lax functor defined in the previous proposition. Now we show $H_{\mC}(f)=H_{\mC}(g)$ implies $g$ and $f$ are preorder equivalent. Notice when $H_{\mC}(f)=H_{\mC}(g)$, in particular, we have that $\id_AH_{\mC}(f)f$ implies that  $\id_AH_{\mC}(g)f$. This means that $g\leq f$. Similarly, we have that  $\id_AH_{\mC}(g)g$ implies that  $\id_AH_{\mC}(f)g$, i.e. $f\leq g$. Therefore, we can conclude that $f$ and $g$ are preorder equivalent.

§ CONCLUSION AND FUTURE WORKS

After a string-diagrammatic presentation of gs-monoidal categories and a few related structures.
our paper introduces their preorder-enriched extensions, and in particular oplax cartesian categories.

We show that these categories represent a core language for relations and partial functions,
hence fitting in the current interest for the use of visual languages in modelling computational
formalisms (see e.g. [45, 46] and the references therein).

Such an interest in confirmed by our proof that such categories naturally arise in terms of Kleisli categories
and span categories, thus providing a large number of potential case studies.

As for the former, we also show that the canonical functor from the Kleisli category of a given monad
back to the original category has a gs-monoidal structure.

Finally, we turn to functorial completeness, showing it for oplax cartesian categories
with respect to certain mappings into $\Rel$, thus generalising [5].

Future work will focus on completeness with respect to $\Rel$, in order to strengthen our result
to genuine functors instead of lax-on-identities ones, following ideas in [47].

We will also attempt to establish a stronger connection between the constructions involving Kleisli and span categories.
Furthermore, it could be interesting to address the traced monoidal case, as well as take into account the whole 2-categorical structure of $\mathbf{Span}(\mC)$,
for a presentation of graph rewriting and of inequational deduction for relational algebras, investigated in a
set-theoretical flavour in [4, 48],
and recently (at least for the diagrammatic presentation of the monoidal closed case) in [49].

From a practical standpoint, we believe that our completeness results will find application in rewriting theory. The idea is that a completeness result makes it possible to derive new properties of a rewriting system in a straightforward manner, simply by analysing rewriting in a standard category like the one of preordered sets as in Theorem <ref>. Indeed, in rewriting the oplax structure amounts to changing the topology of the underlying graph [4] so that the analysis of confluence could be performed simply by looking at the associated preorder in the model. Given that term graph rewriting is frequently used in functional programming language implementations, where the sharing of sub-terms is a key issue, our result may be concretely useful in improving such language implementations.

§ DECLARATIONS

Author's Contribution Tobias Fritz, Fabio Gadducci, Davide Trotta and Andrea Corradini contributed equally to this work.
Conflict of interestThe authors declare that they have no conflict of interest.
Availability of Data and MaterialsNot applicable
FundingTobias Fritz acknowledges funding
by the Austrian Science Fund (FWF) through the project “P 35992-N”.
Andrea Corradini, Fabio Gadducci and Davide Trotta acknowledge funding
by the Italian Ministry of Education, University and Research (MIUR) through the project PRIN 20228KXFN2 “STENDHAL”.

#1ISBN #1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1<https://doi.org/#1>et al.#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1#1<><#>1#1#1#1#1#1#1#1#1#1#1#1#1#1PreBibitemsHook

[1]

Gadducci, F.:
On the algebraic approach to concurrent term rewriting.
PhD thesis,
University of Pisa

[2]

Corradini, A.,
Gadducci, F.:
A 2-categorical presentation of term graph rewriting.
In: Moggi, E.,
Rosolini, G. (eds.)
CTCS 1997.
vol. 1290,
pp. 87–105.

[3]

Corradini, A.,
Gadducci, F.:
An algebraic presentation of term graphs, via gs-monoidal categories.
Applied Categorical Structures

[4]

Corradini, A.,
Gadducci, F.:
Rewriting on cyclic structures: equivalence between the operational
and the categorical description.
RAIRO - Theoretical Informatics and Applications - Informatique
Théorique et Applications

[5]

Corradini, A.,
Gadducci, F.:
A functorial semantics for multi-algebras and partial algebras, with
applications to syntax.
Theoretical Computer Science

[6]

Fox, T.:
Coalgebras and cartesian categories.
Communications in Algebra

[7]

Lawvere, F.W.:
Functorial semantics of algebraic theories.
Proceedings of the National Academy of Sciences

[8]

Carboni, A.,
Walters, R.F.C.:
Cartesian bicategories I.
Journal of Pure and Applied Algebra

[9]

Carboni, A.,
Kelly, G.M.,
Walters, R.F.C.,
Wood, R.J.:
Cartesian bicategories II.
Theory and Applications of Categories

[10]

Bonchi, F.,
Seeber, J.,
Sobociński, P.:
Graphical conjunctive queries.
In: Ghica, D.,
Jung, A. (eds.)
CSL 2018.
vol. 119,
pp. 13–11323.
Schloss Dagstuhl–Leibniz-Zentrum für Informatik,

[11]

Bonchi, F.,
Pavlovic, D.,
Sobociński, P.:
Functorial semantics for relational theories.

[12]

Fong, B.,
Spivak, D.:
Regular and relational categories: Revisiting `Cartesian bicategories I'.

[13]

Golubtsov, P.V.:
Axiomatic description of categories of information transformers.
Problems of Information Transmission

[14]

Cho, K.,
Jacobs, B.:
Disintegration and Bayesian inversion via string diagrams.
Mathematical Structures in Computer Science

[15]

Fritz, T.:
A synthetic approach to Markov kernels, conditional independence and
theorems on sufficient statistics.
Advances in Mathematics

[16]

Cockett, J.R.B.,
Lack, S.:
Restriction categories III: colimits, partial limits and
Mathematical Structures in Computer Science

[17]

Cockett, J.R.B.,
Lack, S.:
Restriction categories I: categories of partial maps.
Theoretical Computer Science

[18]

Cockett, J.R.B.,
Lack, S.:
Restriction categories II: partial map classification.
Theoretical Computer Science

[19]

Aguiar, M.,
Mahajan, S.:
Monoidal Functors, Species and Hopf Algebras.
CRM Monograph Series,
vol. 29,
p. 784.
American Mathematical Society,
Providence, RI

[20]

Selinger, P.:
A survey of graphical languages for monoidal categories.
In: Coecke, B. (ed.)
New Structures for Physics.
Lecture Notes in Physics,
vol. 813,
pp. 289–355.

[21]

Fong, B.,
Spivak, D.:
Supplying bells and whistles in symmetric monoidal categories.

[22]

Robinson, E.,
Rosolini, G.:
Categories of partial maps.
Information and Computation

[23]

Fritz, T.,
Gonda, T.,
Perrone, P.,
Rischel, E.F.:
Representable Markov categories and comparison of statistical
experiments in categorical probability.
Theoretical Computer Science

[24]

Bruni, R.,
Gadducci, F.:
Some algebraic laws for spans (and their connections with
In: Kahl, W.,
Parnas, D.L.,
Schmidt, G. (eds.)
RelMiS 2001.
vol. 44,
pp. 175–193.

[25]

Carboni, A.:
Bicategories of partial maps.
Cahiers de Topologie et Géométrie Différentielle Catégoriques

[26]

Kelly, G.M.:
Basic concepts of enriched category theory.
Reprints in Theory and Applications of Categories

[27]

Moggi, E.:
Computational lambda-calculus and monads.
In: LICS 1989,
pp. 14–23.
IEEE Press,
CA, USA

[28]

Moggi, E.:
Notions of computation and monads.
Information and Computation

[29]

Borceux, F.:
Handbook of Categorical Algebra 2: Categories and Structures.
Encyclopedia of Mathematics and its Applications,
vol. 51.
Cambridge University Press,

[30]

MacLane, S.,
Moerdijk, I.:
Sheaves in Geometry and Logic. A First Introduction to Topos Theory.
New York

[31]

Makkai, M.,
Reyes, G.:
First Order Categorical Logic.
Lecture Notes in Mathematics,
vol. 611.
Berlin-New York

[32]

Lambek, J.,
Scott, P.J.:
Introduction to Higher Order Categorical Logic.
Cambridge University Press,

[33]

Tanaka, M.:
Pseudo-distributive laws and a unified framework for variable binding.
PhD thesis,
The University of Edinburgh

[34]

Giry, M.:
A categorical approach to probability theory.
In: Banaschewski, B. (ed.)
Categorical Aspects of Topology and Analysis.
Lecture Notes in Mathematics,
vol. 915,
pp. 68–85.
Berlin-New York

[35]

Jacobs, B.:
From probability monads to commutative effectuses.
Journal of Logical and Algebraic Methods in Programming

[36]

Kock, A.:
Monads on symmetric monoidal closed categories.
Archiv der Mathematik

[37]

Kock, A.:
Bilinearity and cartesian closed monads.
Mathematica Scandinavica

[38]

Jacobs, B.:
Semantics of weakening and contraction.
Annals of Pure and Applied Logic

[39]

Heunen, C.,
Kammar, O.,
Staton, S.,
Yang, H.:
A convenient category for higher-order probability theory.
In: LICS 2017,
p. 12.
IEEE Press,
Piscataway, NJ

[40]

Guitart, R.:
Tenseurs et machines.
Cahiers de Topologie et Géométrie Différentielle

[41]

Fritz, T.,
Perrone, P.,
Rezagholi, S.:
Probability, valuations, hyperspace: Three monads on Top and the
support as a morphism.
Math. Struct. Comput. Sci.

[42]

Day, B.:
On closed categories of functors.
In: Reports of the Midwest Category Seminar, IV.
Lecture Notes in Mathematics,
vol. 137,
pp. 1–38.

[43]

Day, B.J.:
Construction of biclosed categories.
PhD thesis,
University of New South Wales

[44]

Mandell, M.A.,
May, J.P.,
Schwede, S.,
Shipley, B.:
Model categories of diagram spectra.
Proceedings of the London Mathematical Society

[45]

Bonchi, F.,
Sobociński, P.,
Zanasi, F.:
A survey of compositional signal flow theory.
In: Goedicke, M.,
Neuhold, E.J.,
Rannenberg, K. (eds.)
Advancing Research in Information and Communication Technology.
IFIP AICT,
vol. 600,
pp. 29–56.

[46]

Bonchi, F.,
Gadducci, F.,
Kissinger, A.,
Sobociński, P.,
Zanasi, F.:
String diagram rewrite theory I: rewriting with Frobenius
Journal of the ACM

[47]

Gadducci, F.:
A term-graph syntax for algebras over multisets.
In: Corradini, A.,
Montanari, U. (eds.)
WADT 2008.
vol. 5486,
pp. 152–165.
Berlin, Heidelberg

[48]

Corradini, A.,
Gadducci, F.,
Kahl, W.,
König, B.:
Inequational deduction as term graph rewriting.
In: Mackie, I.,
Plump, D. (eds.)
TERMGRAPH 2002.
vol. 72,
pp. 31–44.

[49]

Alvarez-Picallo, M.,
Ghica, D.,
Sprunger, D.,
Zanasi, F.:
Rewriting for monoidal closed categories.
In: Felty, A. (ed.)
FSCD 2022.
vol. 228,
pp. 29–12920.
Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

[50]

Kock, A.:
Strong functors and monoidal monads.
Archiv der Mathematik

[51]

Kock, A.:
Monads on symmetric monoidal closed categories.
Archiv der Mathematik

§ LAX/OPLAX/BILAX MONOIDAL FUNCTORS

This section recalls the definitions of lax, colax, and bilax monoidal functors, see e.g. [19].
Throughout, $\mC$ and $\mD$ are symmetric monoidal categories with tensor functor $\otimes$ and monoidal unit $I$, and we assume that
$\otimes$ strictly associates without loss of generality in order to keep the diagrams simple.
Left and right unitors are denoted by $\lambda$ and $\rho$, respectively[Strict unitality could also be assumed, but that choice would make some diagrams potentially confusing.], and braidings by $\gamma$.

A functor $\freccia{\mC}{F}{\mD}$ is lax monoidal if it is equipped with a natural transformation

\[\freccia{\otimes \circ \, (F\times F)}{\psi}{F\circ \otimes}\]

and an arrow $\freccia{I}{\psi_0}{F(I)}$ such that the associativity diagrams

\[\begin{tikzcd}[column sep=3ex]
{F(A)\otimes F(B)\otimes F(C)} &&& {F(A)\otimes F(B\otimes C)} \\
\\
{F(A\otimes B)\otimes F(C)} &&& {F(A\otimes B\otimes C)}
\arrow["{\id\otimes \,\psi_{B,C}}", from=1-1, to=1-4]
\arrow["{\psi_{A,B}\otimes {}\id}"', from=1-1, to=3-1]
\arrow["{\psi_{A\otimes B,C}}"', from=3-1, to=3-4]
\arrow["{\psi_{A,B\otimes C}}", from=1-4, to=3-4]
\end{tikzcd}\]

and the unitality diagrams commute

\begin{equation}
\label{eq:lax_monoidal_unitality}
\begin{tikzcd}[column sep=1ex]
{I\otimes F(A)} && F(A) && {F(A)\otimes  I} && F(A) \\
\\
{F(I)\otimes F(A)} && {F(I\otimes A)} && {F(A)\otimes F(I)} && {F(A\otimes  I).}
\arrow["{\psi_{I,A}}"', from=3-1, to=3-3]
\arrow["{F(\lambda_A)}", from=1-3, to=3-3]
\arrow["{\psi_0\otimes {}\id}"', from=1-1, to=3-1]
\arrow["{\lambda_{FA}}"', from=1-3, to=1-1]
\arrow["{\rho_{FA}}"', from=1-7, to=1-5]
\arrow["{\id\otimes \psi_0}"', from=1-5, to=3-5]
\arrow["{\psi_{A,I}}"', from=3-5, to=3-7]
\arrow["{F(\rho_A)}", from=1-7, to=3-7]
\end{tikzcd}
\end{equation}

$F$ is said to be lax symmetric monoidal if also the following diagram commutes

\[\begin{tikzcd}
{F(A\otimes B)} && {F(B\otimes A)} \\
{F(A)\otimes F(B)} && {F(B)\otimes F(A)}
\arrow["{F(\gamma_{A,B})}", from=1-1, to=1-3]
\arrow["{\psi_{A,B}}"', from=1-1, to=2-1]
\arrow["{\gamma_{FA,FB}}"', from=2-1, to=2-3]
\arrow["{\psi_ {B,A}}", from=1-3, to=2-3]
\end{tikzcd}\]

For example, if $\mC$ is the terminal monoidal category with only one object $I$ and $\id_I$ as the only arrow, then $F$ is simply a monoid in $\mD$.
We do not spell out the following dual version in full detail.

A functor $\freccia{\mC}{F}{\mD}$ is oplax monoidal if it is equipped with a
natural transformation

\[\freccia{F\circ \otimes }{\phi}{ \otimes\circ (F\otimes F)}\]

and a map
satisfying axioms dual to those in Definition <ref>. Similarly, an oplax symmetric monoidal functor is an oplax monoidal functor such that $\phi$ commutes with the braiding $\gamma$.

We also have the notion of strong symmetric monoidal functor, which is a lax symmetric monoidal functor with invertible structure arrows, or equivalently an oplax monoidal functor with invertible structure arrows; and that of strict symmetric monoidal functor, in which the structure arrows are identities.

A monoid and comonoid structure on an object in a symmetric monoidal category often interact in a nice way, either such that they form a bimonoid or a Frobenius monoid (and sometimes both).
The following definition (see [19]) generalises the former notion to functors.

A functor $\freccia{\mC}{F}{\mD}$ is bilax monoidal if it is equipped with a lax monoidal structure $\psi,\psi_0$ and an oplax monoidal structure $\phi,\phi_0$ such that the following compatibility conditions hold

* Braiding. The following diagram commutes

\[\begin{tikzcd}[column sep=-5ex]
& {F(A\otimes B) \otimes F(C\otimes D)} \\
{F(A\otimes B\otimes C\otimes D)} && {F(A)\otimes F(B)\otimes F(C)\otimes F(D)} \\
{F(A\otimes C\otimes B\otimes D)} && {F(A)\otimes F(C)\otimes F(B)\otimes F(D)} \\
& {F(A\otimes C)\otimes F(B\otimes D)}
\arrow["{\psi_{A\otimes B,C\otimes D}}"', from=1-2, to=2-1]
\arrow["{\phi_{A,B}\otimes \phi_{C,D}}", from=1-2, to=2-3]
\arrow["{F(\id\otimes \gamma\otimes \id)}"', from=2-1, to=3-1]
\arrow["{\id\otimes \gamma\otimes \id}", from=2-3, to=3-3]
\arrow["{\phi_{A\otimes C,B\otimes D}}"', from=3-1, to=4-2]
\arrow["{\psi_{A,C}\otimes \psi_{B,D}}", from=3-3, to=4-2]
\end{tikzcd}\]

* Unitality. The following diagrams commute

\[\begin{tikzcd}
I & {F(I)} & {F(I\otimes I)} & I & {F(I)} & {F(I\otimes I)} \\
{I\otimes I} && {F(I)\otimes F(I)} & {I\otimes I} && {F(I) \otimes F(I)} \\
&& {F(I)} \\
& I && I
\arrow["{\psi_0}", from=1-1, to=1-2]
\arrow["{F(\lambda_I)}", from=1-2, to=1-3]
\arrow["{\lambda_I}"', from=1-1, to=2-1]
\arrow["{\phi_{I,I}}", from=1-3, to=2-3]
\arrow["{\psi_{I,I}}"', from=2-6, to=1-6]
\arrow["{F(\lambda_I^{-1})}"', from=1-6, to=1-5]
\arrow["{\phi_0}"', from=1-5, to=1-4]
\arrow["{\phi_0\otimes \phi_0}", from=2-6, to=2-4]
\arrow["{\lambda_I^{-1}}", from=2-4, to=1-4]
\arrow["{\psi_0}", from=4-2, to=3-3]
\arrow["{\phi_0}", from=3-3, to=4-4]
\arrow[Rightarrow, no head, from=4-2, to=4-4]
\arrow["{\psi_0\otimes \psi_0}"', from=2-1, to=2-3]
\end{tikzcd}\]

We also say that $F$ is bilax symmetric monoidal if in addition both the lax and oplax structures are symmetric.

The following notion is due to Szlachányi <cit.>, see also <cit.>.
[Frobenius monoidal functor]
A functor $\freccia{\mC}{F}{\mD}$ is Frobenius monoidal if it is
equipped with a monoidal structure $\psi,\psi_0$ and an oplax monoidal structure $\phi,\phi_0$ such that
the following diagrams commute

\[\begin{tikzcd}
{F(A\otimes B)\otimes F(C)} && {F(A\otimes B\otimes C)} \\
{F(A)\otimes F(B)\otimes F(C)} && {F(A)\otimes F(B\otimes C)} \\
{F(A)\otimes F(B\otimes C)} && {F(A\otimes B\otimes C)} \\
{F(A)\otimes F(B)\otimes F(C)} && {F(A\otimes B)\otimes F(C)}
\arrow["{\phi_{A,B}\otimes {}\id}"', from=1-1, to=2-1]
\arrow["{\psi_{A\otimes B,C}}", from=1-1, to=1-3]
\arrow["{\phi_{A,B\otimes C}}", from=1-3, to=2-3]
\arrow["{\id\otimes \,\psi_{B,C}}"', from=2-1, to=2-3]
\arrow["{\psi_{A,B\otimes C}}", from=3-1, to=3-3]
\arrow["{\phi_{A\otimes B,C}}", from=3-3, to=4-3]
\arrow["{\id\otimes \,\phi_{B,C}}"', from=3-1, to=4-1]
\arrow["{\psi_{A\otimes B,C}\otimes {}\id}"', from=4-1, to=4-3]
\end{tikzcd}\]

There is again the obvious notion of Frobenius symmetric monoidal functor.

In the main text, we also use all of these definitions for lax functors, to which they apply without further modifications.

§ COMMUTATIVE MONADS

Here we start by recalling the definition of Kleisli category of a monad.

The Kleisli category $\mC_{T}$ of a monad $(T,\mu,\eta)$ on a category $\mC$ has as objects those of $\mC$, and for every $X$ and $Y$ in $\mC_{T}$ the hom-set

\[
\mC_{T}(X,Y) := \mC(X,T(Y)).
\]

Writing $\freccia{X}{f^\sharp}{T(Y)}$ for the representative in $\mC$ of an arrow $\freccia{X}{f}{Y}$ in $\mC_T$, composition of $f\in \mC_{T}(X,Y)$ and $g\in \mC_{T}(Y,Z)$ is defined as

\[
(g\circ f)^\sharp := \mu_Z \circ T(g^\sharp) \circ f^\sharp.
\]

In particular, we have $\id_X^\sharp = \eta_X$, since the naturality of $\eta$ and the unitality equations for $T$ imply

\[
\mu_Y \circ T(f^\sharp) \circ \eta_X = \mu_Y \circ T(\eta_Y) \circ f^\sharp = f^\sharp,
\]

and this shows the required equations $f \circ \id_X = \id_Y \circ f = f$.

A strength and a costrength for a monad on a monoidal category are structures relating the monad with the tensor product of the category at least in one direction. A monad equipped with a strength is called a strong monad.
This notion was introduced by Kock in [50, 51] as an alternative description of enriched monads.
Strong monads have been successfully used in computer science, playing a fundamental role in Moggi’s theory of computation [27, 28].

We recall these concepts in the following definitions.

A strong monad $(T,\mu,\eta,t)$ on a symmetric monoidal category $\mC$ is a monad $(T,\mu,\eta)$ on $\mC$ together with a natural transformation

\[
\freccia{X\otimes T(Y)}{t_{X,Y}}{T(X\otimes Y)},
\]

called strength, such that the following diagrams commute for all objects $X$, $Y$, $Z$ of $\mC$

\[\begin{tikzcd}
{X\otimes Y} & {X\otimes T(Y)}  & {I\otimes T(X)} & {T(I\otimes X)} \\
& {T(X\otimes Y)} && {T(X)}\\
%	{I\otimes T(X)} & {T(I\otimes X)} \\
%	& {T(X)} \\
{X\otimes Y\otimes T(Z)} && {T(X\otimes Y\otimes Z)} \\
& {X\otimes T(Y\otimes Z)} \\
{X \otimes T^2(Y)} & {T(X\otimes T(Y))} & {T^2(X\otimes Y)} \\
{X\otimes T(Y)} && {T(X\otimes Y)}
\arrow["{\lambda^{-1}_{T(X)}}"', from=1-3, to=2-4]
\arrow["{t_{I,X}}", from=1-3, to=1-4]
\arrow["{T(\lambda^{-1}_X)}", from=1-4, to=2-4]
\arrow["{t_{X,T(Y)}}", from=5-1, to=5-2]
\arrow["{T(t_{X,Y})}", from=5-2, to=5-3]
\arrow["{\id_X\otimes \mu_Y}"', from=5-1, to=6-1]
\arrow["{t_{X,Y}}"', from=6-1, to=6-3]
\arrow["{\mu_{X\otimes Y}}", from=5-3, to=6-3]
\arrow["{\id_X\otimes \eta_Y}", from=1-1, to=1-2]
\arrow["{\eta_{X\otimes Y}}"', from=1-1, to=2-2]
\arrow["{t_{X,Y}}", from=1-2, to=2-2]
\arrow["{t_{X,Y\otimes Z}}"', from=4-2, to=3-3]
\arrow["{\id_X\otimes t_{Y,Z}}"', from=3-1, to=4-2]
\arrow["{t_{X\otimes Y,Z}}", from=3-1, to=3-3]
\end{tikzcd}\]

The list monad $\freccia{\Set}{T_{\mathrm{list}}}{\Set}$ is strong. Given two sets $X$ and $Y$, the strength component

\[
\freccia{X \times T_{\mathrm{list}}(Y)}{t_{X,Y}}{T_{\mathrm{list}}(X \times Y)}
\]

is given by the function assigning to an element $(x,[y_1,\dots,y_m])) $ of $ X\times T_{\mathrm{list}}(Y)$ the element $[(x,y_1),\dots,(x,y_m)]$ of $ T_{\mathrm{list}}(X\times Y)$.

In fact, any monad on the cartesian category $\Set$ is strong in a unique way, where the strength can be defined similarly to the strength of the list monad. We refer to  [50, 51] for more details.

The braiding $\gamma$ of $\mC$ let us define a costrength with components

\[\freccia{T(X)\otimes Y}{t_{X,Y}'}{T(X\otimes Y)}\]

given by

\[t_{X,Y}':=T(\gamma_{Y,X}) \circ t_{Y,X} \circ \gamma_{T(X),Y}.\]

It satisfies axioms that are analogous to those of strength.

A strong monad $(T,\mu,\eta,t)$ on a symmetric monoidal category $\mC$ is said to be commutative if the following
diagram commutes for every object $X$ and $Y$

\begin{equation}
\begin{split}
\label{commutative_monad_diag}
\xymatrix@+1pc{
T(X)\otimes T(Y) \ar[r]^{t_{T(X),Y}} \ar[d]_{t'_{X,T(Y)}} & T(T(X)\otimes Y) \ar[r]^{T(t'_{X,Y})} & T^2(X\otimes Y) \ar[d]^{\mu_{X\otimes Y}}\\
T(X\otimes T(Y))\ar[r]_{T(t_{X,Y})} & T^2(X\otimes Y) \ar[r]_{\mu_{X\otimes Y}} & T(X\otimes Y)
\end{split}
\end{equation}

\begin{equation}
\label{commutative_monad_diag}
% https://q.uiver.app/?q=WzAsNixbMCwwLCJUKFgpXFxvdGltZXMgVChZKSJdLFsxLDAsIlQoVChYKVxcb3RpbWVzIFkpIl0sWzIsMCwiVF4yKFhcXG90aW1lcyBZKSJdLFswLDEsIlQoWFxcb3RpbWVzIFQoWSkpIl0sWzIsMSwiVChYXFxvdGltZXMgWSkiXSxbMSwxLCJUXjIoWFxcb3RpbWVzIFkpIl0sWzAsMSwidF97VChYKSxZfSJdLFsxLDIsIlQodCdfe1gsWX0pIl0sWzAsMywidCdfe1gsVChZKX0iLDJdLFszLDUsIlQodF97WCxZfSkiLDJdLFs1LDQsIlxcbXVfe1hcXG90aW1lcyBZfSIsMl0sWzIsNCwiXFxtdV97WFxcb3RpbWVzIFl9Il1d
\begin{tikzcd}
{T(X)\otimes T(Y)} & {T(T(X)\otimes Y)} & {T^2(X\otimes Y)} \\
{T(X\otimes T(Y))} & {T^2(X\otimes Y)} & {T(X\otimes Y)}
\arrow["{t_{T(X),Y}}", from=1-1, to=1-2]
\arrow["{T(t'_{X,Y})}", from=1-2, to=1-3]
\arrow["{t'_{X,T(Y)}}"', from=1-1, to=2-1]
\arrow["{T(t_{X,Y})}"', from=2-1, to=2-2]
\arrow["{\mu_{X\otimes Y}}"', from=2-2, to=2-3]
\arrow["{\mu_{X\otimes Y}}", from=1-3, to=2-3]
\end{tikzcd}
\end{equation}

It is well-known that on a symmetric monoidal category, commutative monads are equivalent to symmetric monoidal monads <cit.>.
Indeed, the diagonal of (<ref>) equips the functor $T$ with a lax symmetric monoidal structure, whose components we denote by $c_{X,Y} : T(X) \otimes T(Y) \to T(X \otimes Y)$.

§ A STRING DIAGRAM PRESENTATION OF RESTRICTION CATEGORIES

Let $\mC$ be a gs-monoidal category. Then the category $\pfn{\mC}$ of $\mC$-functional arrows is a restriction category
with respect to the structure given by $\dom (-)$.

By [17], we have to verify the following equations, that we also present graphically by making explicit the definition of $\dom (-)$:

* $f\circ \dom (f)=f$ for any arrow $\freccia{A}{f}{B}$

[scale=0.60, transform shape]
[style=none] (31) at (4.75, 1.5) ;
[style=none] (32) at (6.25, 2) ;
[style=none] (33) at (6.25, 1) ;
[style=none] (34) at (7, 1) ;
[style=nodonero] (35) at (5.75, 1.5) ;
[style=none] (36) at (5.25, 1.75) A;
[style=box] (37) at (7, 1) $f$;
[style=nodonero] (38) at (8.25, 1) ;
[style=none] (39) at (8.25, 2) ;
[style=none] (40) at (8.25, 2.25) B;
[style=none] (41) at (7.75, 0.75) B;
[style=none] (42) at (9.75, 1.5) ;
[style=none] (43) at (10.25, 1.75) A;
[style=none] (44) at (9, 1.5) $=$;
[style=box] (45) at (7, 2) $f$;
[style=box] (46) at (10.75, 1.5) $f$;
[style=none] (47) at (11.75, 1.5) ;
[style=none] (48) at (11.25, 1.75) B;

(31.center) to (35);
[bend left, looseness=1.25] (35) to (32.center);
[bend right] (35) to (33.center);
(33.center) to (34.center);
(34.center) to (37.center);
(37) to (38);
(32.center) to (45);
(45) to (39.center);
(42.center) to (46);
(46) to (47.center);

In fact, $(B \otimes {!B})\circ(f \otimes f)\circ \nabla_A =\mbox{ [$f$ functional] } (B \otimes {!B})\circ \nabla_B \circ f = id_B \circ f = f$.

* $\dom (f) \circ \dom (g)=\dom (g) \circ \dom (f) $ if the source of $g$ is the same of $f$

[scale=0.60, transform shape]
[style=none] (31) at (4.75, 1.5) ;
[style=none] (32) at (6.25, 2) ;
[style=none] (33) at (6.25, 1) ;
[style=none] (34) at (7, 1) ;
[style=nodonero] (35) at (5.75, 1.5) ;
[style=none] (36) at (5.25, 1.75) A;
[style=box] (37) at (7, 1) $g$;
[style=nodonero] (38) at (8.25, 1) ;
[style=none] (39) at (8.25, 2) ;
[style=none] (40) at (7.25, 2.25) A;
[style=none] (41) at (7.75, 0.75) C;
[style=none] (44) at (12, 1.5) $=$;
[style=none] (50) at (8.75, 2.5) ;
[style=none] (51) at (8.75, 1.5) ;
[style=none] (52) at (9.5, 1.5) ;
[style=nodonero] (53) at (8.25, 2) ;
[style=box] (55) at (9.5, 1.5) $f$;
[style=nodonero] (56) at (10.75, 1.5) ;
[style=none] (57) at (10.75, 2.5) ;
[style=none] (58) at (10.75, 2.75) A;
[style=none] (59) at (10.25, 1.25) B;
[style=none] (60) at (13, 1.5) ;
[style=none] (61) at (14.5, 2) ;
[style=none] (62) at (14.5, 1) ;
[style=none] (63) at (15.25, 1) ;
[style=nodonero] (64) at (14, 1.5) ;
[style=none] (65) at (13.5, 1.75) A;
[style=box] (66) at (15.25, 1) $f$;
[style=nodonero] (67) at (16.5, 1) ;
[style=none] (68) at (16.5, 2) ;
[style=none] (69) at (15.5, 2.25) A;
[style=none] (70) at (16, 0.75) B;
[style=none] (71) at (17, 2.5) ;
[style=none] (72) at (17, 1.5) ;
[style=none] (73) at (17.75, 1.5) ;
[style=nodonero] (74) at (16.5, 2) ;
[style=box] (75) at (17.75, 1.5) $g$;
[style=nodonero] (76) at (19, 1.5) ;
[style=none] (77) at (19, 2.5) ;
[style=none] (78) at (19, 2.75) A;
[style=none] (79) at (18.5, 1.25) C;

(31.center) to (35);
[bend left, looseness=1.25] (35) to (32.center);
[bend right] (35) to (33.center);
(33.center) to (34.center);
(34.center) to (37.center);
(37) to (38);
(32.center) to (39.center);
[bend left, looseness=1.25] (53) to (50.center);
[bend right] (53) to (51.center);
(51.center) to (52.center);
(52.center) to (55.center);
(55) to (56);
(50.center) to (57.center);
(60.center) to (64);
[bend left, looseness=1.25] (64) to (61.center);
[bend right] (64) to (62.center);
(62.center) to (63.center);
(63.center) to (66);
(66) to (67);
(61.center) to (68.center);
[bend left, looseness=1.25] (74) to (71.center);
[bend right] (74) to (72.center);
(72.center) to (73.center);
(73.center) to (75);
(75) to (76);
(71.center) to (77.center);

Proof missing: see comment below

* $\dom (g\circ \dom (f))=\dom (g) \circ \dom (f) $ if the source of $g$ is the same of $f$

[scale=0.60, transform shape]
[style=none] (44) at (10, -2.5) $=$;
[style=none] (60) at (11, -2.5) ;
[style=none] (61) at (12.5, -2) ;
[style=none] (62) at (12.5, -3) ;
[style=none] (63) at (13.25, -3) ;
[style=nodonero] (64) at (12, -2.5) ;
[style=none] (65) at (11.5, -2.25) A;
[style=box] (66) at (13.25, -3) $f$;
[style=nodonero] (67) at (14.5, -3) ;
[style=none] (68) at (14.5, -2) ;
[style=none] (69) at (13.5, -1.75) A;
[style=none] (70) at (14, -3.25) B;
[style=none] (71) at (15, -1.5) ;
[style=none] (72) at (15, -2.5) ;
[style=none] (73) at (15.75, -2.5) ;
[style=nodonero] (74) at (14.5, -2) ;
[style=box] (75) at (15.75, -2.5) $g$;
[style=nodonero] (76) at (17, -2.5) ;
[style=none] (77) at (17, -1.5) ;
[style=none] (78) at (17, -1.25) A;
[style=none] (79) at (16.5, -2.75) C;
[style=none] (80) at (4, -2) ;
[style=none] (81) at (5.5, -1.5) ;
[style=none] (82) at (5.5, -2.5) ;
[style=none] (83) at (6.25, -2.5) ;
[style=nodonero] (84) at (5, -2) ;
[style=none] (85) at (4.5, -1.75) A;
[style=none] (88) at (8.75, -1.5) ;
[style=none] (92) at (6.25, -2.5) ;
[style=none] (93) at (6.75, -2) ;
[style=none] (94) at (6.75, -3) ;
[style=none] (95) at (7.5, -3) ;
[style=nodonero] (96) at (6.25, -2.5) ;
[style=box] (97) at (7.5, -3) $f$;
[style=nodonero] (98) at (8.75, -3) ;
[style=none] (101) at (8.25, -3.25) B;
[style=none] (103) at (8.25, -1.25) A;
[style=box] (104) at (7.5, -2) $g$;
[style=nodonero] (105) at (8.75, -2) ;
[style=none] (106) at (8.25, -2.25) C;

(60.center) to (64);
[bend left, looseness=1.25] (64) to (61.center);
[bend right] (64) to (62.center);
(62.center) to (63.center);
(63.center) to (66);
(66) to (67);
(61.center) to (68.center);
[bend left, looseness=1.25] (74) to (71.center);
[bend right] (74) to (72.center);
(72.center) to (73.center);
(73.center) to (75);
(75) to (76);
(71.center) to (77.center);
(80.center) to (84);
[bend left, looseness=1.25] (84) to (81.center);
[bend right] (84) to (82.center);
(82.center) to (83.center);
(81.center) to (88.center);
[bend left, looseness=1.25] (96) to (93.center);
[bend right] (96) to (94.center);
(94.center) to (95.center);
(95.center) to (97.center);
(97) to (98);
(93.center) to (104);
(104) to (105);

Proof missing: see comment below

* $\dom (g) \circ f=f \circ \dom (g \circ f)$ if the source of $g$ is equal to the target of $f$

[scale=0.60, transform shape]
[style=none] (32) at (6.25, 2) ;
[style=none] (33) at (6.25, 1) ;
[style=none] (34) at (7, 1) ;
[style=nodonero] (35) at (5.75, 1.5) ;
[style=none] (36) at (4, 1.75) A;
[style=box] (37) at (7, 1) $g$;
[style=nodonero] (38) at (8.25, 1) ;
[style=none] (39) at (8.25, 2) ;
[style=none] (40) at (5.25, 1.75) B;
[style=none] (41) at (7.75, 0.75) C;
[style=none] (44) at (9, 1.5) $=$;
[style=none] (49) at (9.75, 1.5) ;
[style=none] (50) at (11.25, 2) ;
[style=none] (51) at (11.25, 1) ;
[style=none] (52) at (12, 1) ;
[style=nodonero] (53) at (10.75, 1.5) ;
[style=none] (54) at (10.25, 1.75) A;
[style=box] (55) at (12, 1) $f$;
[style=nodonero] (56) at (14.75, 1) ;
[style=none] (57) at (14.75, 2) ;
[style=none] (58) at (13.25, 2.25) B;
[style=none] (59) at (12.75, 0.75) B;
[style=box] (60) at (12, 2) $f$;
[style=box] (61) at (13.5, 1) $g$;
[style=none] (62) at (14.25, 0.75) C;
[style=box] (63) at (4.5, 1.5) $f$;
[style=none] (64) at (3.25, 1.5) ;
[style=none] (65) at (7.75, 2.25) B;

[bend left, looseness=1.25] (35) to (32.center);
[bend right] (35) to (33.center);
(33.center) to (34.center);
(34.center) to (37.center);
(37) to (38);
(49.center) to (53);
[bend left, looseness=1.25] (53) to (50.center);
[bend right] (53) to (51.center);
(51.center) to (52.center);
(52.center) to (55);
(55) to (56);
(50.center) to (60);
(60) to (57.center);
(64.center) to (63);
(63) to (35);
(32.center) to (39.center);

Proof missing: see comment below

Clearly, axioms $2$ and $3$ are satisfied by any gs-monoidal category.
This is very confusing: why do we list axioms 2 and 3 as conditions if they're automatically satisfied? (I had turned this into a proposition from a definition; maybe this was actually supposed to be the defn of restriction category, as the section title indicates? But it's clearly not since a general restriction category doesn't even have a monoidal structure, so also the section title seems problematic to me)
I tried to turn the above into a meaningful statement. The missing proofs can be added if we decide to keep the Proposition, which is not original according to the Tobias comments that I've found along the paper.