Premonoidal categories and Freyd categories provide an encompassing
framework for the semantics of call-by-value programming languages.
Premonoidal categories
are a weakening of monoidal categories in which the interchange law
for the tensor
may not hold,
modelling the fact that
effectful programs cannot generally be re-ordered. A Freyd category
is a pair of categories
with the same objects:
a premonoidal category of general programs, and a monoidal category of `effect-free' programs which do admit re-ordering.

Certain recent innovations in semantics, however, have produced
models which are not categories but bicategories.
Here we develop the theory to capture such examples by introducing premonoidal and Freyd structure in a bicategorical setting.
The second dimension introduces new subtleties, so we
verify our definitions with several examples and a correspondence theorem—between Freyd bicategories and certain actions of monoidal bicategories—which parallels the categorical framework.

§ INTRODUCTION

A fundamental aspect of call-by-value functional programming languages is the distinction between values and computations. While
values are `pure' program fragments that can be passed around safely,
computations may interact with their environment in the form of effects (such
as raising exceptions, interacting with state, or behaving probabilistically), and must therefore be manipulated with care.

Values and computations obey different algebraic properties, and in
particular only
computations are sensitive to the evaluation order.
For instance
print "a"; print "b"
is not equivalent to
print "b"; print "a". This is reflected in the
denotational semantics of call-by-value languages, which
consists of  a pair of categories: a monoidal category of
values, and a premonoidal category of
computations. These are related by an identity-on-objects functor
coercing values into effect-free computations, and the
resulting structure is called a Freyd category
([38, 26]).

In this paper we generalize these notions from categories to
bicategories.  The resulting theory includes models of
programming languages
in which the morphisms are themselves objects
with structure—spans, strategies, parameter spaces,
profunctors, open systems, etc.—for which the notion of
composition uses a universal construction, such as a pullback or a pushout.
In these models, the 2-cells play a central role in characterizing the composition
operation for morphisms, and additionally provide refined semantic information
(see  [17, 8, 48, 34, 22]).

§.§ Bicategorical models

A bicategory is a 2-dimensional category in which the associativity and  unit laws
for the composition of morphisms are
replaced by invertible 2-cells satisfying coherence axioms [2].
Bicategories have recently found prominence as models of computational processes: see  [31, 6, 12, 1].
We illustrate this with two simple examples: spans of sets, and graded
monads. For reasons of space we have omitted definitions of the basic notions in bicategory theory, such as pseudofunctors, pseudonatural
transformations, and modifications. For a textbook account, see  [2].

Bicategories of spans.

The bicategory $\Span(\Set)$ has objects sets and 1-cells
$A \rightsquigarrow B$
spans of functions
$A \longleftarrow S \longrightarrow B$.
We can compose pairs of morphisms
$A \longleftarrow S \longrightarrow B$
$B \longleftarrow R \longrightarrow C$
using a pullback in the category of sets, as on the left below:

\begin{equation*}
\begin{tikzcd}[column sep=.3em, row sep=0.3em]
&[1em] & {R \circ S} \\
& S && R \\
A && B &&[1em] C
\arrow[from=2-2, to=3-1]
\arrow[from=2-2, to=3-3]
\arrow[from=2-4, to=3-3]
\arrow[from=2-4, to=3-5]
\arrow[from=1-3, to=2-2]
\arrow[from=1-3, to=2-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-3, to=3-3]
\end{tikzcd}\qquad
\begin{tikzcd}[column sep=0.7em, row sep=0.7em, scalenodes=0.6]
&&& \bullet \\
&& \bullet \\
& \bullet && \bullet && \bullet \\
\bullet && \bullet && \bullet && \bullet
\arrow[from=3-2, to=4-3]
\arrow[from=3-4, to=4-3]
\arrow[from=3-4, to=4-5]
\arrow[from=2-3, to=3-2]
\arrow[from=2-3, to=3-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=2-3, to=4-3]
\arrow[from=3-6, to=4-5]
\arrow[from=1-4, to=2-3]
\arrow[from=1-4, to=3-6]
\arrow[from=3-6, to=4-7]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-4, to=3-4]
\arrow[from=3-2, to=4-1]
\end{tikzcd}
\hspace{5mm}
\begin{tikzcd}[column sep=0.7em, row sep=0.7em, scalenodes=0.6]
&&& \bullet \\
&&&& \bullet \\
& \bullet && \bullet && \bullet \\
\bullet && \bullet && \bullet && \bullet
\arrow[from=3-2, to=4-3]
\arrow[from=3-4, to=4-3]
\arrow[from=3-4, to=4-5]
\arrow[from=3-6, to=4-5]
\arrow[from=3-6, to=4-7]
\arrow[from=3-2, to=4-1]
\arrow[from=1-4, to=3-2]
\arrow[from=2-5, to=3-4]
\arrow[from=2-5, to=3-6]
\arrow[from=1-4, to=2-5]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=1-4, to=3-4]
\arrow["\lrcorner"{anchor=center, pos=0.125, rotate=-45}, draw=none, from=2-5, to=4-5]
\end{tikzcd}
\end{equation*}

This composition correctly captures a notion of `plugging together' spans, but is only
associative in a weak sense, since the two ways of taking pullbacks
(on the right above) are not generally equal. But, by the universal property of
pullbacks, they are canonically isomorphic as spans.

Kleisli bicategories for graded monads.

For another example we consider monads graded by monoidal
categories. Formally, a graded monad on a category $\catC$ consists of a monoidal category $(\catE, \bullet, \tensu)$
of grades and a lax monoidal functor
$T : \catE \to [\catC, \catC]$
(see  [43, 30, 21]).
In particular, this gives a functor $T_e : \catC \to \catC$ for every
$e \in \catE$, and natural transformations
$\mu_{e, e'}  : T_{e'} \circ T_e \To T_{e \bullet e'}$ and
$\eta : \id \To T_{\tensu}$
corresponding to a multiplication and unit.

Previous Kleisli-like constructions for graded monads have used presheaf-enriched categories
( [10, 28]),
but there is also a natural bicategorical construction.
The objects are those of $\catC$ and 1-cells $A \rightsquigarrow B$ consist of a grade $e$ and a map
$f : A \to T_eB$ in $\catC$.
The 2-cells $(e, f) \To (e', f')$  are re-gradings: maps $\gamma : e \to e'$ in $\catE$ such that
$T_\gamma(B) \circ f = f'$.
The composition and identities use the multiplication and unit, as
for a Kleisli category. But, unless $\catE$ is strict monoidal, this
operation is only weakly associative and unital.

A concrete instance of this is the $\mathbf{coPara}$
construction on a monoidal
category $\catC$ ([9, 5]), equivalently defined as the Kleisli bicategory for the
monad graded by $\catC$ itself and given by $T_C(A) = A \otimes C$.

The broader context for this
work is the recent occurrence of bicategories in the semantics of
programming languages. Bicategories of profunctors are
now prominent in the analysis of linear logic and the
$\lambda$-calculus ([7, 11, 22]), and game semantics employs a variety of span-like
constructions that compose weakly ([31, 3]). These
models have also influenced the development of 2-dimensional type theories
([8, 34]).   This paper supports these
developments from the perspective of call-by-value languages. (The
connection to linear logic explains our insistence on monoidal rather
than cartesian Freyd bicategories.)

§.§ Monoidal bicategories

A monoidal bicategory is a bicategory equipped with a unit object and
a tensor product which is only weakly associative and unital. In the
categorical setting `weakly' typically means `up to isomorphism'; in
bicategory theory it typically means `up to equivalence'.

An equivalence between objects $A$ and $B$ in a
bicategory $\B$ is a pair of 1-cells $f : A \to B$ and
$\psinv{f} : B \to A$ together with invertible 1-cells
$\un : \Id_A \To \psinv{f} \circ f$
$\co : f \circ \psinv{f} \To \Id_B$.
This is an adjoint equivalence if the witnessing 2-cells $\un$ and $\co$ satisfy the usual triangle laws for an adjunction (see  [24]).

It is common in bicategory theory for definitions to ask for adjoint equivalences: these are easier to work with and no stronger than asking for just equivalences
(see  <cit.>).

The bicategorical version of a natural isomorphism is a
pseudonatural (adjoint) equivalence: a pseudonatural transformation in which each 1-cell component has the structure of an (adjoint) equivalence.

A monoidal bicategory is a bicategory $\B$ equipped with a
pseudofunctor $\otimes : \B \times \B \to \B$ and an object $I \in \B$,
together with:

* pseudonatural adjoint equivalences $\alpha, \lambda$ and $\rho$ with
$\alpha_{A, B, C} : (A \otimes B) \otimes C \to
{A \otimes (B \otimes C)}$
(the associator),
$\lambda_A : I \otimes A \to A$,
$\rho_A : A \otimes I \to A$
(the unitors); and

* invertible modifications
$\mathfrak{p}, \mathfrak{l}, \mathfrak{m}$ and $\mathfrak{r}$
with components as in <Ref>,
subject to coherence axioms.

The structural modifications of a monoidal bicategory

Monoidal bicategories have a technical algebraic definition but nonetheless
arise naturally.
For example, the cartesian product on the category
$\Set$ induces a monoidal structure on the bicategory $\Span(\Set)$.
Many other examples appear in a similar fashion: see [49].

Coherence theorems.

A careful reader might observe that the diagrams in <Ref> are not, strictly speaking, well-typed: for example, the anti-clockwise route around the diagram for $\pentagonator$ could denote
$(A\alpha \circ \alpha) \circ \alpha D$
$ A\alpha \circ (\alpha \circ \alpha D)$.
This is justified by a suitable coherence theorem.

Typically, coherence theorems show that any two parallel 2-cells built out of the structural data are equal.
Appropriate coherence theorems apply to bicategories [27],
pseudofunctors [14],
(symmetric) monoidal bicategories
([13, 14, 15]).
These results justify writing simply $\iso$ for composites of structural data in commutative diagrams of 2-cells, in much the same way as one does for monoidal categories.

As is common in the field, we rely heavily on the coherence of bicategories and pseudofunctors
when writing pasting diagrams of 2-cells. We omit all compositors and unitors for pseudofunctors, and
ignore the weakness of 1-cell composition.
Thus, even though our diagrams do not strictly type-check, coherence guarantees the resulting 2-cell is the same no matter how one fills in the structural details.
For example, for a pseudofunctor $T$ on a monoidal bicategory we may write $T\mathfrak{l}$ as a 2-cell of type
$T(\lambda B) \To T\lambda \circ T\alpha$.
For a detailed justification see
<cit.> or <cit.>.

§.§ Premonoidal categories and Freyd categories

Premonoidal categories generalize monoidal categories in that
the tensor product $\tens$ is only functorial in each argument separately [37].
The lack of a monoidal “interchange law” reflects the fact that one cannot generally re-order the statements of an effectful program, even
if the data flow permits it.
As a consequence, one can directly model effectful programs in a premonoidal category,
in the sense that a typed program
$(\Gamma \vdash M : A)$
is modelled directly as an arrow
$\Gamma \to A$ and
the result of substituting $M$ into another effectful program
$(\Delta, x: A \vdash N : B)$
is modelled by the composite
\Delta \otimes \Gamma
\xra{\Delta \otimes M}
\Delta \otimes A
\xra{N}
Thus, the composition of morphisms in a
premonoidal category should be understood as encoding control
flow. This is illustrated in Figure <ref> using the
graphical calculus for premonoidal categories
([20, 39]),
where the dashed red line indicates control flow.
This direct interpretation contrasts with monadic approaches ([32, 33]),
which rely on a monad whose structure may not be reflected in the syntax.

We can axiomatize the morphisms for which
interchange does hold. Let $\catD$ be a category equipped with functors
$A \ltie (-) : \catD \longrightarrow \catD$
$(-) \rtie B : \catD \longrightarrow \catD$
for every $A, B \in \catD$,
such that
$A \ltie B = A \rtie B$.
We write $A \tens B$, or
just $AB$, for their joint value, and $\binoidal\catD$ is called a
binoidal category.
A map  $f : A \to A'$ in $\catD$ is central if the two diagrams

\begin{equation}
\label{eq:centrality-cat}
\begin{tikzcd}[column sep = 3 em]
A B
\arrow{r}{A \ltie g}
\arrow[swap]{d}{f \rtie B}
A B'
\arrow{d}{f \rtie B'}
\\
A'  B
\arrow[swap]{r}{A' \ltie g}
A' B'
\end{tikzcd}
\hspace{16mm}
\begin{tikzcd}[column sep = 3 em]
B   A
\arrow{r}{g \rtie A}
\arrow[swap]{d}{B \ltie f}
B' A
\arrow{d}{B' \ltie f}
\\
B  A'
\arrow[swap]{r}{g \rtie A'}
B'  A'
\end{tikzcd}
\end{equation}

commute for every $g :B \to B'$.
Semantically, $f$ corresponds to a computation which may be run at any
point without changing the observable result.

A premonoidal category is a binoidal category $\binoidal\catD$ with central structural isomorphisms $\alpha, \lambda$ and $\rho$ similar to those in a monoidal category.
Unlike with monoidal categories, however, the associator $\alpha$ cannot be a natural transformation in all arguments simultaneously, because $\tens$ is not a functor on
$\catD$. Instead, we must ask for naturality in each argument separately, so the following three diagrams commute:

\begin{equation}
\label{eq:naturality-for-alpha}
\begin{tikzcd}[column sep=4em, row sep = 1.5em]
\arrow{r}{(f \rtie B) \rtie C}
\arrow[swap]{d}[xshift=0mm]{\alpha}  &
\arrow{d}[xshift=0mm]{\alpha} \\
\arrow{r}[swap]{f \rtie (B C)} &
\end{tikzcd}
\hspace{4mm}
\begin{tikzcd}[column sep=4em, row sep = 1.5em]
(AB)C \arrow{d}[swap]{\alpha} \arrow{r}{(A \ltie g) \rtie C} &
(AB')C \arrow{d}{\alpha}\ \\
A(BC) \arrow{r}[swap]{A \ltie (g \rtie C)}  & A(B'C)
\end{tikzcd}
\hspace{4mm}
\begin{tikzcd}[column sep=4em, row sep = 1.5em]
(AB)C \arrow{d}[swap]{\alpha}  \arrow{r}{(A B) \ltie h}&
(AB)C'  \arrow{d}{\alpha}  \\
A(BC') \arrow[]{r}[swap]{A \ltie (B \ltie h)} & A(BC')
\end{tikzcd}
\end{equation}

A premonoidal category is a binoidal category
equipped with a unit object $I$ and central isomorphisms
$\rho_A : A I \to A$,
$\lambda_A : IA \to A$
$\alpha_{A, B, C} : (AB)C \to A  (B  C)$
for every $A, B, C \in \catD$,
natural in each argument separately
and satisfying the axioms for a monoidal category.

One important contribution of this paper is to bicategorify the
notion of central morphism. We will
see that as we move  from categories to bicategories centrality evolves from property to structure

Freyd categories.
When modelling call-by-value languages in premonoidal categories, it
is natural to think of the values as effect-free
computations. Semantically, this is captured by Freyd
categories [38], which are  premonoidal categories
together with a choice of effect-free maps.

Precisely, a Freyd category consists of a monoidal
category $\catV$ (often cartesian monoidal), a premonoidal
category $\catC$, and an identity-on-objects functor $\J : \catV \to
\catC$ that strictly preserves the tensor product and structural
morphisms, and such that every morphism $\J(f)$ is central in

Although every premonoidal category $\catD$ canonically induces a Freyd
category $\centreOf{\catD} \hookrightarrow \catD$, where $\centreOf{\catD}$ is the
subcategory of central maps (called the centre), there are several reasons to consider Freyd
categories directly. First, it does not always make sense to regard all
central maps as values: for instance, in a language with
commutative effects ( probability), all computations are central. Second, functors between binoidal categories do not in general preserve central maps, whereas morphisms of Freyd categories include a functor between the categories of values specifying how values are sent to values.

Relationship to monad models.
Freyd categories encompass the
strong monad semantics of call-by-value proposed by
Moggi ([32, 33]).
Indeed, if
$(\catC, \otimes,I)$
is symmetric monoidal, then any strength for a monad $(T, \mu, \eta)$ on $\catC$ induces a
premonoidal structure on the Kleisli category $\catC_T$, and $\eta
\circ (-) : \catC \to \catC_T$ becomes a Freyd category. Conversely,
a Freyd category corresponds to a monad whenever $\J$ has a right
adjoint [37].
This adjoint is necessary if the programming language has
higher-order functions, but some `first-order'
Freyd categories are not known to arise from a monad
( [47, 36, 44]).

§.§ Contributions and outline

The central aim of this paper is to introduce definitions of
premonoidal bicategories (<Ref>)
Freyd bicategories (<Ref>).
Premonoidal structure relies on an adequate
notion of centrality for 1-cells and 2-cells in a bicategory (<Ref>). Freyd bicategories
then require a coherent assignment of centrality data, which leads to
subtle compatibility issues, outlined in
<Ref> and <Ref>.

As ever with bicategorical definitions
(see  <cit.>),
the main difficulty is in ensuring the right axioms on the 2-cells.
We therefore give further justification for our definitions.
On the one hand, we show that our definitions are not too strict: they capture natural examples,
presented in <Ref> and <Ref>.
On the other hand, we show that our definitions are not too weak: the well-known correspondence between Freyd categories and actions [25] lifts to our setting
We note that our definition of action is extracted from standard
higher-categorical constructions, and so our work connects to an already-existing and well-understood body of theory.

The definition of premonoidal bicategory presented here is based on that in the ArXiv preprint [35].
For reasons of space, we sketch only the proof of the main theorem
For more proofs, see the longer version of this paper, available on the authors' webpages.

§ PREMONOIDAL BICATEGORIES

Just as in the categorical setting ( [37]), our starting point is binoidal structure.

A binoidal bicategory $\binoidal{\baseCat}$ is a bicategory $\baseCat$ with pseudofunctors
$A \ltie (-)$
$(-) \rtie B$
for every $A, B \in \baseCat$, such that $A \ltie B = A \rtie B$.
We write $A \tens B$,  or just $AB$, for the joint value on objects.

As is standard when moving from categories to bicategories, the category-theoretic property of centrality becomes extra structure in a binoidal bicategory. For the definition, we observe that the diagrams defining centrality (<ref>) amount to requiring that $f$ induces two natural transformations:

\begin{equation}
\label{eq:transformation-for-centrality}
\begin{aligned}
\lc{f} : A \ltie (-) \To A' \ltie (-) &
\qquad
\qquad
\lc{f}_B :=  \big( A \ltie B = A \rtie B \xra{f \rtie B} A' \rtie B = A' \ltie B \big)  \\
\rc{f} : (-) \rtie A \To (-) \rtie A' &
\qquad
\qquad
\rc{f}_B := \big( B \rtie A = B \ltie A \xra{B \ltie f} B \ltie A' = B \rtie A' \big)
\end{aligned}
\end{equation}

This lifts naturally to the bicategorical setting, and gives an immediate notion of centrality for 2-cells.

Let $\binoidal{\B}$ be a binoidal bicategory.
central 1-cell
is a 1-cell $f : A \to A'$ equipped with invertible 2-cells as on the right
for every $g: B \to B'$, such that the 1-cells in (<ref>) are the components of pseudonatural transformations
$\lc{f} : A \ltie (-) \To A' \ltie (-)$
$\rc{f} : (-) \rtie A \To (-) \rtie A'$.
A central 2-cell $\sigma$ between central 1-cells
$(f, \lc{f}, \rc{f})$
$(f', \lc{f'}, \rc{f'})$
is a 2-cell $\sigma : f \To f'$
such that the 2-cells $\sigma \rtie B$ and $B \ltie \sigma$
(for $B \in \baseCat$) define modifications
$\lc{f} \To \lc{f'}$
$\rc{f} \To \rc{f'}$,

row sep = 1em,
column sep = 3em
A B
rA g
[swap]df B

A  B'
df B'
[draw=none, yshift=-8mm, swap, shorten=.5em]lf_g

A'  B
[swap]rA' g

A' B'

row sep = 1em,
column sep = 3em
B   A
rg A
[swap]dB f

B'  A
dB' f
[draw=none, yshift=-8mm, swap, shorten=.5em]lf_g

B  A'
[swap]rg A'

B' A'

Every monoidal bicategory $\monoidal{\baseCat}$ has a canonical
binoidal structure, with  $\ltie$ and $\rtie$ directly
induced from the monoidal structure by fixing one argument.
Every 1-cell $f$ in $\B$ is canonically central,
with $\lc{f}_g$ given by the interchange isomorphism induced by the pseudofunctor structure of $\tens$, and  $\rc{f}_g$ by $(\lc{g}_f)^{-1}$:

\begin{equation}
\label{eq:centrality-from-interchange}
\lc{f}_g :=
\big(
(f \tens B') \circ (A \tens g)
\XRA{\iso}
(f \tens g)
\XRA{\iso}
(A' \tens g) \circ (f \tens B)
\big).
\end{equation}

By the functoriality of $\otimes$, every 2-cell is
central with respect to this structure.

We will define premonoidal bicategories as binoidal bicategories with
central structural equivalences. As in <Ref>, the
associator $\alpha$ for the tensor product can only be
pseudonatural in each argument separately, because $\tens$ is
not a functor of two arguments.
We therefore need a family of equivalences
$\alpha_{A, B, C} : (A \tens B) \tens C \to A \tens (B \tens C)$
together with invertible 2-cells
$\cellOf{\alpha}_{f, B, C},
\cellOf{\alpha}_{A, g, C}$
$\cellOf{\alpha}_{A, B, h}$
filling the three squares in
so that we get three families of pseudonatural transformations:

\begin{align}
\label{eq:2-cells-for- alpha}
(\alpha_{-, B, C}, \cellOf{\alpha}_{-, B, C})& : (- \rtie B) \rtie C \To (-) \rtie (B \tens C) \nonumber \\
(\alpha_{A, -, C}, \cellOf{\alpha}_{A, -, C}) &: (A \ltie -) \rtie C \To A \ltie (- \rtie C) \\
(\alpha_{A, B, -}, \cellOf{\alpha}_{A, B, -}) &: (A \tens B) \ltie (-) \To A \ltie (B \ltie -) \nonumber
\end{align}

A premonoidal bicategory also involves structural modifications
corresponding to those of <Ref>.
Here the 2-dimensional structure introduces new subtleties.
For example, one side of  modification
$\mathfrak{l}$ in <Ref>
uses the pseudonatural transformation with components
$\lambda_A \tens B  : (\tensu A)  B \to A B$.
For $g : B \to B'$, the 2-cell witnessing pseudonaturality of this
transformation is the canonical isomorphism that interchanges $\lambda_A$ and $g$.
This 2-cell does not exist in a premonoidal bicategory, so instead we
must use the centrality witness $\lc{\lambda_A}_g$ for
Thus, we define $\mathfrak{l}$ to be a family of 2-cells
$\mathfrak{l}_{A, B} : (\lambda_A \rtie B) \To \lambda_{A
\tens B} \circ \alpha_{\tensu, A, B}$, pictured on the left below,
inducing modifications in $\homBicat{\B}{\B}$ of both types
on the right below:

\begin{equation*}
\begin{tikzcd}[column sep = .8em, row sep = 1em]
(\tensu  A)  B
\arrow{rr}{\lambda \rtie B}
\arrow[bend right = 12, swap]{dr}{\alpha_{\tensu, A, B}}
\:
\arrow[phantom]{d}{  \mathfrak{l}_{A, B} }
A B
\\
\:
\tensu (A  B)
\arrow[bend right = 12, swap]{ur}{\lambda_{A  \tens B}}
\:
\end{tikzcd}
\qquad
\begin{tikzcd}[column sep = -1em, row sep = 1em]
(\tensu \ltie -) \ltie B
\arrow{rr}{\lambda \rtie B}
\arrow[bend right = 12, swap]{dr}{\alpha_{\tensu, -, B}}
\:
\arrow[phantom]{d}{  \mathfrak{l}_{-, B} }
(- \rtie B)
\\
\:
\tensu \ltie (- \rtie B)
\arrow[bend right = 12, swap]{ur}{\lambda_{- \rtie B}}
\:
\end{tikzcd}
\qquad
\begin{tikzcd}[column sep = -1em, row sep = 1em]
(\tensu A) \ltie (-)
\arrow{rr}{  \lc{\lambda} }
\arrow[bend right = 12, swap]{dr}{\alpha_{\tensu, A, -}}
\:
\arrow[phantom]{d}{  \mathfrak{l}_{A, -} }
(A \ltie -)
\\
\:
\tensu \ltie (A \rtie -)
\arrow[bend right = 12, swap]{ur}{\lambda_{A \ltie -}}
\:
\end{tikzcd}
\end{equation*}

Notice that the middle diagram appears exactly as in the definition of
a monoidal bicategory; no adjustments are necessary because each
transformation is pseudonatural in the open argument without any
assumptions of centrality.

Modulo the subtleties just outlined, our main definition is a natural extension of the categorical one. We abuse notation by saying “$f$ is central” to mean $f$ comes with chosen $\lc{f}$ and $\rc{f}$ making $(f, \lc{f}, \rc{f})$ a central 1-cell and saying
“the pseudonatural transformation $\eta$ is central”
to mean each 1-cell component $\eta_A$ is central.

A premonoidal bicategory is a binoidal bicategory
$\binoidal{\baseCat}$ equipped with a unit object $\tensu \in \B$,
together with the following data:

* For every $A \in \baseCat$, central pseudonatural adjoint equivalences
$\lambda_A : \tensu \ltie A \to A$
$\rho_A : A \rtie \tensu \to A$;

* For every $A, B, C \in \baseCat$, an adjoint equivalence
$\alpha_{A, B, C} : (A \tens B)  \tens C \to A \tens (B \tens C)$
with 2-cells as in (<ref>) inducing central pseudonatural equivalences in each component separately;

* For each $A, B, C, D \in \baseCat$, invertible central 2-cells
$\mathfrak{p}_{A, B, C, D}, \mathfrak{m}_{A, B}, \mathfrak{l}_{A, B}$
and $\mathfrak{r}_{A, B}$, forming
modifications in each argument as in
or, if not shown there, as in a monoidal bicategory.

This data is subject to the same equations between 2-cells as in a monoidal bicategory.

Note that we cannot ask for the 2-cell components of the structural transformations to be central: for example, $\cellOf{\rho}_f$ has type
$\rho_{A'} \circ (f \rtie \tensu) \To f \circ \rho_A$,
but $f$ may not be a central map.
Also note that, although we have changed the conditions for
$\mathfrak{p}, \mathfrak{m}, \mathfrak{l}$ and $\mathfrak{r}$
to be modifications, their type as 2-cells has not changed, and thus
the equations for a monoidal bicategory are still well-typed.

Modification axioms for the structural 2-cells of a premonoidal bicategory,
where they differ from those of a monoidal
bicategory. (To save space we suppress $\ltie$ and $\rtie$: these can be inferred.)

Just as every premonoidal category has a centre, so does every premonoidal bicategory.

For a premonoidal category $\premonoidal{\baseCat}$, denote by
$\centreOf \baseCat$ the bicategory with the same objects, whose
1-cells and 2-cells are the central 1-cells and central 2-cells in
Composition is defined using composition in $\homBicat{\B}{\B}$, and the identity on $A$ is $\Id_A$ with the identity transformations.

The pseudofunctors $A \ltie (-)$ and $(-) \rtie B$ lift to the centre. Because
$A \ltie (-)$
is  a pseudofunctor, then for any central 1-cell
$(f, \lc{f}, \rc{f})$
we already have pseudonatural transformations
$A \ltie \lc{f}$
$A \ltie \rc{f}$
in $\B$.
To disambiguate between these transformations and the action of $A \ltie (-)$ on central 1-cells, we denote the latter by
$A \ltie (f, \lc{f}, \rc{f})
:= (A \ltie f, \lc{A \ltie f}, \rc{A \ltie f})$,
and likewise for $(-) \rtie B$.

Let $\premonoidal{\baseCat}$ be a premonoidal bicategory.
For every $A, B \in \baseCat$ the operations
$A \ltie (-)$
$(-) \rtie B$
induce pseudofunctors on $\centreOf\B$.

We only sketch the action of $X \ltie (-)$ and $(-) \rtie X$ on a central 1-cell
$(f, \lc{f}, \rc{f}) : A \to A'$. For $g : B \to B'$, the 2-cell
$\lc{X\ltie f}_g$ is uniquely determined by the equation

\begin{equation}
\label{eq:diag-bowtie-on-centre}
\input{diag-bowtie-on-centre}
\vspace{-3mm}
\end{equation}

in which, for clarity, we have omitted object names and left implicit the functors
$\ltie, \rtie$, which can be inferred. This is a valid definition for
$\lc{X \ltie f}_g$ because $\alpha$ is an equivalence, and all 2-cells involved are
We similarly construct 2-cells $\lc{f \rtie X}_g$, $\rc{X \ltie f}_g$,
$\rc{f \rtie X}_g$. The rest of the proof consists of routine

§.§ Examples of premonoidal bicategories

State-passing style.
Power & Robinson motivate their definition of premonoidal categories by considering an uncurried version of the State monad [37]: for a symmetric monoidal category $\monoidal\catC$ and an object $S \in \catC$ modelling a set of states, one can model a program from $A$ to $B$ interacting with the state as a morphism
$S \tens A \to S \tens B$.
The same applies bicategorically.

[ [37], <cit.>]

be a symmetric monoidal bicategory ( [45])
and $S \in \B$. Define a bicategory $\K$ with the same objects as $\B$, hom-categories
$\K(A, B) := \B(S \tens A, S \tens B)$,
and composition and identities as in $\B$.
Then $\K$ admits a canonical premonoidal structure.

For the binoidal structure, one whiskers with the canonical pseudonatural equivalences:

\begin{equation}
\begin{aligned}
\label{eq:binoidal-structure-for-State}
f \rtie B &:=
\big(
\xra{\simeq}
\xra{f \tens B}
\xra{\simeq}
\big) \\
A \ltie g &:=
\big(
\xra{\simeq}
\xra{A \tens g}
\xra{\simeq}
\big)
\end{aligned}
\end{equation}

The structural transformations are then given by composing the structural transformations in $\B$ with the naturality 2-cells for the equivalences in (<ref>).

*Bistrong graded monads.

It is well-known that if a monad $T$ on a monoidal category $\monoidal\catC$ is bistrong, meaning that it is equipped with a left strength
$t_{A,B} : A \tens TB \to T(A \tens B)$
and a right strength
$s_{A, B} : T(A) \tens B \to T(A \tens B)$,
and these strengths are compatible in the sense that the two canonical maps
$(A \tens T(B)) \tens C \to T{\big(A \tens  (B \tens C)\big)}$
are equal,
then $\catC_T$ is premonoidal
(see  [29]).
(This definition is obscured in the symmetric setting, because if $\catC$ is symmetric every strong monad is canonically bistrong.)
A similar fact applies to the Kleisli bicategory $\Kl_T$ for a graded monad defined in <Ref>.
To state this we need to define bistrong graded monads: we make a small adjustment to Katsumata's definition of strong graded monads
An endofunctor $T : \catC\to \catC$ equipped with two strengths
which are compatible in the sense above is called  bistrong (see  [29]).

A bistrong graded monad on a monoidal category $\monoidal\catC$ consists of a monoidal category
$(\catE, \bullet, \tensu)$
of grades and a lax monoidal functor
$T : \catE \to [\catC, \catC]_{\text{bistrong}}$,
$[\catC, \catC]_{\text{bistrong}}$
is the category of bistrong endofunctors and natural transformations that commute with both strengths (see  [29]).

Thus, a bistrong graded monad is a graded monad equipped with natural transformations
$t_{A, B}^e :  A \tens T_e(B) \to T_e(A \tens B)$
$s_{A, B}^e : T_e(A) \tens B \to T_e(A \tens B)$
for every grade $e$, compatible with the graded monad structure and with maps between grades.

One  then obtains strict pseudofunctors
$A \ltie (-), (-) \rtie B : \Kl_T \to \Kl_T$
for every $A, B \in \Kl_T$, defined similarly to the premonoidal structure on a Kleisli category:

\begin{equation*}
\begin{aligned}
A \ltie g \:\:&=\:\:
\big(
\xra{A \tens g}
\xra{t^e}
\big)
\quad
\quad
f \rtie B \:\:&=\:\:
\big(
\xra{f \tens B}
\xra{s^e}
\big).
\end{aligned}
\end{equation*}

Moreover, every $f \in \catC(A, A')$  determines a `pure' 1-cell
in $\Kl_T$, as
\para{f} := \big(A \xra{f} A' {\xra{\eta_{A'}} T_I A'} \big).
This 1-cell canonically determines a central 1-cell, with
given by the canonical isomorphism in $\catC$;
in particular,
$\lc{\tilde{f}}_{\tilde{g}} = (\rc{\tilde{g}}_{\tilde{f}})^{-1}$
for every $g \in \catC(B, B')$.
The structural transformations are then all of the form $\widetilde{\sigma}$ for $\sigma$ a structural transformation in $\catE$, and the structural modifications are all canonical isomorphisms of the form $\tensu^{\tens i} \xra\iso \tensu^{\tens j}$ for $i, j \in \Nat$.
Summarizing, we have the following.

Let $(T, \mu, \eta)$ be a bistrong graded monad on $\monoidal\catC$
with grades $(\catE, \bullet, \tensu)$.
Then the bicategory $\Kl_T$ has a canonical choice of premonoidal structure.

Unnatural transformations.
For any category $\catC$ the category
$[\catC, \catC]_{u}$
of functors and unnatural transformations
( families of maps $\sigma_C: {FC \to GC}$ with no further conditions)
is strictly premonoidal.
This is almost by definition, because  Power & Robinson define a strict premonoidal category to be a monoid with respect to the funny tensor product $\tens$ on the category $\Cat$ [37].
A version holds bicategorically.

[ [37]]
For any bicategory $\B$, let
$[\B, \B]_u$
denote the bicategory with objects pseudofunctors $F : \B \to \B$, 1-cells
$F \to G$
families of maps
$\{ \sigma_B : FB \to GB \st B \in \B \}$,
and 2-cells $\sigma \To \tau$ families of 2-cells
$\{ \modif_B : \sigma_B \To \tau_B  \st B \in \B \}$.
$[\B, \B]_u$
admits a premonoidal structure given by composition.

§ FREYD BICATEGORIES

We build up to our definition of Freyd bicategories in
stages. Although the
bicategories of values and computations have the same objects and
their structures are tightly connected,
bicategories offer a range of levels of strictness, so we must make
careful choices.

We begin with a useful technical notion for relating two pseudofunctors
which agree on objects:

For pseudofunctors $F, G : \B \to \C$ which agree on
objects, an icon $\theta : F \to G$ is an oplax natural transformation
whose 1-cell components are all identity. More explicitly, $\theta$
is a family of 2-cells $\theta_f : F(f) \to G(f)$ indexed by 1-cells of
$\B$, subject to naturality, identity and composition laws.

Using this, we define a notion of strict morphism between binoidal bicategories.

Let $\binoidal{\V}$ and $\binoidal{\B}$ be binoidal bicategories. A
0-strict binoidal pseudofunctor
is a pseudofunctor $\J : \V \to \B$
together  with families of invertible icons $\theta^A$ and
$\zeta^A$ (for $A \in \B$) as on the right; their existence implicitly requires that $\J(A \tens B) = \J A \tens \J B$.

\[
\begin{tikzcd}[
row sep = 2em,
column sep = 3em,
execute at end picture={
\foreach \nom in  {A,B,C, D}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) -- (B) -- (C) -- (D) -- (A);
\alias{A} \V
\arrow[phantom]{dr}{\twocellIso\zeta^A}
\arrow{r}{ (-) \rtie A}
\arrow[swap]{d}{\J}
\V
\arrow{d}[description]{\J}
\alias{D} \V
\arrow[phantom]{dl}{\twocellIso\theta^A}
\arrow{l}[swap]{A \ltie (-)}
\arrow{d}{\J}
\\
\alias{B} \B
\arrow[swap]{r}{(-) \rtie \J A}
\B
\alias{C} \B
\arrow{l}{\J A \ltie (-)}
\end{tikzcd}
\]

It is crucial that we take preservation up to icons, and not up to identity. In the context of <Ref>, for instance, we get a 0-strict binoidal pseudofunctor
$S \tens (-) :  \B \to \K$
with icons $\theta$ and $\zeta$ constructed using the pseudonaturality of the equivalences in (<ref>).
However, these icons do strictly commute with the premonoidal structure of $\K$ by the coherence of symmetric monoidal bicategories [15].
This suggests the following; for simplicity we focus on the case where $\J$ is identity-on-objects.

Let $\premonoidal{\V}$ and $\premonoidal{\B}$ be premonoidal
bicategories with the same objects and unit $I$. An identity-on-objects,
0-strict premonoidal pseudofunctor
$\V \to \B$ is a 0-strict binoidal pseudofunctor $(\J, \theta, \zeta)$ such that $\J$ is
identity-on-objects and the following axioms hold:

* $\J$ strictly preserves the components of the structural transformations:
for each $A, B, C \in \B$ we have
$\J \alpha_{A,B,C} =  \alpha_{A,B,C}, \J \lambda_A = \lambda_A$,
and $\J\rho_A = \rho_A$;

* $\J$ preserves structural 2-cells up to the icons $\theta$ and $\zeta$, according to the axioms in

A Freyd bicategory is an identity-on-objects
0-strict premonoidal pseudofunctor from a monoidal bicategory
of values
to a premonoidal bicategory of computations,
together with a choice of centrality witnesses for every
value. This choice must be functorial, coherent, and compatible
with the interchange law whenever two values are being
interchanged. We formalize this in terms of a strict
factorization through the centre $\centreOf \B$, as is done for
Freyd categories [26]. (Unlike for Freyd categories,
this factorization is additional structure and not a
property of the premonoidal pseudofunctor.)

A Freyd bicategory $\freydCat$ consists of a monoidal
bicategory $\monoidal\V$, a premonoidal bicategory, $\premonoidal{\B}$, an
identity-on-objects, 0-strict premonoidal pseudofunctor $\J : \V \to \B$, and a binoidal pseudofunctor $\J_{\centre}$ factoring $\J$ through the
centre of $\B$, as pictured below,

\[\begin{tikzcd}
\V && \B \\
& \centreOf\B
\arrow["\mathrm{forget}"', from=2-2, to=1-3]
\arrow["\J", from=1-1, to=1-3]
\arrow["{\J_\centre}"', dashed, from=1-1, to=2-2]
\end{tikzcd}\]

such that the following axioms hold, where we write
$(\J f, \lc{\J f}, \rc{\J f})$

* The chosen centrality witnesses for the structural 1-cells agree with those in the premonoidal structure of $\B$.

* For each value $f : A \to A'$, the chosen $\lc{\J f}$ satisfies the following
compatibility law for every $g \in \B(B, B')$ and $X\in
\B$. (This complements  the constructions of

\[\begin{tikzcd}
&& {} \\
{} &&& {} \\
&& {} \\
{} &&& {} \\
& {}
\arrow["{(fB)X}", from=2-1, to=1-3]
\arrow["\alpha", from=1-3, to=2-4]
\arrow[""{name=0, anchor=center, inner sep=0}, "{A'(gX)}", from=2-4, to=4-4]
\arrow["{f(B'X)}"', from=5-2, to=4-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "\alpha"', from=4-1, to=5-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{(Ag)X }"', from=2-1, to=4-1]
\arrow[""{name=3, anchor=center, inner sep=0}, "{(A'g)X}"{description}, from=1-3, to=3-3]
\arrow["{(fB')X}"{description}, from=4-1, to=3-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "\alpha"{description}, from=3-3, to=4-4]
\arrow["{\cellOf{\alpha}}"{description}, draw=none, from=1, to=4]
\arrow["{\cellOf{\alpha}}"{description}, draw=none, from=3, to=0]
\arrow["{\lc{\J f}_g \rtie X}"{description}, draw=none, from=2, to=3]
\end{tikzcd}
\quad = \quad
\begin{tikzcd}
&& {} \\
{} &&& {} \\
& {} \\
{} &&& {} \\
& {}
\arrow[""{name=0, anchor=center, inner sep=0}, "{(fB)X}", from=2-1, to=1-3]
\arrow["\alpha", from=1-3, to=2-4]
\arrow[""{name=1, anchor=center, inner sep=0}, "{A'(gX)}", from=2-4, to=4-4]
\arrow["{f(B'X)}"', from=5-2, to=4-4]
\arrow["\alpha"', from=4-1, to=5-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{(Ag)X }"', from=2-1, to=4-1]
\arrow[""{name=3, anchor=center, inner sep=0}, "{f(BX)}"{description}, from=2-4, to=3-2]
\arrow["\alpha"{description}, from=2-1, to=3-2]
\arrow[""{name=4, anchor=center, inner sep=0}, "{A(gX)}"{description}, from=3-2, to=5-2]
\arrow["{\cellOf{\alpha}}"{description}, draw=none, from=2, to=4]
\arrow["{\lc{\J f}_{g\rtie X}}"{description}, draw=none, from=4, to=1]
\arrow["{\cellOf{\alpha}}"{description}, draw=none, from=0, to=3]
\end{tikzcd}\]

For values
$x : X \to X'$ and $y : Y \to Y'$,
$\lc{\J x}_{\J y}$ and $\rc{\J y}_{J x}$ are determined by the interchange law in $\V$ (<ref>):

\[
\vspace{-2mm}
\begin{tikzcd}[
execute at end picture={
\foreach \nom in  {A,B,C}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=12pt}] (B) to[curve={height=12pt}] (A);
\fill[\extcolour,opacity=\opacity]
(B) to[curve={height=12pt}] (C) to[curve={height=12pt}] (B);
\alias{A} XY & \alias{B} {XY'} & \alias{C} {X'Y'} \\
& {X'Y}
\arrow["{\J(x) \rtie Y}"', curve={height=6pt}, from=1-1, to=2-2]
\arrow["{\J(Xy)}", curve={height=-10pt}, from=1-1, to=1-2]
\arrow["{X' \ltie \J y}"', curve={height=6pt}, from=2-2, to=1-3]
\arrow["{\J(xY')}", curve={height=-10pt}, from=1-2, to=1-3]
\arrow[curve={height=10pt}, from=1-2, to=1-3]
\arrow[curve={height=10pt}, from=1-1, to=1-2]
\arrow["\theta"{description}, draw=none, from=1-1, to=1-2]
\arrow["\zeta"{description}, draw=none, from=1-2, to=1-3]
\arrow["{\rc{\J y}_{\J x}}"{description, yshift = -1mm}, draw=none, from=1-2, to=2-2]
\arrow[
rounded corners,
to path=
{ -- ([yshift=.8cm]\tikztostart.north)
-| ([yshift=.8cm]\tikztotarget.south)
-- ([yshift=.6cm]\tikztotarget.south)
from=1-1, to=1-3
\arrow[
"\iso"{description, yshift=6mm},
from=1-1, to=1-3,
draw = none,
\arrow[
"\J(xy)"{description, yshift=12mm},
from=1-1, to=1-3,
draw = none,
\end{tikzcd}
\hspace{2mm}
\hspace{2mm}
\begin{tikzcd}[
execute at end picture={
\foreach \nom in  {A,B,C}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=12pt}] (B) to[curve={height=12pt}] (A);
\fill[\extcolour,opacity=\opacity]
(B) to[curve={height=12pt}] (C) to[curve={height=12pt}] (B);
\alias{A} XY  & \alias{B} {X'Y} & \alias{C} {X'Y'}
\arrow[""{name=0, anchor=center, inner sep=0}, "{\J(xY)}", curve={height=-10pt}, from=1-1, to=1-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\J(X'y)}", curve={height=-10pt}, from=1-2, to=1-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "{X' \ltie \J y}"', curve={height=10pt}, from=1-2, to=1-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\J(x) \rtie Y}"', curve={height=10pt}, from=1-1, to=1-2]
\arrow["\theta"{description}, draw=none, from=1, to=2]
\arrow["\zeta"{description}, draw=none, from=0, to=3]
\arrow[
rounded corners,
to path=
{ -- ([yshift=.8cm]\tikztostart.north)
-| ([yshift=.8cm]\tikztotarget.south)
-- ([yshift=.6cm]\tikztotarget.south)
from=1-1, to=1-3
\arrow[
"\iso"{description, yshift=6mm},
from=1-1, to=1-3,
draw = none,
\arrow[
"\J(xy)"{description, yshift=12mm},
from=1-1, to=1-3,
draw = none,
\end{tikzcd}
\hspace{2mm}
\hspace{2mm}
\begin{tikzcd}[
execute at end picture={
\foreach \nom in  {A,B,C}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=12pt}] (B) to[curve={height=12pt}] (A);
\fill[\extcolour,opacity=\opacity]
(B) to[curve={height=12pt}] (C) to[curve={height=12pt}] (B);
\alias{A} XY & \alias{B} {XY'} & \alias{C} {X'Y'} \\
& {X'Y}
\arrow["{\J(x) \rtie Y}"', curve={height=6pt}, from=1-1, to=2-2]
\arrow["{\J(Xy)}", curve={height=-10pt}, from=1-1, to=1-2]
\arrow["{X' \ltie \J y}"', curve={height=6pt}, from=2-2, to=1-3]
\arrow["{\J(xY')}", curve={height=-10pt}, from=1-2, to=1-3]
\arrow[curve={height=10pt}, from=1-2, to=1-3]
\arrow[curve={height=10pt}, from=1-1, to=1-2]
\arrow["\theta"{description}, draw=none, from=1-1, to=1-2]
\arrow["\zeta"{description}, draw=none, from=1-2, to=1-3]
\arrow["{\lc{\J x}_{\J y}}"{description, yshift=-1mm}, draw=none, from=1-2, to=2-2]
\arrow[
rounded corners,
to path=
{ -- ([yshift=.8cm]\tikztostart.north)
-| ([yshift=.8cm]\tikztotarget.south)
-- ([yshift=.6cm]\tikztotarget.south)
from=1-1, to=1-3
\arrow[
"\iso"{description, yshift=6mm},
from=1-1, to=1-3,
draw = none,
\arrow[
"\J(xy)"{description, yshift=12mm},
from=1-1, to=1-3,
draw = none,
\end{tikzcd}
\]

§.§ Examples of Freyd bicategories

Two of the examples of premonoidal bicategories from <Ref> naturally yield Freyd bicategories.
First, in the context of <Ref>, we have a pseudofunctor
$S \tens (-) : \B \to \K$
and icons $\theta$ and $\zeta$ constructed using the equivalences defining the binoidal structure
(recall (<ref>)).
Moreover, coherence for symmetric monoidal bicategories [15] gives a unique choice of 2-cell for each $\lc{S \tens f}_g$ and $\rc{S \tens f}_g$, so $S \tens (-)$ factors through the centre, yielding the following.

be a symmetric monoidal bicategory and let $\K$ be the premonoidal bicategory defined in
Then the pseudofunctor
$S \tens (-)$
defines a Freyd bicategory
$\B \to \K$.

Similarly, for a bistrong graded monad $T$, we can think of morphisms
in the base monoidal category $\catC$ as parameterized maps with
trivial parameter space, to construct a Freyd bicategory. The
identity-on-objects pseudofunctor has action on morphisms determined by
$\J(f) := \para{f} = \eta \circ f$.
The structural icons $\theta$ and $\zeta$ are the identity, and $\J$ factors strictly through the centre because every $ \para{f}$ has a canonical choice of centrality data.

Let $(T, \eta, \mu)$ be a bistrong graded monad on $\monoidal\catC$
with grades $(\catE, \bullet, \tensu)$.
Then, writing $\d\catC$ for the monoidal category $\catC$ viewed as a locally-discrete monoidal 2-category, there exists a canonical choice of pseudofunctor $\J$ making
$\J : \d\catC \to \Kl_T$
a Freyd bicategory.

Finally, recall the unnatural
transformations discussed in <Ref>: although one could expect the inclusion
$\iota : [\B, \B] \hookrightarrow [\B, \B]_u$
to be a Freyd bicategory, this is not true even in the categorical
setting: it is not the case that every natural transformation is
central, so $\iota$ does not factor through the centre.

§ FREYD BICATEGORIES AND ACTIONS

Freyd categories may equivalently be defined as certain actions of monoidal
categories ( [25]). In this section we show that this is also possible
in the two-dimensional setting.

We first define actions of monoidal bicategories.
As observed in [19], a left action on a category is equivalently a bicategory with two objects and certain hom-categories taken to be trivial. We therefore define a left action on a bicategory so it is equivalently a tricategory (see [13]) with two objects and certain hom-bicategories taken to be trivial.
It follows from the coherence of
tricategories ([13, 14]) that every diagram of
2-cells constructed using the structural data of an action must

A left action of a monoidal bicategory $(\V, \otimes, I)$ on a
bicategory $\B$ consists of a pseudo-functor
$\act : \V \times \B \to \B$,
together with the following data:

* Pseudonatural adjoint equivalences
$\actlambda_A : I \act A \to A$ and
$\actalpha_{X,Y,C} : {(X \otimes Y) \act C} \to X \act (Y \act C)$;

* Invertible modifications as shown below,
satisfying the same coherence axioms as $\pentagonator, \montrianglem$, and $\montrianglel$ in a monoidal bicategory ( [45]):

A right action $\ract : \B \times \V \to \B$
can be defined analogously, with a right unitor
$\actrho_A : A \ract I \to A$, an
$\actalpha_{A, X, Y} : (A \ract X) \ract Y \to A \ract (X \tens Y)$,
and 2-dimensional structural data.

Every monoidal bicategory $\V$ has canonical left and right actions on
itself given by the monoidal data. As we will see, a Freyd bicategory $\J : \V \to \B$
corresponds to a pair of actions $\act : \V \times \B \to \B$ and
$\ract : \B \times \V \to \B$
that extend the canonical actions: this mirrors the categorical situation.
To that end, we consider a category $\Vact$ of actions of $\V$ and
identity-on-objects pseudofunctors that preserve the action strictly on objects, but weakly on morphisms. (This is a very special
case of a more canonical notion of map between actions.)

Let $\V$ be a monoidal bicategory and let $(\B, \lact)$ and
$(\B', \lactprime)$ be left actions of $\V$. A 0-strict morphism of actions from
$(\B, \lact)$ to $(\B', \lactprime)$ is an
identity-on-objects functor $\J : \B \to \B'$
$\widetilde{\lambda^{\lact}_A} = \J(\widetilde{\lambda^{\lactprime}_A})$
$\widetilde{\alpha^{\lact}}_{\!\!A, B, C} = \J(\widetilde{\alpha^{\lactprime}}_{\!\!A, B, C})$
for every $A, B, C \in \B$,
equipped with an icon as on the right,
which relates the structural data for the actions according to the
axioms below:

execute at end picture=
in  A,B,C, D
() at (.center);
(A) – (C) – (D) – (B) – (A);

[Rightarrow, shorten = 8, "θ", from=C, to=B, xshift=0mm,yshift=-1mm]

A key example is the following:

For a monoidal bicategory $(\V, {}{\otimes}{}, I)$,
a left extension of the canonical action of $\V$ on itself
is a $\V$-action $(\B, \act)$, together with a 0-strict morphism $(\J,
\theta) : (\V, \tens) \to (\B, \act)$ such that $\theta$ is
invertible. (We say this is an extension along $\J$.)

Compatibility laws for <Ref>

We define a right extension analogously; this involves a right action
$\ract : \B \times \V \to \B$
and an invertible icon with components
$\zeta_{f, g} : f \ract \J g \To \J(f \tens g)$.
The rest of this section is devoted to showing
Freyd bicategories may be equivalently presented as pairs of extensions, which we call Freyd actions.

A Freyd action consists of an identity-on-objects pseudofunctor
$\J : \V \to \B$
from a monoidal bicategory
to a bicategory $\B$, together with:

* A left extension $(\lact, \theta)$ and right extension $(\ract, \zeta)$ along $\J$ of the canonical actions of $\V$ on itself;

* A pseudonatural adjoint equivalence
with 1-cell components
$\kappa_{X, B, Z} = \J(\alpha_{X, B, Z}) : (X \lact B) \ract Z \to X \lact (B \ract Z)$,
subject to the equation below
and additional axioms given in <Ref>:

\[
\begin{tikzcd}[
column sep = 3em,
row sep = 2em,
execute at end picture={
\foreach \nom in  {A,B,C, D,E, X, Y}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=35pt}] (B) to[curve={height=35pt}] (A);
\fill[\kcolour,opacity=\opacity]
(X) to (Y)  to (B) to[curve={height=-35pt}] (A) to (X);
\alias{X} {(XY)Z} & \alias{A} {X(YZ)} \\
\alias{Y} {(X'Y')Z'} & \alias{B} {X'(Y'Z')}
\arrow[""{name=0, anchor=center, inner sep=0}, "{(f \lact Jg) \ract h}"', from=1-1, to=2-1]
\arrow["\kappa", from=1-1, to=1-2]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=28pt}, from=1-2, to=2-2]
\arrow["\kappa"', from=2-1, to=2-2]
\arrow[""{name=2, anchor=center, inner sep=0}, from=1-2, to=2-2]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\J(f \tens (g \tens h))}"{}, curve={height=-28pt}, from=1-2, to=2-2]
\arrow["{\cellOf{\kappa}_{f, Jg, h}}"{description}, draw=none, from=0, to=1]
\arrow["{X' \lact \zeta}"{description}, shorten <=2pt, shorten >=2pt, Rightarrow, from=1, to=2]
\arrow["\theta"{description}, draw=none, from=2, to=3]
\end{tikzcd}
\hspace{2mm}
\hspace{2mm}
\begin{tikzcd}[
column sep = 3em,
row sep = 2em,
execute at end picture={
\foreach \nom in  {A,B,C, D,E}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=35pt}] (B) to[curve={height=35pt}] (A);
\alias{A} {(XY)Z} & {X(YZ)} \\
\alias{B} {(X'Y')Z'} & {X'(Y'Z')}
\arrow[""{name=0, anchor=center, inner sep=0}, "{(f \lact Jg) \ract h}"', curve={height=28pt}, from=1-1, to=2-1]
\arrow["{\J(\alpha)}", from=1-1, to=1-2]
\arrow["{\J(\alpha)}"', from=2-1, to=2-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\J(f \tens (g \tens h))}", from=1-2, to=2-2]
\arrow[""{name=2, anchor=center, inner sep=0}, from=1-1, to=2-1]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=-28pt}, from=1-1, to=2-1]
\arrow["{\J(\cellOf{\alpha}_{f,g,h})}"{description}, draw=none, shorten <=6pt, shorten >=6pt, Rightarrow, from=3, to=1]
\arrow["{\theta \ract Z}"{description}, draw=none, from=0, to=2]
\arrow["\zeta"{description}, draw=none, shorten <=4pt, shorten >=4pt, Rightarrow, from=2, to=3]
\end{tikzcd}
\]

We construct an equivalence of categories between Freyd actions and
Freyd bicategories, over a fixed identity-on-objects pseudofunctor $\J
: \V \to\B$. (The corresponding categorical result is a
bijection, but we must work modulo the structural
isomorphisms, and hence lose the strictness.)

On one side, the category $\FreydAct{}(\J)$ has
objects Freyd actions $(\lact, \theta, \ract, \zeta, \kappa)$ with
underlying pseudofunctor $\J$.
$((\lact, \theta), (\ract, \zeta), \kappa) \to ((\lact', \theta'), (\ract', \zeta), \kappa')$
are pairs of icons $\lefttrans : \lact \To \lact'$ and
$\righttrans : \ract \To \ract'$
fitting in the diagram in $\Vact$ as on the left below, such that
$\kappa$ is preserved as
on the right:

\[
\hspace{-2mm}
\begin{tikzcd}[column sep = 1.5em]
{(\B,\lact)} & {(\V, \tens)} & (\B, \ract) \\
{(\B, \lact')} & \: & (\B', \ract')
\arrow["{(\id_{\B}, \lefttrans)}"', from=1-1, to=2-1]
\arrow["{(J, \theta')}", from=1-2, to=2-1]
\arrow["{(J, \theta)}"', from=1-2, to=1-1]
\arrow["{(\id_{\B}, \righttrans)}"{}, from=1-3, to=2-3]
\arrow["{(J, \zeta')}", from=1-2, to=1-3]
\arrow["{(J, \zeta)}"', from=1-2, to=2-3]
\end{tikzcd}
\hspace{4mm}
\begin{tikzcd}[
column sep=1em, scalenodes=1,
execute at end picture={
\foreach \nom in  {A,B,C, D, Y, X}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=-30pt}] (B) to[curve={height=-30pt}] (A);
\fill[\kcolour,opacity=\opacity]
(A) to[curve={height=-30pt}] (B) -- (Y) -- (X) -- (A);
\alias{A} {(A B) C} && \alias{X} A(B C) \\
\alias{B} {(A' B') C'} && \alias{Y} {A' (B' C')}
\arrow["{\kappaprime}", from=1-1, to=1-3]
\arrow["{\kappaprime}"', from=2-1, to=2-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{f \lact' (b \ract' h)}",
from=1-3, to=2-3]
\arrow[""{name=1, anchor=center, inner sep=0},
curve={height=24pt}, from=1-1, to=2-1, ""{swap}] %
\arrow[""{name=2, anchor=center, inner sep=0}, %
from=1-1, to=2-1]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=0pt}, from=1-1, to=2-1]
\arrow[""{name=4, anchor=center, inner sep=0},
curve={height=-24pt}, from=1-1, to=2-1]
\arrow["\righttrans"{description}, draw=none, from=4, to=3]
\arrow["\lefttrans \ract h"{yshift=-2mm, xshift=.2mm}, draw=none, from=1, to=3]
\arrow["\oncell{\cellOf{(\kappaprime)}_{f, b, h}}"{description, xshift=4mm},
draw=none, from=2, to=0]
\end{tikzcd}
\hspace{0mm}
\hspace{0mm}
\begin{tikzcd}[
column sep=1em, scalenodes=1,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=28pt}] (B) to[curve={height=28pt}]  (A);
\fill[\kcolour,opacity=\opacity]
(A) to[curve={height=28pt}]  (B) -- (Y) -- (X);
\alias{X} {(AB)C} && \alias{A} {A(BC)} \\
\alias{Y} {(A'B')C'} && \alias{B} {A'(B'C')}
\arrow[""{name=0, anchor=center, inner sep=0}, "\kappaone", from=1-1, to=1-3]
\arrow["\kappa"', from=2-1, to=2-3]
\arrow[""{name=1, anchor=center, inner sep=0},
curve={height=22pt}, from=1-3, to=2-3] 		%
\arrow[""{name=2, anchor=center, inner sep=0}, %
from=1-1, to=2-1, "(f \lact b) \ract h"{swap}]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=0pt}, from=1-3, to=2-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "",
curve={height=-22pt}, from=1-3, to=2-3] %
\arrow["\oncell{{\cellOf{\kappaone}_{f, b, h}}}"{description}, draw=none, from=2, to=1]
\arrow["\oncell{{f \lact \righttrans}}"{yshift=-2mm,xshift=.17mm}, draw=none, from=1, to=3]
\arrow["\oncell{{\lefttrans}}"{description}, draw=none, from=3, to=4]
\end{tikzcd}
\]

On the other side, the category $\FreydBicat{\V, \J, \B}(\J)$ has
objects Freyd bicategories whose underlying pseudofunctor is $\J$;
these are determined by a premonoidal structure on $\B$ and families of
icons $\theta = \{ \theta^A \st A \in \B \}$ and $\{ \zeta^A \st A \in \B \}$
making the pseudofunctor $\J$ premonoidal.
$(\ltie, \rtie, \theta, \zeta) \to (\ltie', \rtie',\theta', \zeta')$
are families of icons $\lefttrans^A  : (A \ltie -) \To (A \ltie' -)$
and  $\righttrans^A  : (- \rtie A) \To (- \rtie' A)$
making the identity pseudofunctor $\B \to \B$ premonoidal and such
$(J, \theta', \zeta') \circ (\id_{\B}, \lefttrans, \righttrans) =
(J, \theta, \zeta)$
as premonoidal pseudofunctors.

Our correspondence theorem is then as follows.

For any monoidal bicategory $\monoidal{\V}$, bicategory $\B$, and
identity-on-objects pseudofunctor $\J : \V \to \B$, the categories
$\FreydAct{\V, \J, \B}(\J)$
$\FreydBicat{\V, \J, \B}(\J)$
are equivalent.

§ CONCLUSIONS

We have introduced bicategorical versions of premonoidal categories
and Freyd categories
Along the way we have observed subtleties that arise only in the
2-dimensional setting, and discussed simple canonical
examples. Finally, we have connected our theory to the existing literature by showing our definition is equivalent to certain actions in the expected way.

This paper develops abstract categorical notions, but these are
intended to be immediately practical. Specifically, the literature contains no satisfying account of
call-by-value languages in bicategories of games
([31, 3]), spans [6], or
profunctors [7], and this work offers a technical basis to fill that
gap. Our next steps will be in this direction.

This work takes place in a broader line of research on bicategorical
semantic structures, and there are several avenues to explore. We expect a tight connection between Freyd
bicategories and recently-developed notions of strength for
pseudomonads on monoidal bicategories ([46, 35, 42]).
Freyd bicategories should also be related to a 2-dimensional notion of
arrows, based on $\Cat$-valued profunctors, yet to be
developed ([16, 4]).

In particular,
the Kleisli bicategory of a strong pseudomonad should be premonoidal,
and the canonical functor from the base category should give a Freyd
structure, and conversely, a closed Freyd bicategory should be equivalent
to a strong pseudomonad together with Kleisli exponentials.
From a syntactic perspective, we expect cartesian Freyd bicategories to have an internal language similar to fine-grained call-by-value $\lambda$-calculus [26], with the addition of rewrites between terms
( [41, 17, 18, 8]).

In a more theoretical direction, although the centre of a premonoidal
category is always a monoidal category, this does not happen in the
bicategorical setting. Roughly speaking, for central $f$ and $g$, the
interchange of $f$ and $g$ is witnessed independently by 2-cells $\lc{f}_g$ and
$(\rc{g}_f)^{-1}$. This leads to ambiguity and it is not clear
how to define the pseudofunctor $\tens$; indeed, it is not even clear that these 2-cells are themselves central. In this paper we have shown that
the centre is a binoidal bicategory, and in further work we will give
a more complete description of its structure, along with
an alternative presentation of Freyd bicategories in terms of centrality

HP was supported by a Royal Society University Research Fellowship and by a Paris Region Fellowship co-funded by the European Union (Marie Skodowska-Curie grant agreement 945298).
PS was supported by the
Air Force Office of Scientific Research under award number FA9550-21-1-0038.
Both authors thank D. McDermott, N. Arkor, and the Oxford PL
group for useful discussions.

[1]
authorJ. C. Baez,
authorB. Fong & authorB. S.
Pollard (year2016):
titleA compositional framework for Markov processes.
journalJournal of Mathematical Physics
volume57(number3), 10.1063/1.4941578.

[2]
authorJ. Bénabou
(year1967): titleIntroduction to bicategories.
In: booktitleReports of the Midwest Category
Seminar, publisherSpringer Berlin Heidelberg,
addressBerlin, Heidelberg, pp. pages1–77,

[3]
authorS. Castellan,
authorP. Clairambault,
authorS. Rideau &
authorG. Winskel (year2017):
titleGames and Strategies as Event Structures.
journalLogical Methods in Computer Science
volumeVolume 13, Issue 3, 10.23638/LMCS-13(3:35)2017.

[4]
authorAlexander S Corner
(year2016): titleDay convolution for monoidal
Ph.D. thesis, schoolUniversity of Sheffield.

[5]
authorG. S. H. Cruttwell,
authorB. Gavranović,
authorN. Ghani,
authorP. Wilson &
authorF. Zanasi (year2022):
titleCategorical Foundations of Gradient-Based Learning.
In: booktitleProgramming Languages and
Systems, 10.1007/978-3-030-99336-8_1.

[6]
authorJ. L. Fiadeiro &
authorV. Schmitt (year2007):
titleStructured Co-spans: An Algebra of Interaction
In: booktitleAlgebra and Coalgebra in Computer
Science, pp. pages194–208, 10.1007/978-3-540-73859-6_14.

[7]
authorM. Fiore,
authorN. Gambino,
authorM. Hyland &
authorG. Winskel (year2007):
titleThe cartesian closed bicategory of generalised species
of structures.
journalJournal of the London Mathematical
Society volume77(number1), pp.
pages203–220, 10.1112/jlms/jdm096.

[8]
authorM. Fiore &
authorP. Saville (year2019):
titleA type theory for cartesian closed bicategories.
In: booktitle34th Annual ACM/IEEE Symposium on
Logic in Computer Science (LICS), 10.1109/LICS.2019.8785708.

[9]
authorB. Fong,
authorD. Spivak &
authorR. Tuyeras (year2019):
titleBackprop as Functor: A compositional perspective on
supervised learning.
In: booktitle34th Annual ACM/IEEE Symposium
on Logic in Computer Science (LICS), 10.1109/lics.2019.8785665.

[10]
authorM. Gaboardi,
authorS. Katsumata,
authorD. Orchard &
authorT. Sato (year2021):
titleGraded Hoare Logic and its Categorical Semantics.
In: booktitleProgramming Languages and
Systems, pp. pages234–263, 10.1007/978-3-030-72019-3_9.

[11]
authorZ. Galal (year2020):
titleA Profunctorial Scott Semantics.
In: booktitle5th International Conference on
Formal Structures for Computation and Deduction (FSCD 2020),

[12]
authorF. R. Genovese,
authorJ. Herold,
authorF. Loregian &
authorD. Palombi (year2021):
titleA Categorical Semantics for Hierarchical Petri
journalElectronic Proceedings in Theoretical
Computer Science volume350, pp. pages51–68,

[13]
authorR. Gordon, authorA. J.
Power & authorR. Street (year1995): titleCoherence
for tricategories.
publisherMemoirs of the American Mathematical Society,

[14]
authorN. Gurski (year2013):
titleCoherence in Three-Dimensional Category Theory.
publisherCambridge University Press,

[15]
authorN. Gurski &
authorA. Osorno (year2013):
titleInfinite loop spaces, and coherence for symmetric
monoidal bicategories.
journalAdvances in Mathematics
volume246, pp. pages1 – 32,

[16]
authorC. Heunen &
authorB. Jacobs (year2006):
titleArrows, like Monads, are Monoids.
In: booktitle22nd Annual Conference on
Mathematical Foundations of Programming Semantics (MFPS),

[17]
authorB. P. Hilken (year1996):
titleTowards a proof theory of rewriting: the simply typed
journalTheoretical Computer Science
volume170(number1), pp. pages407–444,

[18]
authorT. Hirschowitz
(year2013): titleCartesian closed 2-categories
and permutation equivalence in higher-order rewriting.
journalLogical Methods in Computer Science
volume9, pp. pages1–22,

[19]
authorG. Janelidze &
authorG. M. Kelly
(year2001): titleA note on actions of a monoidal
journalTheory and Applications of Categories
volume9(number4), pp. pages61–91.
noteAvailable at

[20]
authorA. Jeffrey (year1997):
titlePremonoidal categories and a graphical view of

[21]
authorS. Katsumata (year2014):
titleParametric effect monads and semantics of effect
In: booktitle41st ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages (POPL),

[22]
authorA. Kerinec,
authorG. Manzonetto &
authorF. Olimpieri
(year2023): titleWhy Are Proofs Relevant in
Proof-Relevant Models?
journalProceedings of the ACM on Programming
Languages (POPL), 10.1145/3571201.

[23]
authorS. Lack (year2008):
journalApplied Categorical Structures
volume18(number3), pp. pages289–307,

[24]
authorT. Leinster (year2004):
titleHigher operads, higher categories.
seriesLondon Mathematical Society Lecture Note
Series volume298, publisherCambridge University
Press, 10.1017/CBO9780511525896.

[25]
authorP. B. Levy (year2003):
titleCall-By-Push-Value: A Functional/Imperative
publisherSpringer Netherlands,

[26]
authorP. B. Levy,
authorJ. Power &
authorH. Thielecke
(year2003): titleModelling environments in
call-by-value programming languages.
journalInformation and Computation
volume185(number2), pp. pages182–210,

[27]
authorS. Mac Lane &
authorR. Paré
(year1985): titleCoherence for bicategories and
indexed categories.
journalJournal of Pure and Applied Algebra
volume37, pp. pages59 – 80,

[28]
authorD. McDermott &
authorT. Uustalu (year2022):
titleFlexibly Graded Monads and Graded Algebras.
In: booktitleLecture Notes in Computer
Science, publisherSpringer International Publishing, pp.
pages102–128, 10.1007/978-3-031-16912-0_4.

[29]
authorD. McDermott &
authorT. Uustalu (year2022):
titleWhat Makes a Strong Monad?
journalElectronic Proceedings in Theoretical
Computer Science volume360, pp. pages113–133,

[30]
authorP.-A. Melliès
(year2012): titleParametric monads and enriched
noteAvailable at
<https://www.irif.fr/ mellies/tensorial-logic/8-parametric-monads-and-enriched-adjunctions.pdf>.

[31]
authorP.-A. Melliès
(year2021): titleAsynchronous Template Games and
the Gray Tensor Product of 2-Categories.
In: booktitle36th Annual ACM/IEEE Symposium
on Logic in Computer Science (LICS),

[32]
authorE. Moggi (year1989):
titleComputational lambda-calculus and monads.
In: booktitleProceedings, Fourth Annual
Symposium on Logic in Computer Science, publisherIEEE Comput.
Soc. Press, 10.1109/lics.1989.39155.

[33]
authorE. Moggi (year1991):
titleNotions of computation and monads.
journalInformation and Computation
volume93(number1), pp. pages55–92,

[34]
authorF. Olimpieri (year2021):
titleIntersection Type Distributors.
In: booktitle36th Annual ACM/IEEE Symposium
on Logic in Computer Science (LICS),

[35]
authorH. Paquet &
authorP. Saville (year2023):
titleStrong pseudomonads and premonoidal bicategories.

[36]
authorJ. Power (year2002):
titlePremonoidal categories as categories with algebraic
journalTheoretical Computer Science
volume278(number1-2), pp. pages303–321,

[37]
authorJ. Power &
authorE. Robinson
(year1997): titlePremonoidal categories and
notions of computation.
journalMathematical Structures in Computer
Science volume7(number5), pp.
pages453–468, 10.1017/s0960129597002375.

[38]
authorJ. Power &
authorH. Thielecke
(year1997): titleEnvironments, continuation
semantics and indexed categories.
In: booktitleLecture Notes in Computer
Science, publisherSpringer Berlin Heidelberg, pp.
pages391–414, 10.1007/bfb0014560.

[39]
authorM. Román
(year2022): titlePromonads and String Diagrams
for Effectful Categories.
journalCoRR volumeabs/2205.07664,

[40]
authorC. J. Schommer-Pries
(year2009): titleThe Classification of
Two-Dimensional Extended Topological Field Theories.
Ph.D. thesis, schoolUniversity of California.

[41]
authorR. A. G. Seely
(year1987): titleModelling Computations: A
2-Categorical Framework.
In: booktitle2nd Annual IEEE Symp. on Logic in
Computer Science (LICS).

[42]
authorA. Slattery (year2023):
titlePseudocommutativity and Lax Idempotency for Relative

[43]
authorA. L. Smirnov
(year2008): titleGraded monads and rings of
journalJournal of Mathematical Sciences
volume151(number3), pp. pages3032–3051,

[44]
authorS. Staton (year2017):
titleCommutative Semantics for Probabilistic Programming.
In: booktitleProgramming Languages and
Systems, publisherSpringer Berlin Heidelberg, pp.
pages855–879, 10.1007/978-3-662-54434-1_32.

[45]
authorM. Stay (year2016):
titleCompact Closed Bicategories.
journalTheories and Applications of Categories
volume31(number26), pp. pages755–798.

[46]
authorM. Tanaka (year2005):
titlePseudo-Distributive Laws and a Unified Framework for
Variable Binding.
Ph.D. thesis, schoolUniversity of Edinburgh.

[47]
authorH. Thielecke (year1997):
titleContinuation Semantics and Self-adjointness.
journalElectronic Notes in Theoretical Computer
Science volume6, pp. pages348–364,

[48]
authorT. Tsukada,
authorK. Asada &
authorC.-H. L. Ong
(year2018): titleSpecies, Profunctors and
Taylor Expansion Weighted by SMCC.
In: booktitle33rd Annual ACM/IEEE Symposium
on Logic in Computer Science (LICS), 10.1145/3209108.3209157.

[49]
authorL. Wester Hansen &
authorM. Shulman (year2019):
titleConstructing symmetric monoidal bicategories

§ MISSING COHERENCE AXIOMS FOR DEFINITION 22

We complete the list of coherence equations for
<Ref>. In the diagrams that follow, we consider $b : B \to B'$
and $c : C \to C'$ in $\B$ and, for $f : A \to A'$ and $g : B \to B'$
in $\V$, we write $\nu$ for the composite $\J f \ract g \XRA{\zeta}
\J(f \tens g) \XRA{\theta} f \lact \J g$.
In <Ref>, $\kappa$ represents the
pseudonaturality of the associator $\alpha$ in its middle argument,
and these axioms enforce the appropriate modification conditions
( <Ref>).

\[
\hspace{-1mm}
\begin{minipage}{0.5\textwidth}
\[
\begin{tikzcd}[
column sep = 1.3em,
scalenodes = .8,
execute at end picture={
\foreach \nom in  {A,B,C, D, X}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=9pt}] (B) to[curve={height=9pt}] (A);
\fill[\monoidallcolour,opacity=\opacity]
(A) to[curve={height=9pt}] (B) to (C) to (A);
\fill[\kcolour,opacity=\opacity]
(A) to (C) to (D) to (X);
\alias{A} {(IA)B} && \alias{B} AB \\
\alias{X} {(IA')B} & \alias{C} {I(AB)} & {A'B} \\
& \alias{D} {I(A'B)}
\arrow["\alpha"'{description}, from=1-1, to=2-2]
\arrow["\lambda"'{description},, from=2-2, to=1-3]
\arrow[""{name=0, anchor=center, inner sep=0}, from=2-2, to=3-2]
\arrow[""{name=1, anchor=center, inner sep=0},  from=1-1, to=2-1]
\arrow["\alpha"', from=2-1, to=3-2]
\arrow["\lambda"', from=3-2, to=2-3]
\arrow[""{name=2, anchor=center, inner sep=0}, from=1-3, to=2-3, "{a \ract B}"]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\lambda \ract B}", curve={height=-8pt}, from=1-1, to=1-3]
\arrow[""{name=4, anchor=center, inner sep=0}, curve={height=8pt}, from=1-1, to=1-3]
\arrow["\acttrianglel^{\lact}"{description,yshift=0mm}, draw=none, from=4, to=2-2]
\arrow["\nu"{description}, shorten <=2pt, shorten >=2pt, Rightarrow, from=3, to=4]
\arrow["{\cellOf{\kappa}_{I, a, B}}"{description}, draw=none, from=1, to=0]
\arrow["{\cellOf{\lactlambda}}"{description}, draw=none, from=2, to=0]
\end{tikzcd}
\hspace{-1mm}
\hspace{-3mm}
\begin{tikzcd}[
column sep = -.1em,
scalenodes = .8,
execute at end picture={
\foreach \nom in  {A,B,C, D, X}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=8pt}] (B) to[curve={height=9pt}] (A);
\fill[\monoidallcolour,opacity=\opacity]
(A) to[curve={height=8pt}] (B) to (C) to (A);
{(IA)B} && AB \\
\alias{A} {(IA')B} && \alias{B} {A'B} \\
& \alias{C} {I(A'B)}
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=2-1, "{(I \lact a) \ract B}"']
\arrow[""{name=1, anchor=center, inner sep=0}, "\alpha"', from=2-1, to=3-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "\lambda"', from=3-2, to=2-3]
\arrow[""{name=3, anchor=center, inner sep=0}, from=1-3, to=2-3]
\arrow["{\lambda \ract B}", curve={height=-6pt}, from=1-1, to=1-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "{\lambda \ract B}", curve={height=-6pt}, from=2-1, to=2-3]
\arrow[""{name=5, anchor=center, inner sep=0}, curve={height=6pt}, from=2-1, to=2-3]
\arrow["{\cellOf{\lactlambda} \ract B}"{description, yshift=3mm}, draw=none, from=0, to=3]
\arrow["{\acttrianglel^{\lact}}"{description, yshift=1mm}, draw=none, from=1, to=2]
\arrow["\nu"{description}, shorten <=2pt, shorten >=2pt, Rightarrow, from=4, to=5]
\end{tikzcd}
\]
\end{minipage}
\hspace{2mm}
\begin{minipage}{0.5\textwidth}
\[
\begin{tikzcd}[
column sep = 1.45em,
scalenodes = .8,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y, Z}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=9pt}] (B) to[curve={height=11pt}] (A);
\fill[\actlcolour,opacity=\opacity]
(X) to[curve={height=-11pt}] (B) to[curve={height=11pt}] (A) to (X);
\fill[\kcolour,opacity=\opacity]
(X) to (A) to (Z) to (Y);
\alias{X} {(AB)I} && \alias{B} AB \\
\alias{Y} {(AB')I} & \alias{A} {A(BI)} & {AB'} \\
& \alias{Z} {A(B'I)}
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=2-1]
\arrow["\alpha"', from=2-1, to=3-2]
\arrow["{A \lact \rho}"', curve={height=6pt}, from=3-2, to=2-3]
\arrow[""{name=1, anchor=center, inner sep=0}, from=1-3, to=2-3, "{A \lact b}"]
\arrow[""{name=2, anchor=center, inner sep=0}, "\rho", curve={height=-10pt}, from=1-1, to=1-3]
\arrow["\alpha"{description}, from=1-1, to=2-2]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=6pt}, from=2-2, to=1-3]
\arrow[""{name=4, anchor=center, inner sep=0}, from=2-2, to=3-2]
\arrow[""{name=5, anchor=center, inner sep=0}, curve={height=-10pt}, from=2-2, to=1-3]
\arrow["{\acttriangler^{\ract}}"{description}, draw=none, from=2, to=2-2]
\arrow["\nu"{description}, draw=none, from=5, to=3]
\arrow["{\cellOf{\kappa}_{A, b, I}}"{description, xshift=.5mm, yshift=-.5mm}, draw=none, from=0, to=4]
\arrow["{A \lact \cellOf{\ractlambda}}"{description, xshift = -.5mm, yshift = .5mm}, curve={height=6pt}, draw=none, from=4, to=1]
\end{tikzcd}
\hspace{-1mm}
\hspace{-3mm}
\begin{tikzcd}[
column sep = -.1em,
scalenodes = .8,
execute at end picture={
\foreach \nom in  {A,B,C, D, X}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=8pt}] (B) to[curve={height=10pt}] (A);
\fill[\actlcolour,opacity=\opacity]
(A) to[curve={height=-10pt}] (B) to[curve={height=11pt}] (C) to (A);
{(AB)I} && AB \\
\alias{C} {(AB')I} && \alias{B} {AB'} \\
& \alias{A} {A(B'I)}
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=2-1, "{(A \lact b) \ract I}"']
\arrow["\alpha"', from=2-1, to=3-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{A \lact \rho}"', curve={height=6pt}, from=3-2, to=2-3]
\arrow[""{name=2, anchor=center, inner sep=0},from=1-3, to=2-3]
\arrow["\rho", curve={height=-6pt}, from=1-1, to=1-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "\rho"{description}, curve={height=-9pt}, from=2-1, to=2-3]
\arrow[""{name=4, anchor=center, inner sep=0}, curve={height=-9pt}, from=3-2, to=2-3]	%
\arrow["\nu"{description}, draw=none, from=4, to=1]
\arrow["{\acttriangler^{\ract}}"{description, yshift=2mm}, draw=none, from=3, to=3-2]
\arrow["{\cellOf{\ractlambda}}"{description, yshift=2mm}, draw=none, from=0, to=2]
\end{tikzcd}
\]
\end{minipage}
\]

\[
\begin{tikzcd}[
row sep = 1em,
column sep = 3em,
scalenodes = .9,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y, Z, W}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=10pt}] (B) to[curve={height=10pt}] (A);
\fill[\actpcolour,opacity=\opacity]
(X) to (B) to[curve={height=10pt}] (A) to (Y) to (X);
\fill[\kcolour,opacity=\opacity]
(Z) to (X) to (Y) to (A) to (W) to (Z);
\alias{Z} {((AB)C)D} && \alias{X} {((AB')C)D} \\
{(A(BC)))D} & \alias{Y} {(A(B'C))D} \\
\alias{W} {A((BC)D)} & \alias{A} {A((B'C)D)} \\
{A(B(CD))} && \alias{B} {A(B'(CD))}
\arrow["{((A \lact b) \ract C) \ract D}", from=1-1, to=1-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\alpha \ract D}"{description}, from=1-3, to=2-2]
\arrow[""{name=1, anchor=center, inner sep=0}, from=2-2, to=3-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{A \ract \alpha}", curve={height=-8pt}, from=3-2, to=4-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\alpha \circ\alpha}", from=1-3, to=4-3]
\arrow[""{name=4, anchor=center, inner sep=0}, curve={height=8pt}, from=3-2, to=4-3]
\arrow[""{name=5, anchor=center, inner sep=0}, "{\alpha \ract D}"', from=1-1, to=2-1]
\arrow[""{name=6, anchor=center, inner sep=0}, "\alpha"', from=2-1, to=3-1]
\arrow[""{name=7, anchor=center, inner sep=0}, "{A \lact \alpha}"', from=3-1, to=4-1]
\arrow["{A \lact (b \ract CD)}"', from=4-1, to=4-3]
\arrow[from=3-1, to=3-2]
\arrow[from=2-1, to=2-2]
\arrow["\nu"{description}, draw=none, from=2, to=4]
\arrow["{\actpentagonator^{\ract}}"{description, xshift=2mm, yshift=1mm}, draw=none, from=1, to=3]
\arrow["{\cellOf{\kappa}_{A, b, C} \ract D}"{description}, draw=none, from=5, to=0]
\arrow["{\cellOf{\kappa}_{A, b \ract C, D}}"{description}, draw=none, from=6, to=1]
\arrow["{A \lact \cellOf{\ractalpha}}"{description, xshift=-1mm, yshift =1mm}, draw=none, from=7, to=4]
\end{tikzcd}
\hspace{1mm}
\hspace{1mm}
\begin{tikzcd}[
row sep = 1em,
column sep = 3em,
scalenodes = .9,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y, Z, U}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=8pt}] (B) to[curve={height=8pt}] (A);
\fill[\actpcolour,opacity=\opacity]
(U) to (Z) to (B) to[curve={height=8pt}] (A) to (U);
\fill[\kcolour,opacity=\opacity]
(Z) to (X) to (Y) to (B) to (Z);
\alias{U} {((AB)C)D} && {((AB')C)D} \\
{(A(BC)))D} & \alias{Z} {(AB)(CD)} & \alias{X} {(AB')(CD)} \\
\alias{A} {A((BC)D)} \\
\alias{B} {A(B(CD))} && \alias{Y} {A(B'(CD))}
\arrow["{((A \lact b) \ract C) \ract D}", from=1-1, to=1-3]
\arrow["{\alpha \ract D}"', from=1-1, to=2-1]
\arrow[""{name=0, anchor=center, inner sep=0}, "\alpha"', from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{A \lact \alpha}"', curve={height=6pt}, from=3-1, to=4-1]
\arrow["{A \lact (b \ract CD)}"', from=4-1, to=4-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "\alpha", from=1-3, to=2-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "\alpha", from=2-3, to=4-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "\alpha"{description}, from=1-1, to=2-2]
\arrow[""{name=5, anchor=center, inner sep=0}, "\alpha"{description}, from=2-2, to=4-1]
\arrow[from=2-2, to=2-3]
\arrow[""{name=6, anchor=center, inner sep=0}, curve={height=-6pt}, from=3-1, to=4-1]
\arrow["\nu"{description}, draw=none, from=1, to=6]
\arrow["{\cellOf{\kappa}_{A, b, CD}}"{description}, draw=none, from=5, to=3]
\arrow["{\cellOf{\ractalpha}}"{description}, draw=none, from=4, to=2]
\arrow["{\actpentagonator^{\ract}}"{description, xshift = 2mm}, draw=none, from=0, to=2-2]
\end{tikzcd}
\]

\[
\begin{tikzcd}[
row sep = 1em,
column sep = 3em,
scalenodes = .9,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y, Z, W, F}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=10pt}] (B) to[curve={height=10pt}] (A);
\fill[\actpcolour,opacity=\opacity]
(X) to (B) to[curve={height=10pt}] (A) to (Y) to (X);
\fill[\kcolour,opacity=\opacity]
(W) to (Y) to (A) to[curve={height=10pt}] (B) to (F) to (W);
\alias{Z} {((AB)C)D} && \alias{X} {((AB)C')D} \\
\alias{W} {(A(BC)))D} & \alias{Y} {(A(BC'))D} \\
{A((BC)D)} & \alias{A} {A((BC')D)} \\
\alias{F} {A(B(CD))} && \alias{B} {A(B(C'D))}
\arrow["{(AB \lact c) \ract D}", from=1-1, to=1-3]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\alpha \ract D}"{description}, from=1-3, to=2-2]
\arrow[""{name=1, anchor=center, inner sep=0}, from=2-2, to=3-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{A \ract \alpha}", curve={height=-8pt}, from=3-2, to=4-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "{\alpha \circ\alpha}", from=1-3, to=4-3]
\arrow[""{name=4, anchor=center, inner sep=0}, curve={height=8pt}, from=3-2, to=4-3]
\arrow[""{name=5, anchor=center, inner sep=0}, "{\alpha \ract D}"', from=1-1, to=2-1]
\arrow[""{name=6, anchor=center, inner sep=0}, "\alpha"', from=2-1, to=3-1]
\arrow[""{name=7, anchor=center, inner sep=0}, "{A \lact \alpha}"', from=3-1, to=4-1]
\arrow["{A \lact (B \lact (c \ract D)}"', from=4-1, to=4-3]
\arrow[from=3-1, to=3-2]
\arrow[from=2-1, to=2-2]
\arrow["\nu"{description}, draw=none, from=2, to=4]
\arrow["{\actpentagonator^{\ract}}"{description}, draw=none, from=1, to=3]
\arrow["{\cellOf{\lactalpha} \ract D}"{description}, draw=none, from=5, to=0]
\arrow["{\cellOf{\kappa}_{A, B \lact c, D}}"{description}, draw=none, from=6, to=1]
\arrow["{A \lact \cellOf{\kappa}_{B, c, D}}"{description}, draw=none, from=7, to=4]
\end{tikzcd}
\hspace{1mm}
\hspace{1mm}
\begin{tikzcd}[
row sep = 1em,
column sep = 3em,
scalenodes = .9,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y, Z, U, F}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=8pt}] (B) to[curve={height=8pt}] (A);
\fill[\actpcolour,opacity=\opacity]
(U) to (Z) to (B) to[curve={height=8pt}] (A) to (U);
\fill[\kcolour,opacity=\opacity]
(F) to (D) to (X) to (Z);
\alias{F} {((AB)C)D} && \alias{D} {((AB)C')D} \\
{(A(BC)))D} & \alias{Z} {(AB)(CD)} & \alias{X} {(AB)(C'D)} \\
\alias{A} {A((BC)D)} \\
\alias{B} {A(B(CD))} && \alias{Y} {A(B(C'D))}
\arrow["{((AB \lact c) \ract D}", from=1-1, to=1-3]
\arrow["{\alpha \ract D}"', from=1-1, to=2-1]
\arrow[""{name=0, anchor=center, inner sep=0}, "\alpha"', from=2-1, to=3-1]
\arrow[""{name=1, anchor=center, inner sep=0}, "{A \lact \alpha}"', curve={height=6pt}, from=3-1, to=4-1]
\arrow["{A \lact (B \lact (c \ract D)}"', from=4-1, to=4-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "\alpha", from=1-3, to=2-3]
\arrow[""{name=3, anchor=center, inner sep=0}, "\alpha", from=2-3, to=4-3]
\arrow[""{name=4, anchor=center, inner sep=0}, "\alpha"{description}, from=1-1, to=2-2]
\arrow[""{name=5, anchor=center, inner sep=0}, "\alpha"{description}, from=2-2, to=4-1]
\arrow[from=2-2, to=2-3]
\arrow[""{name=6, anchor=center, inner sep=0}, curve={height=-6pt}, from=3-1, to=4-1]
\arrow["\nu"{description}, draw=none, from=1, to=6]
\arrow["{\cellOf{\lactalpha}}"{description}, draw=none, from=5, to=3]
\arrow["{\cellOf{\kappa}_{AB, c, D}}"{description}, draw=none, from=4, to=2]
\arrow["{\actpentagonator^{\ract}}"{description, xshift = 2mm}, draw=none, from=0, to=2-2]
\end{tikzcd}
\]

§ PROOFS FOR  SECTION 4

§.§ From Freyd action to Freyd bicategory

Fix a Freyd action
$(\lact, \theta, \ract, \zeta, \kappa)$
$\J : \V \to \B$.
We construct a Freyd bicategory with the same underlying pseudofunctor.
For the unit of the premonoidal structure we take the unit $\tensu$ for $\V$.
Next define
$A \ltie (-) := A \lact (-)$
$(-) \rtie B := (-) \ract B$.
The icons $\theta$ and $\zeta$ for the Freyd action then determine the required icons component-wise:

\[
A \ltie J(-) =  A \lact (-) \XRA{\theta_{A, -}} \J(A \tens -)
\qquad,\qquad
\J(-) \rtie B  =  J(-) \ract B \XRA{\zeta_{-, B}} \J(- \tens B).
\]

The left- and right unitors are given by
$\actlambda^{\lact} : IA \to A$
$\actlambda^{\ract} : AI \to A$
respectively, and the associator by $\J(\alpha)$ with 2-cell components given by the witnessing 2-cells for
The compatibility laws of a Freyd action immediately give the compatibility laws of a Freyd bicategory.
Similarly, the structural modifications are wholly determined by the definition of a Freyd bicategory: for example, the pentagonator $\pentagonator$ in $\B$ is $\J(\pentagonator)$ composed with $\theta$ and $\zeta$ as in <Ref>.
The axioms of a premonoidal bicategory are then checked using the compatibility laws and the corresponding axioms in $\V$.

It remains to show that the 2-cell components of $\theta$ and $\zeta$ are central and that $\J$ factors through the centre. The former is a short direct calculation. For the latter, for
$f : X \to X'$
in $\V$ and
$a : A \to A'$
in $\B$ we define $\lc{f}_a$
using $\theta, \zeta$ and the interchange laws for the pseudofunctors underlying the actions as in the diagram to the right; $\rc{f}_a$ is similar.
We write
$\nu$ for the composite
$\J f \ract g \XRA{\zeta} \J(f \tens g) \XRA{\theta} f \lact \J g$.

\[
\lc{\J f}_a :=
\begin{tikzcd}[
row sep = 4em,
column sep = 5em,
execute at end picture={
\foreach \nom in  {A,B,C, D, X, Y}
{\coordinate (\nom) at (\nom.center);}
\fill[\extcolour,opacity=\opacity]
(A) to[curve={height=14pt}] (B) to[curve={height=14pt}] (A);
\fill[\extcolour,opacity=\opacity]
(X) to[curve={height=14pt}] (Y) to[curve={height=14pt}] (X);
\alias{A} XA & \alias{B} {X'A} \\
\alias{X} {XA'} & \alias{Y} {X'A'}
\arrow[""{name=0, anchor=center, inner sep=0}, "{X \lact a}"{description}', from=1-1, to=2-1]
\arrow[""{name=2, anchor=center, inner sep=0}, "{X' \lact a}"{description}, from=1-2, to=2-2]
\arrow["{f \lact A'}"{name = 3}, curve={height=-12pt}, from=2-1, to=2-2]
\arrow["{\J(f) \ract A}"{name = 4}, curve={height=-12pt}, from=1-1, to=1-2]
\arrow[""{name=5, anchor=center, inner sep=0}, "{f \lact A}"{swap}, curve={height=12pt}, from=1-1, to=1-2]
\arrow[""{name=7, anchor=center, inner sep=0}, "{\J(f) \ract A'}"', curve={height=12pt}, from=2-1, to=2-2]
\arrow["\cong"{description}, draw=none, from=0, to=2]
\arrow["\nu"{description}, draw=none, from=4, to=5]
\arrow["\nu"{description}, draw=none, from=3, to=7]
\end{tikzcd}
\]

Thus, we define $\J'(f) := (f, \lc{\J f}, \rc{\J f})$.
For any 2-cell $\sigma : f \To f'$ in $\V$, we get that $\J(\sigma)$ is natural by naturality of all the data defining $\lc{\J f}$ and $\rc{\J f}$.
Finally, one shows that the unit and compositor for $\J$ are central using the identity and composition laws of the icons $\theta$ and $\zeta$.

In summary, we have the following:

Every Freyd action with underlying pseudofunctor
$\J : \V \to \B$
determines a Freyd bicategory with the same underlying pseudofunctor.

§.§ From Freyd bicategory to Freyd action

Let $\freydCat = (\V \xra{\J} \B)$ be a Freyd bicategory.
First we shall show how to construct a left action
$\lact : \V \times \B \to B$;
the right action is constructed similarly.
Thereafter we shall show how to construct the rest of the data for a Freyd action.

*From Freyd bicategory to a left action.

\[
\begin{tikzcd}[row sep = 1.8em, column sep = 3em]
XB \\
{X'B} & {X''B} \\
{X'B'} & {X''B'} & {X''B''}
\arrow["{\J(f) \rtie B}"', from=1-1, to=2-1]
\arrow[""{name=0, anchor=center, inner sep=0}, "{X' \rtie b}"', from=2-1, to=3-1]
\arrow["{\J(f') \rtie B'}"', from=3-1, to=3-2]
\arrow["{X'' \ltie b}"', from=3-2, to=3-3]
\arrow["{\J(f') \rtie B}", from=2-1, to=2-2]
\arrow[""{name=1, anchor=center, inner sep=0}, "{X'' \ltie b}"{description}, from=2-2, to=3-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{\J(f'f) \rtie B}", curve={height=-6pt}, from=1-1, to=2-2]
\arrow[""{name=3, anchor=center, inner sep=0}, "{X'' \ltie (b'b)}", curve={height=-6pt}, from=2-2, to=3-3]
\arrow["{\lc{\J f'}_b}"{description}, draw=none, from=0, to=1]
\arrow["\iso"{description}, draw=none, from=2-1, to=2]
\arrow["\iso"{description}, draw=none, from=3-2, to=3]
\end{tikzcd}
\]

We get a left action
$\lact : \V \times \B \to \V$
as follows.
On objects, we set
$X \lact B := X \tens B$.
The action on 1-cells is
$f \lact b :=
\big(
\xra{\J(f) \rtie B}
\xra{X' \ltie b}
\big)$
with the evident action on 2-cells. The unitor is constructed from the unitors for the premonoidal structure,
but the compositor relies on centrality. We define $\phi_{x, b}$ as on the right, where we write just $\iso$ for the compositors.

Next note that
$X \lact b = (X \ltie b) \circ (\J\Id_X \rtie B)$
so the unitor also gives a canonical structural isomorphism
$(X \lact b) \iso (X \ltie b)$
yielding an icon
$(X \lact -) \To (X \ltie -)$.
So we may define the unitor to be the composite
$\actlambda := (\tensu \lact -) \XRA\iso (\tensu \ltie -) \XRA\lambda \id$.
For the associator, we take the 1-cell components to be as for the premonoidal structure in $\B$, so that
$\actalpha_{X, Y, C} := \alpha_{X,Y,C}$,
and define the 2-cell components using  $\theta, \zeta$, and the associator for the premonoidal structure:

\begin{equation*}
\cellOf{\actalpha}_{f,g,c} :=
\begin{tikzcd}[column sep = 5em, row sep =1.3em]
{(XY)C} && {(X'Y')C} & {(X'Y')C'} \\
& {(X'Y)C} \\
{X(YC)} & {X'(YC)} & {X'(Y'C)} & {X'(Y'C')}
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=2-2, curve={height=-12pt}]
\arrow["{\J(f \tens g) \rtie C }", from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, ""'{yshift=-1mm, xshift=1mm, swap}, from=2-2, to=1-3,curve={height=-12pt}] %
\arrow[""{name=2, anchor=center, inner sep=0}, "\alpha"', from=1-1, to=3-1]
\arrow["{\J(f) \rtie (YC)}"', from=3-1, to=3-2]
\arrow["{(X'Y')\ltie a}", from=1-3, to=1-4]
\arrow["{X' \ltie (\J(g) \rtie C)}"', from=3-2, to=3-3]
\arrow["{X' \rtie (Y' \rtie a)}"', from=3-3, to=3-4]
\arrow[""{name=3, anchor=center, inner sep=0}, "\alpha", from=1-4, to=3-4]
\arrow[""{name=4, anchor=center, inner sep=0}, from=1-3, to=3-3]
\arrow[from=2-2, to=3-2]
\arrow[""{name=5, anchor=center, inner sep=0}, curve={height=12pt}, from=2-2, to=1-3, "(X\J(g))C"{swap, yshift=1mm}] %
\arrow[""{name=6, anchor=center, inner sep=0}, curve={height=12pt}, from=1-1, to=2-2, "{(\J (f)Y)C}"'{}]
\arrow["{\cellOf{\alpha}_{X', Y', c}}"{description, xshift=-2mm}, draw=none, from=4, to=3]
\arrow["{\cellOf{\alpha}_{\J f, Y, C}}"{description, yshift=-2mm}, shift right=5, draw=none, from=2, to=2-2]
\arrow["{\cellOf{\alpha}_{X', \J g, C}}"{description, pos=0.6,yshift=-2mm}, shift right=5, draw=none, from=2-2, to=4]
\arrow["\iso"{description, yshift =-2mm}, draw=none, from=0, to=1]
\arrow["{\theta C }"{description}, draw=none, from=1, to=5]
\arrow["{\zeta C}"{description}, draw=none, from=0, to=6]
\end{tikzcd}
\end{equation*}

The compatibility laws on
hold by the corresponding compatibility laws of a Freyd bicategory.
Turning now to the structural modifications, because the structural transformations agree with those of $\B$ on 1-cells, we take the corresponding modifications for the premonoidal structure.
Showing these are indeed modifications relies on  the condition that
$\lc{\J f}_{\J g} = (\rc{\J g}_{\J f})^{-1}$.
Consider the case of $\acttrianglem$. As 2-cells,
$\acttrianglem_{A,B} = \mathfrak{m}_{A,B}$
but $\acttrianglem$ is required to be a modification in two arguments, while the axioms of a premonoidal bicategory make
a modification in each argument separately: in one argument, using $\rc{\lambda}$, and in the other argument using $\lc{\rho}$.
Unpacking the equations for showing $\acttrianglem$ is a modification at maps
$a : A \to A'$
$x : X \to X'$,
we get an instance of $\lc{\J a}_{\lambda}$ arising from the compositor for $\lact$. To apply the modification law for $\mathfrak{m}$, therefore, we first need to pass through the equality
$\lc{\J a}_{\lambda} = \lc{\J a}_{\J\lambda} = (\rc{\J\lambda}_{\J a})^{-1}$.

The axioms of an action hold immediately from the axioms of a premonoidal bicategory.
The proof for the right action case is analogous, except one sets
a \ract g :=
\big(
AY \xra{a \rtie Y} A'Y \xra{A' \ltie \J g} A'Y'
\big)
and defines the compositor using right centrality.
In summary, therefore, we have the following.

Every Freyd bicategory
$(\V \xra{\J} \B)$
determines a left action
$\lact : \V \times \B \to \B$
and a right action
$\ract : \B \times \V \to \V$.

*From Freyd bicategory to Freyd action.

It remains to show the actions just constructed extend the canonical action of $\V$ on itself, and show they are compatible.

XY        X'Y'
[""name=0, anchor=center, inner sep=0, "(f) Y", curve=height=-12pt, from=2-1, to=1-2]
[""name=1, anchor=center, inner sep=0, "X' (g)", curve=height=-12pt, from=1-2, to=2-3]
[""name=2, anchor=center, inner sep=0, "(f g)"', from=2-1, to=2-3]
[""name=3, anchor=center, inner sep=0, curve=height=12pt, from=2-1, to=1-2]
[""name=4, anchor=center, inner sep=0, curve=height=12pt, from=1-2, to=2-3]
["ζ"description, draw=none, from=0, to=3]
["θ"description, draw=none, from=1, to=4]
[""description, draw=none, from=1-2, to=2]

First we define icons $\theta'$ and $\zeta'$ by noting that
f \lact \J(g)
(X' \ltie \J(g)) \circ (\J(f) \rtie Y)
\J(f) \ract g
so that we can set $\theta'_{f,g}$ and $\zeta'_{f,g}$ both to be the composite diagram on the right.
In particular, $\theta'_{f, Y}$ and $\zeta'_{X, g}$ are just $\theta_f$ and $\zeta_g$, respectively, composed with structural isomorphisms.

Now we define $\kappa$. On 1-cells we take just $\alpha$, but on 2-cells we take a definition similar to the proof of naturality in the 1-dimensional case:
$f : X \to X'$
$h : Z \to Z'$
in $\V$ and
$b : B \to B'$
in $\B$ we take:

\begin{equation*}
\cellOf{\kappa}_{f,b,h} :=
\begin{tikzcd}[column sep = 4em, row sep = 1em]
{(XB)Z} && {(X'B')Z} & {(X'B')Z'} \\
& {(X'B)A} \\
{X(BZ)} & {X'(BZ)} & {X'(B'Z)} & {X'(B'Z')}
\arrow[
rounded corners,
to path=
{ -- ([yshift=.6cm]\tikztostart.north)
-| ([yshift=.6cm]\tikztotarget.south)
-- ([yshift=.7cm]\tikztotarget.south)
from=1-1, to=1-4
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.4cm]\tikztostart.south)
-| ([yshift=-.4cm]\tikztotarget.south)
-- ([yshift=0cm]\tikztotarget.south)
from=3-2, to=3-4
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.9cm]\tikztostart.south)
-| ([yshift=-.9cm]\tikztotarget.south)
-- ([yshift=0cm]\tikztotarget.south)
from=3-1, to=3-4
\arrow[from=3-2, to=3-4, "{X' \ltie (b \ract h)}", yshift=-1.2cm, draw=none]
\arrow[from=3-2, to=3-4, "{\iso}", yshift=-.6cm, draw=none]
\arrow[from=3-1, to=3-4, "{f \lact (b \ract h)}", yshift=-1.7cm, draw=none]
\arrow[from=1-1, to=1-4, "{(f \lact b) \ract h}", yshift=1cm, draw=none]
\arrow[""{name=0, anchor=center, inner sep=0}, "{(\J (f)B)Z}"{description, xshift=-2mm}, from=1-1, to=2-2]
\arrow["{(f \lact b) \rtie Z }", from=1-1, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{(X \ltie b)Z}"{description, xshift=2mm}, from=2-2, to=1-3]
\arrow[""{name=2, anchor=center, inner sep=0}, "\alpha"', from=1-1, to=3-1]
\arrow["{\J(f) \rtie (BZ)}"', from=3-1, to=3-2]
\arrow["{(X'B')\ltie \J h}", from=1-3, to=1-4]
\arrow["{X' \ltie (b \rtie Z)}"', from=3-2, to=3-3]
\arrow["{X' \rtie (B' \rtie \J h)}"', from=3-3, to=3-4]
\arrow[""{name=3, anchor=center, inner sep=0}, "\alpha", from=1-4, to=3-4]
\arrow[""{name=4, anchor=center, inner sep=0}, from=1-3, to=3-3]
\arrow[from=2-2, to=3-2]
\arrow["{\cellOf{\alpha}_{X', B', \J h}}"{description}, draw=none, from=4, to=3]
\arrow["\iso"{description}, draw=none, from=0, to=1]
\arrow["{\cellOf{\alpha}_{\J f, B, Z}}"{description}, yshift=-3mm, draw=none, from=2, to=2-2]
\arrow["{\cellOf{\alpha}_{X', b, Z}}"{description}, yshift=-3mm, draw=none, from=2-2, to=4]
\end{tikzcd}
\end{equation*}

The rest of the equations to check for the Freyd action are proven by applying the various compatibility laws to massage the statement into the corresponding axiom given by the definition of a Freyd bicategory.
This completes the proof of the following.

Every Freyd bicategory
$(\V \xra{\J} \B)$
determines a Freyd action with the same underlying pseudofunctor.

§.§ The correspondence theorem

We define functors
$F :\FreydAct{\V, \J, \B}
\leftrightarrows
\FreydBicat{\V, \J, \B} : G$
given on objects by the constructions in
So suppose
$(\lefttrans, \righttrans)$
is a map in $\FreydAct{\V, \J, \B}$. Then
$F(\lefttrans, \righttrans) := (F\lefttrans, F\righttrans)$
is defined by taking

\begin{align*}
\big(
(A \ltie f)
= (\Id_A \lact f)
\XRA{\lefttrans_{\Id_A, f}} (\Id_A \lact' f)
= (A \ltie' f)
\big) \\
\big(
(f \rtie A)
= (f \ract \Id_A)
\XRA{\righttrans_{f, \Id_A}} (f \ract' \Id_A)
= (f \rtie A)
\big)
\end{align*}

Conversely, given a map
$(\lefttrans, \righttrans)$
in $\FreydBicat{\V, \J, \B}$ we define
$G(\lefttrans, \righttrans) := (G\lefttrans, G\righttrans)$
to be

\begin{equation*}
(G\lefttrans)_{f, b} :=
\begin{tikzcd}[column sep = 4em]
XB & {X'B} & {X'B'}
\arrow[""{name=0, anchor=center, inner sep=0}, curve={height=-12pt}, from=1-1, to=1-2,
"{\J f \rtie B}"]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=12pt}, from=1-1, to=1-2,
"{\J f \rtie' B}"{swap}]
\arrow[""{name=2, anchor=center, inner sep=0}, curve={height=-12pt}, from=1-2, to=1-3,
"X' \ltie b"]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=12pt}, from=1-2, to=1-3,
"X' \ltie' b"{swap}]
\arrow[shorten <=2pt, shorten >=2pt, Rightarrow, from=2, to=3,
\arrow[shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=1,
"\:\:\righttrans^{B}_{\J f}"]
\arrow[
rounded corners,
to path=
{ -- ([yshift=.8cm]\tikztostart.north)
-| ([yshift=.8cm]\tikztotarget.south)
-- ([yshift=.6cm]\tikztotarget.south)
from=1-1, to=1-3
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.8cm]\tikztostart.south)
-| ([yshift=-.8cm]\tikztotarget.north)
-- ([yshift=-.6cm]\tikztotarget.north)
from=1-1, to=1-3
\arrow["", draw = none, from=1-1, to=1-3, "f \lact b", yshift = 1.1cm]
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = .5cm]
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = -.9cm]
\arrow["", draw = none, from=1-1, to=1-3, "f \lact' b", yshift = -1.6cm]
\end{tikzcd}
\quad , \quad
(G\righttrans)_{a, g} :=
\begin{tikzcd}[column sep = 4em]
AX & {A'X} & {A'X'}
\arrow[""{name=0, anchor=center, inner sep=0}, curve={height=-12pt}, from=1-1, to=1-2,
"{a \rtie X}"]
\arrow[""{name=1, anchor=center, inner sep=0}, curve={height=12pt}, from=1-1, to=1-2,
"{a \rtie' X}"{swap}]
\arrow[""{name=2, anchor=center, inner sep=0}, curve={height=-12pt}, from=1-2, to=1-3,
"A' \ltie \J g"]
\arrow[""{name=3, anchor=center, inner sep=0}, curve={height=12pt}, from=1-2, to=1-3,
"A' \ltie' \J g"{swap}]
\arrow[shorten <=2pt, shorten >=2pt, Rightarrow, from=2, to=3,
"\:\:\lefttrans^{A'}_{\J g}"]
\arrow[shorten <=2pt, shorten >=2pt, Rightarrow, from=0, to=1,
\arrow[
rounded corners,
to path=
{ -- ([yshift=.8cm]\tikztostart.north)
-| ([yshift=.8cm]\tikztotarget.south)
-- ([yshift=.6cm]\tikztotarget.south)
from=1-1, to=1-3
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.8cm]\tikztostart.south)
-| ([yshift=-.8cm]\tikztotarget.north)
-- ([yshift=-.6cm]\tikztotarget.north)
from=1-1, to=1-3
\arrow["", draw = none, from=1-1, to=1-3, "a \ract g", yshift = 1.1cm]
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = .5cm]
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = -.9cm]
\arrow["", draw = none, from=1-1, to=1-3, "a \ract' g", yshift = -1.6cm]
\end{tikzcd}
\end{equation*}

One shows both $F$ and $G$ are well-defined by a long calculation using the compatibility properties on one side to show the required compatibility condition on the other side.

We now show that $GF \iso \id$ and $FG \iso \id$. Given an action
$\mathcal{A} := (\lact, \theta, \ract, \zeta, \kappa)$,
the composite $GF(\mathcal{A})$ has left action $\lact'$ given by
f \lact' b
(\Id_{X'} \lact b) \circ (\J f \ract \Id_B)
and right action
given by
a \ract' g
(\Id_{A'} \lact \J g) \circ (a \ract \Id_Y)
so we get an obvious choice of icons
$\lact' \To \lact$
$\ract' \To \ract$
given by

\[
\begin{tikzcd}[column sep = 3em, row sep=2.5em]
XB & {X'B} & {X'B'}
\arrow[""{name=0, anchor=center, inner sep=0}, from=1-1, to=1-2]
\arrow["{\Id_{X'} \lact b}", from=1-2, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\J f \ract \Id_B}", curve={height=-16pt}, from=1-1, to=1-2]
\arrow[""{name=2, anchor=center, inner sep=0}, "{f \lact \Id_B}"', curve={height=16pt}, from=1-1, to=1-2]
\arrow["\zeta"{description}, draw=none, from=1, to=0]
\arrow["\theta"{description}, draw=none, from=0, to=2]
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.8cm]\tikztostart.south)
-| ([yshift=-.8cm]\tikztotarget.north)
-- ([yshift=-.6cm]\tikztotarget.north)
from=1-1, to=1-3
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = -.9cm, xshift=4mm]
\arrow["", draw = none, from=1-1, to=1-3, "f \lact b", yshift = -1.6cm]
\end{tikzcd}
\qquad
\qquad
\begin{tikzcd}[column sep = 3em, row sep=2.5em]
AY & {A'Y} & {A'Y'}
\arrow["{a \ract \Id_{Y}}"', from=1-1, to=1-2]
\arrow[""{name=0, anchor=center, inner sep=0}, "{\Id_{A'} \lact \J g}", curve={height=-16pt}, from=1-2, to=1-3]
\arrow[""{name=1, anchor=center, inner sep=0}, "{\Id_{A'} \ract g}"', curve={height=16pt}, from=1-2, to=1-3]
\arrow[""{name=2, anchor=center, inner sep=0}, from=1-2, to=1-3]
\arrow["\theta"{description}, draw=none, from=0, to=2]
\arrow["\zeta"{description}, draw=none, from=2, to=1]
\arrow[
rounded corners,
to path=
{ -- ([yshift=-.8cm]\tikztostart.south)
-| ([yshift=-.8cm]\tikztotarget.north)
-- ([yshift=-.6cm]\tikztotarget.north)
from=1-1, to=1-3
\arrow["", draw = none, from=1-1, to=1-3, "\iso", yshift = -.9cm, xshift=-4mm]
\arrow["", draw = none, from=1-1, to=1-3, "a \ract g", yshift = -1.6cm]
\end{tikzcd}
\]

These commute with all the data because $\theta$ and $\zeta$ do, and forms a natural isomorphism
$GF(\mathcal{A}) \iso \mathcal{A}$
because morphisms in $\FreydAct{\V, \J, \B}$ commute with the icons of the actions.

Finally, to show that $FG \iso \id$ consider a Freyd bicategory
$\freydCat := (\ltie, \theta, \rtie, \zeta)$.
${a \rtie' B} := (X' \ltie \J\Id_B) \circ (a \rtie B)$
${A \ltie' b} := (A \ltie b) \circ (\J\Id_A \rtie B)$
so we have evident structural isomorphisms
$(a \rtie' B) \iso (a \rtie B)$
$(A \ltie' b) \iso (A \ltie b)$.
These commute with all the data and define a natural isomorphism
$FG(\freydCat) \iso \freydCat$
by straightforward applications of coherence.