# Bicategories of Automata, Automata in Bicategories

Guido Boccali† Università di Torino, Torino, ItalyTallinn University of
Technology, Tallinn, EstoniaTallinn University of Technology, Tallinn,
EstoniaUniversità di Bologna, Bologna, Italy Andrea Laretto${}^{\oast}$
Tallinn University of Technology, Tallinn, EstoniaTallinn University of
Technology, Tallinn, EstoniaUniversità di Bologna, Bologna, Italy Fosco
Loregian♣ Loregian was supported by the ESF funded Estonian IT Academy
research measure (project 2014-2020.4.05.19-0001).Tallinn University of
Technology, Tallinn, EstoniaUniversità di Bologna, Bologna, Italy Stefano
Luneia♡ Università di Bologna, Bologna, Italy

###### Abstract

We study _bicategories of_ (deterministic) _automata_ , drawing from prior
work of Katis-Sabadini-Walters, and Di Lavore-Gianola-Román-Sabadini-
Sobociński, and linking their bicategories of ‘processes’ to a bicategory of
Mealy machines constructed in 1974 by R. Guitart. We make clear the sense in
which Guitart’s bicategory retains information about automata, proving that
Mealy machines _à la_ Guitart identify to _certain_ Mealy machines _à la_
K-S-W that we call _fugal automata_ ; there is a biadjunction between fugal
automata and the bicategory of K-S-W. Then, we take seriously the motto that a
monoidal category is just a one-object bicategory. We define categories of
Mealy and Moore machines _inside_ a bicategory $\mymathbb{B}$; we specialise
this to various choices of $\mymathbb{B}$, like categories, relations, and
profunctors. Interestingly enough, this approach gives a way to interpret the
universal property of reachability as a Kan extension and leads to a new
notion of 1- and 2-cell between Mealy and Moore automata, that we call
_intertwiners_ , related to the universal property of K-S-W bicategory.

##  1 Introduction

The profound connection between category theory and automata theory is easily
explained: one of the founders of the first wrote extensively about the second
[23, 24]. A more intrinsic reason is that category theory is a theory of
_systems_ and _processes_. Morphisms in a category can be considered a
powerful abstraction of ‘sequential operations’ performed on a domain/input to
obtain a codomain/output. Hence the introduction of categorical models for
computational machines has been rich in results, starting from the elegant
attempts by Arbib and Manes [2, 7, 5, 6, 8, 59] –cf. also [3, 20, 22] for
exhaustive monographs– and Goguen [28, 29, 30], up to the ultra-formal –and
sadly, under-appreciated– experimentations of [9, 10, 32, 33, 35] using
hyperdoctrines, 2-dimensional monads, bicategories, lax co/limits… up to the
modern coalgebraic perspective of [38, 62, 63, 67]; all this, without
mentioning categorical approaches to Petri nets [54], based essentially on the
same analogy, where the computation of a machine is _concurrent_ –as opposed
to single-threaded.

Furthermore, many constructions of computational significance often, if not
always, have a mathematical counterpart in terms of categorical notions: the
transition from a deterministic machine to a non-deterministic one is
reflected in the passage from automata in a monoidal category (cf. [22, 55]),
to automata in the Kleisli category of an opmonoidal monad (cf. [34, 40]; this
approach is particularly useful to capture categorically _stochastic_
automata, [19, 7, 15] as they appear as automata in the Kleisli category of a
probability distribution monad); _minimisation_ can be understood in terms of
factorisation systems (cf. [18, 30]); behaviour as an adjunction (cf. [56,
57]).

The present work starts from the intuition, first presented in [45, 60], that
the analogy between morphisms and sequential machines holds up to the point
that the series and parallel composition of automata should itself be
reflected in the ‘series’ and ‘parallel’ composition of morphisms in a
category. As a byproduct of the ‘Circ’ construction in _op. cit._ , one can
see how the 1-cells of a certain monoidal bicategory specialise exactly a
_Mealy machines_ $E\xleftarrow{d}E\otimes I\xrightarrow{s}O$ with inputs and
outputs $I$ and $O$.

#### Outline of the paper.

The first result we present in section 2 is that this category relates to
_another_ bicategory constructed by R. Guitart in [32]. Guitart observes that
one can use certain categories $\mathsf{Mac}(\mathcal{M},\mathcal{N})$ of
spans as hom categories of a bicategory $\mathsf{Mac}$, and shows that
$\mathsf{Mac}$ admits a concise description as the Kleisli bicategory of the
_monad of diagrams_ [32, §1] (cf. also [35], by the same author, and [58] for
a more modern survey); Mealy machines shall be recognisable as the 1-cells of
$\mathsf{Mac}$ between monoids, regarded as categories with a single object.
The fundamental assumption in [32] is that a Mealy machine
$E\xleftarrow{d}E\otimes M\xrightarrow{s}N$ satisfies a certain property of
compatibility with the action of $d$ on $E$, cf. (2.8), that we call being a
_fugal_ automaton:

$s(e,m\cdot m^{\prime})=s(e,m)\cdot s(d(e,m),m^{\prime}).$

This notion can be motivated in the following way: if $s$ satisfies the above
equation, then it lifts to a functor $\mathcal{E}[d]\to N$ defined on the
category of elements of the action $d$, and in fact, defines a ‘relational
action’ in its own right, compatible with $d$ (formally speaking,
$\mathcal{E}[d]$ is a _displayed category_ [4] over $N$). We show that there
is a sub-bicategory $\mathsf{Mly}^{\flat}_{\mathsf{Set}}$ of
$\mathsf{Mly}_{\mathsf{Set}}$ made of fugal automata and that
$\mathsf{Mly}^{\flat}_{\mathsf{Set}}$ is biequivalent (actually, strictly) to
the 1-full and 2-full sub-bicategory of $\mathsf{Mac}$ spanned by monoids.

The second result we propose in this paper is motivated by the motto for which
a monoidal category is just a bicategory with a single object: what are
automata _inside a bicategory $\mymathbb{B}$ with more than one object_, where
instead of input/output _objects_ $I,O$ we have input/output 1-cells, arranged
as $e\overset{\delta}{\Leftarrow}e\circ i\overset{\sigma}{\Rightarrow}o$? Far
from being merely formal speculation (a similar idea was studied in a short,
cryptic note [10] to describe behaviour through Kan extensions: we take it
seriously and present it as a quite straightforward observation in Remark
3.6), we show how this allows for a concise generalisation of ‘monoidal’
machines.

#### Related work.

A word on related work and how we fit into it: the ideas in section 2 borrow
heavily from [45, 60] where bicategories of automata (or ‘processes’) are
studied in fine detail; in section 2 we carry on a comparison with a different
approach to bicategories of automata, present in [32] but also in [33, 35]; in
particular, our proof that there is an adjunction between the two bicategories
is novel –to the best of our knowledge– and it hints at the fact that the two
approaches are far from being independent. At the level of an informal remark,
the idea of approaching automata via (spans where one leg is a) fibrations
bears some resemblance to Walters’ work on context-free languages through
displayed categories in [69], and the requirement to have a fibration as one
leg of the span should be thought as mirroring _determinism_ of the involved
automata: if $\langle s,d\rangle:E\times M\to N\times E$ is fugal and $s$
defines a _fibration_ over $N$, then $E$ is a $M$-$N$-bimodule, not only an
$M$-set; there is extensive work of Betti-Kasangian [12, 11, 42] and
Kasangian-Rosebrugh [43] on ‘profunctorial’ models for automata, their
behaviour, and the universal property enjoyed by their minimisation: spans of
two-sided fibrations [64, 65] and profunctors are well-known to be equivalent
ways to present the same bicategory of two-sided fibrations. Carrying on our
study will surely determine a connection between the two approaches.

For what concerns section 3, the idea of valuing a Mealy or a Moore machine in
a bicategory seems to be novel, although in light of [60] and in particular of
their concrete description of $\mathcal{C}=\Omega\Sigma(\mathcal{K},\otimes)$
it seems that both $\mathsf{Mly}{B}$ and $\mathsf{Mre}{B}$ allow defining
tautological functors into $\mathcal{C}$. How these two bicategories relate is
a problem we leave for future investigation: [60] proves that when
$\mathcal{K}$ is Cartesian monoidal, $\mathsf{Mly}_{\mathcal{K}}$ is
$\Omega\Sigma(\mathcal{K},\times)$. The conjecture is that our
$\mathsf{Mly}{B}$ is $\Omega\mymathbb{B}$ under some assumptions on the
bicategory $\mymathbb{B}$: our notion of intertwiner seems to hint in that
direction. Characterising ‘behaviour as a Kan extension’ is nothing but taking
seriously the claim that animates applications of coalgebra theory [39, 40] to
automata; the –apparently almost unknown– work of Bainbridge [10] bears some
resemblance to our idea, but his note is merely sketched, no plausibility for
his intuition is given. Nevertheless, we recognise the potential of his idea
and took it to its natural continuation with modern tools of 2-dimensional
algebra.

###  1.1 Mealy and Moore automata

The scope of the following subsection is to introduce the main characters
studied in the paper:111An almost identical introductory short section appears
in [13], of which the present note is a parallel submission –although related,
the two manuscripts are essentially independent, and the purpose of this
repetition is the desire for self-containment. categories of automata valued
in a monoidal category $(\mathcal{K},\otimes)$ (in two flavours: ‘Mealy’
machines, where one considers spans $E\leftarrow E\otimes I\to O$, and
‘Moore’, where instead one consider pairs $E\leftarrow E\otimes I,E\to O$.

The only purpose of this short section is to fix the notation for section 2
and 3; comprehensive classical references for this material are [3, 22].

For the entire subsection, we fix a monoidal category
$(\mathcal{K},\otimes,1)$.

######  Definition 1.1 (Mealy machine).

A _Mealy machine_ in $\mathcal{K}$ of input object $I$ and output object $O$
consists of a triple $(E,d,s)$ where $E$ is an object of $\mathcal{K}$ and
$d,s$ are morphisms in a span
$\mathfrak{e}:=\left(\vbox{\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.97916pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{E}$}}}}}}}{\hbox{\kern 30.97916pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E\otimes
I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.15746pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.97916pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
69.69952pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{s}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 86.34015pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
86.34015pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{O}$}}}}}}}\ignorespaces}}}}\ignorespaces}\right)$.

######  Remark 1.2 (The category of Mealy machines).

Mealy machines of fixed input and output $I,O$ form a category, if we define a
_morphism of Mealy machines_
$f:\mathfrak{e}=(E,d,s)\to(F,d^{\prime},s^{\prime})=\mathfrak{f}$ as a
morphism $f:E\to F$ in $\mathcal{K}$ such that

  * •

$d^{\prime}\circ(f\otimes I)=f\circ d$;

  * •

$s^{\prime}\circ(f\otimes I)=s$.

Composition and identities are performed in $\mathcal{K}$.

The category of Mealy machines of input and output $I,O$ is denoted as
$\mathsf{Mly}_{\mathcal{K}}(I,O)$.

######  Definition 1.3 (Moore machine).

A _Moore machine_ in $\mathcal{K}$ of input object $I$ and output object $O$
is a diagram $\mathfrak{m}:=\left(\vbox{\lx@xy@svg{\hbox{\raise
0.0pt\hbox{\kern
6.97916pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{E}$}}}}}}}{\hbox{\kern 30.97916pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E\otimes
I\>\>;\>\>E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
14.15746pt\raise 5.43056pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.43056pt\hbox{$\scriptstyle{d}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 6.97916pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
90.9909pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{s}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 107.63153pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
107.63153pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{O}$}}}}}}}\ignorespaces}}}}\ignorespaces}\right)$.

######  Remark 1.4 (The category of Moore machines).

Moore machines of fixed input and output $I,O$ form a category, if we define a
_morphism of Moore machines_
$f:\mathfrak{e}=(E,d,s)\to(F,d^{\prime},s^{\prime})=\mathfrak{f}$ as a
morphism $f:E\to F$ in $\mathcal{K}$ such that

  * •

$d^{\prime}\circ(f\otimes I)=f\circ d$;

  * •

$s^{\prime}\circ f=s$.

######  Remark 1.5 (Canonical extension of a machine).

If $(\mathcal{K},\otimes)$ has countable coproducts preserved by each
$A\otimes\,\rule{5.0pt}{0.4pt}\,$ then the span Definition 1.1, considering
for example Mealy machines, can be ‘extended’ to a span

$\textstyle{E}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E\otimes
I^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d^{*}}$$\scriptstyle{s^{*}}$$\textstyle{O}$
(1.1)

where $d^{*},s^{*}$ can be defined inductively from components
$d_{n},s_{n}:E\otimes I^{\otimes n}\to E,O$; if $\mathcal{K}$ is closed, the
map $d^{*}$ corresponds, under the monoidal closed adjunction, to the monoid
homomorphism $I^{*}\to[E,E]$ induced by the universal property of
$I^{*}=\sum_{n\geq 0}I^{\otimes n}$.

##  2 Bicategories of automata

Let $(\mathcal{K},\times)$ be a Cartesian category. There is a bicategory
$\mathsf{Mly}_{\mathcal{K}}$ defined as follows (cf. [60] where this is called
‘$\mathsf{Circ}$’ and studied more generally, in case the base category has a
non-Cartesian monoidal structure):

######  Definition 2.1 (The bicategory $\mathsf{Mly}_{\mathcal{K}}$, [60]).

The bicategory $\mathsf{Mly}_{\mathcal{K}}$ has

  * •

its _0-cells_ $I,O,U,\dots$ are the same objects of $\mathcal{K}$;

  * •

its _1-cells_ $I\to O$ are the Mealy machines $(E,d,s)$, i.e. the objects of
the category $\mathsf{Mly}_{\mathcal{K}}(I,O)$ in Remark 1.2, thought as
morphisms $\langle s,d\rangle:E\times I\to O\times E$ in $\mathcal{K}$;

  * •

its _2-cells_ are Mealy machine morphisms as in Remark 1.2;

  * •

the composition of 1-cells
$\,\rule{5.0pt}{0.4pt}\,\mathbin{\diamondsuit}\,\rule{5.0pt}{0.4pt}\,$ is
defined as follows: given 1-cells $\langle s,d\rangle:E\times I\to J\times E$
and $\langle s^{\prime},d^{\prime}\rangle:F\times J\to K\times F$ their
composition is the 1-cell $\langle
s^{\prime}\mathbin{\diamondsuit}s,d^{\prime}\mathbin{\diamondsuit}d\rangle:(F\times
E)\times I\to K\times(F\times E)$, obtained as

$\textstyle{F\times E\times
I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{F\times\langle
s,d\rangle}$$\textstyle{F\times J\times
E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
s^{\prime},d^{\prime}\rangle\times E}$$\textstyle{K\times F\times E;}$ (2.1)

  * •

the _vertical_ composition of 2-cells is the composition of Mealy machine
morphisms $f:E\to F$ as in Remark 1.2;

  * •

the _horizontal_ composition of 2-cells is the operation defined thanks to
bifunctoriality of
$\,\rule{5.0pt}{0.4pt}\,\mathbin{\diamondsuit}\,\rule{5.0pt}{0.4pt}\,:\mathsf{Mly}_{\mathcal{K}}(B,C)\times\mathsf{Mly}_{\mathcal{K}}(A,B)\to\mathsf{Mly}_{\mathcal{K}}(A,C)$;

  * •

the associator and the unitors are inherited from the monoidal structure of
$\mathcal{K}$.

######  Remark 2.2.

Spelled out explicitly, the composition of 1-cells in Equation 2.1 corresponds
to the following morphisms (where we freely employ $\lambda$-notation
available in any Cartesian closed category):

$d_{2}\mathbin{\diamondsuit}d_{1}:\lambda efa.\langle
d_{2}(f,s_{1}(e,a)),d_{1}(e,a)\rangle\qquad\qquad
s_{2}\mathbin{\diamondsuit}s_{1}:\lambda efa.s_{2}(f,s_{1}(e,a))$ (2.2)

######  Remark 2.3 (Kleisli extension of automata as base changes).

If $P:\mathcal{K}\to\mathcal{K}$ is a commutative monad [48, 49], we can lift
the monoidal structure $(\mathcal{K},\otimes)$ to a monoidal structure
$(\mathsf{Kl}(P),\bar{\otimes})$ on the Kleisli category of $P$; this leads to
the notion of _$P$ -non-deterministic automata_ or _$P_{\lambda}$ -machines_
studied in [34, §2, Définition 6]. Nondeterminism through the passage to a
Kleisli category is a potent idea that developed into the line of research on
automata theory through coalgebra theory [40], cf. in particular Chapter 2.3
for a comprehensive reference, or the self-contained [38].

We do not investigate the theory of $P_{\lambda}$-machines apart from the
following two results the proof of which is completely straightforward: we
content ourselves with observing that the results expounded in [44, 60], and
in general the language of bicategories of processes, naturally lends itself
to the generation of _base-change functors_ , of which the following two are
particular examples.

######  Proposition 2.4.

The correspondence defined at the level of objects by sending
$(E,d,s)\in\mathsf{Mly}_{\mathcal{K}}(I,O)$ to

$\textstyle{PE}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E}$$\scriptstyle{\eta_{E}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
E\otimes
I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d}$$\scriptstyle{s}$$\textstyle{O\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{O}}$$\textstyle{PO}$
(2.3)

extends to a functor
$L:\mathsf{Mly}_{\mathcal{K}}(I,O)\to\mathsf{Mly}_{\mathsf{Kl}(P)}(I,O)$.

######  Proposition 2.5.

The correspondence sending $(E,d,s)\in\mathsf{Mly}_{\mathsf{Kl}(P)}(I,O)$ into

$\textstyle{PE}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
PPE}$$\scriptstyle{\mu_{E}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
PE\otimes
PI\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Pd\circ
D}$$\scriptstyle{Ps\circ
D}$$\textstyle{PPO\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mu_{O}}$$\textstyle{PO}$
(2.4)

extends to a functor
$(-)^{\text{e}}:\mathsf{Mly}_{\mathsf{Kl}(P)}(I,O)\to\mathsf{Mly}_{\mathcal{K}}(PI,PO)$.

More precisely, the proof of the following result is straightforward –only
slightly convoluted in terms of notational burden– so much so that we feel
content to enclose it in a remark.

######  Remark 2.6.

Let $\mathcal{H},\mathcal{K}$ be cartesian monoidal categories, then we can
define 2-categories $\mathsf{Mly}_{\mathcal{H}},\mathsf{Mly}_{\mathcal{K}}$ as
in Definition 2.1; let $F:\mathcal{H}\to\mathcal{K}$ be a lax monoidal
functor. Then, there exists a ‘base change’ pseudofunctor
$F_{*}:\mathsf{Mly}_{\mathcal{H}}\to\mathsf{Mly}_{\mathcal{K}}$, which is the
1-cell part of a 2-functor $\mathsf{Cat}_{\times}\to\mathsf{Bicat}$ defined on
objects as $\mathcal{K}\mapsto\mathsf{Mly}_{\mathcal{K}}$, from (Cartesian
monoidal categories, product-preserving functors, Cartesian natural
transformations), to (bicategories, pseudofunctors, oplax natural
transformations).

As a corollary, we re-obtain the functors of Proposition 2.5 and Proposition
2.4 from the free and forgetful functors $F_{P}:\mathcal{K}\to\mathsf{Kl}(P)$
and $U_{P}:\mathsf{Kl}(P)\to\mathcal{K}$.

###  2.1 Fugal automata, Guitart machines

A conceptual construction for $\mathsf{Mly}_{\mathcal{K}}$ in Definition 2.1
is given as follows in [44]: it is the category
$\Omega\Sigma(\mathcal{K},\otimes)$ of pseudofunctors
$\mymathbb{N}\to\Sigma(\mathcal{K},\times)$ and lax transformations, where
$\Sigma$ is the ‘suspension’ of $(\mathcal{K},\otimes)$, i.e. $\mathcal{K}$
regarded as a one-object bicategory; a universal property for
$\mathsf{Mly}_{\mathcal{K}}$ is provided in [45] (actually, for any
$\Omega\Sigma(\mathcal{K},\otimes)$): it is the free _category with feedbacks_
(op. cit., Proposition 2.6, see also [51]) on $\mathcal{K}$. The bicategory
$\mathsf{Mly}_{\mathcal{K}}$ addresses the fundamental question of whether one
can fruitfully consider morphisms in a category as an abstraction of
‘sequential operations’ performed on a domain/input to obtain a
codomain/output, and up to what point the analogy between morphisms and
sequential machines holds up (composing 1-cells in
$\mathsf{Mly}_{\mathcal{K}}$ accounts for the sequential composition of state
machines, where the state $E$ is an intrinsic part of the specification of a
machine/1-cell $\langle s,d\rangle$).

Twenty eight years before [45], however, René Guitart [32] exhibited another
bicategory $\mathsf{Mac}$ of ‘Mealy machines’, defined as a suitable category
of spans, of which one leg is a fibration, and its universal property:
$\mathsf{Mac}$ is the Kleisli bicategory of the diagram monad (_monade des
diagrammes_ in [32, §1], cf. [47, 58])
$\mathsf{Cat}/\\!\\!/\,\rule{5.0pt}{0.4pt}\,$.222Guitart’s note [32] is rather
obscure with respect of the fine details of his definition, as he chooses for
2-cells the $H$ for which the upper triangle in (2.6) is only _laxly_
commutative, and when it comes to composition of 1-cells he invokes a _produit
fibré canonique_ ; apparently, this can’t be interpreted as a strict pullback,
or there would be no way to define horizontal composition of 2-cells; using a
comma object instead of a strict pullback, the lax structure is given by the
universal property –observe that the functor that must be an opfibration is
indeed an opfibration, thanks to [37, Exercise 1.4.6], but this opfibration
does not remember much of the opfibration $q$ one pulled back. Our theorem
involves a strict version of Guitart’s $\mathsf{Mac}$, because the functor
$\Pi$ of Theorem 2.17 factors through
$\mathsf{Mac}^{\mathrm{s}}\subseteq\mathsf{Mac}$.

######  Definition 2.7 (The bicategory $\mathsf{Mac}^{\mathrm{s}}$, adapting
[32]).

Define a bicategory $\mathsf{Mac}^{\mathrm{s}}$ as follows:

  * •

0-cells are categories $\mathcal{A},\mathcal{B},\mathcal{C}$…;

  * •

1-cells $(\mathcal{E};p,S):\mathcal{A}\to\mathcal{B}$ consist of spans

$\textstyle{\mathcal{A}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{S}$$\textstyle{\mathcal{B}}$
(2.5)

where $p:\mathcal{E}\to\mathcal{A}$ is a discrete opfibration;

  * •

2-cells $H:(\mathcal{E};p,S)\Rightarrow(\mathcal{F};q,T)$ are pairs where
$H:\mathcal{E}\to\mathcal{F}$ is a morphism of opfibrations (cf. [37, dual of
1.7.3.(i)]): depicted graphically, a 2-cell is a diagram

$\textstyle{\mathcal{E}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H}$$\scriptstyle{S}$$\scriptstyle{p}$$\textstyle{\mathcal{B}}$$\textstyle{\mathcal{A}}$$\textstyle{\mathcal{F}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\scriptstyle{T}$
(2.6)

where both triangles commute and $H$ is an opCartesian functor (it preserves
opCartesian morphisms);

  * •

composition of 1-cells
$\mathcal{A}\xleftarrow{p}\mathcal{E}\xrightarrow{S}\mathcal{B}$ and
$\mathcal{B}\xleftarrow{q}\mathcal{F}\xrightarrow{T}\mathcal{C}$ is via
pullbacks, as it happens in spans, and all the rest of the structure is
defined as in spans.

Given this, a natural question that might arise is how do the two bicategories
of Definition 2.1 and Definition 2.7 interact, if at all?

In the present section, we aim to prove the existence of an adjunction (cf.
Theorem 2.18) between a suitable sub-bicategory of $\mathsf{Mac}^{\mathrm{s}}$
and a sub-bicategory of $\mathsf{Mly}_{\mathsf{Set}}$ spanned over what we
call _fugal_ Mealy machines between monoids (cf. Definition 2.11).333A _fugue_
is ‘a musical composition in which one or two themes are repeated or imitated
by successively entering voices and contrapuntally developed in a continuous
interweaving of the voice parts’, cf. [68]. In our case, the interweaving is
between $s,d$ in a Mealy machine.

Since the construction of $\mathsf{Mac}^{\mathrm{s}}$ outlined in [32]
requires some intermediate steps (and it is written in French), we deem it
necessary to delve into the details of how its structure is presented. To fix
ideas, we keep working in the category of sets and functions.

######  Notation 2.8.

In order to avoid notational clutter, we will blur the distinction between a
monoid $M$ and the one-object category it represents; also, given the $d$ part
of a Mealy machine, we will denote as $d^{*}$ both the extension $E\times
I^{*}\to E$ of Remark 1.5, which is a monoid action of $I^{*}$ on $E$, and the
functor $I^{*}\to\mathsf{Set}$ to which the action corresponds.

######  Remark 2.9.

In the notation above, a Mealy machine $\mathfrak{e}=(E,d,s)$ yields a
discrete opfibration (cf. [1, 37]) $\mathcal{E}[d^{*}]\to I^{*}$ over the
monoid $I^{*}$, and $\mathcal{E}[a]$ is the _translation category_ of an
$M$-set $a:M\times X\to X$ (cf. [14] for the case when $M$ is a group:
clearly, $\mathcal{E}[a]$ is the category of elements of the action
$a:M\to\mathsf{Set}$ regarded as a functor), i.e. the category having

  * •

objects the elements of $E$;

  * •

a morphism $m:e\to e^{\prime}$ whenever $e^{\prime}=d^{*}(e,m)$.

Composition and identities are induced by the fact that $d^{*}$ is an action.

######  Remark 2.10.

The hom-categories $\mathsf{Mac}^{\mathrm{s}}(\mathcal{A},\mathcal{B})$ of
Definition 2.7 fit into strict pullbacks

$\textstyle{\mathsf{Mac}^{\mathrm{s}}(\mathcal{A},\mathcal{B})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Cat}/\mathcal{B}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{opFib}/\mathcal{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Cat}}$
(2.7)

where $\mathsf{Cat}/\mathcal{B}$ is the usual slice category of $\mathsf{Cat}$
over $\mathcal{B}$.

######  Definition 2.11 (Fugal automaton).

Let $M,N$ be monoids; a Mealy machine $\langle s,d\rangle:E\times M\to N\times
E$ is _fugal_ if its $s$ part satisfies the equation

$s(e,m\cdot m^{\prime})=s(e,m)\cdot s(d(e,m),m^{\prime}).$ (2.8)

######  Remark 2.12.

This definition appears in [32, §2] and it looks an ad-hoc restriction for
what an output map in a Mealy machine shall be; but (2.8) can be motivated in
two ways:

  * •

A fugal Mealy machine $\langle s,d\rangle:E\times M\to N\times E$ induces in a
natural way a functor $\Sigma:\mathcal{E}[d^{*}]\to N$ because (2.8) is
exactly equivalent to the fact that $\Sigma$ defined on objects in the only
possible way, and on morphisms as $\Sigma(e\to d^{*}(e,m))=s(e,m)$ preserves
(identities and) composition;

  * •

given a generic Mealy machine $\langle s,d\rangle:E\times A\to B\times E$ one
can produce a ‘universal’ fugal Mealy machine $\langle
s,d\rangle^{\flat}=\langle s^{\flat},\,\rule{5.0pt}{0.4pt}\,\rangle:E\times
A^{*}\to B^{*}\times E$, and this construction is well-behaved for 1-cell
composition in $\mathsf{Mly}_{\mathsf{Set}}$, in the sense that
$(s_{2}\mathbin{\diamondsuit}s_{1})^{\flat}=s_{2}^{\flat}\mathbin{\diamondsuit}s_{1}^{\flat}$.

The remainder of this section is devoted to making these claims precise (and
prove them). In particular, the ‘universality’ of $\langle s,d\rangle^{\flat}$
among fugal Mealy machines obtained from $\langle s,d\rangle$ is clarified by
the following Lemma 2.13 and by Theorem 2.18, where we prove that there is a
2-adjunction between $\mathsf{Mly}_{\mathsf{Set}}$ and
$\mathsf{Mly}^{\flat}_{\mathsf{Set}}$.

######  Lemma 2.13.

Given sets $A,B$, denote with $A^{*},B^{*}$ their free monoids; then, there
exists a ‘fugal extension’ functor
$(\,\rule{5.0pt}{0.4pt}\,)_{A,B}^{\flat}:\mathsf{Mly}_{\mathsf{Set}}(A,B)\to\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},B^{*})$.

###### Proof.

The proof is deferred to the appendix, p. A.2. In particular, the map
$s^{\flat}$ is constructed inductively as

$\begin{cases}s^{\flat}(e,[\,])&=[\,]\\\
s^{\flat}(e,a\mathbin{::}as)&=s(e,a)\mathbin{::}s^{\flat}(d(e,a),as)\end{cases}$
(2.9)

and it fits in the Mealy machine $\langle s^{\flat},d^{*}\rangle:E\times
A^{*}\to B^{*}\times E$ where $d^{*}$ is as in (1.1). The proof that $\langle
s^{\flat},d^{*}\rangle$ is fugal in the sense of (2.8) can be done by
induction and poses no particular difficulty. ∎

######  Lemma 2.14.

Given sets $A,B$ there exists a commutative square

$\textstyle{\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},B^{*})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Cat}/B^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{opFib}/A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Cat}.}$
(2.10)

###### Proof of Lemma 2.14.

Given a fugal Mealy machine $\langle s,d\rangle:E\times A^{*}\to B^{*}\times
E$ between free monoids, from the action $d$ we obtain a discrete opfibration
$\mathcal{E}[d]\to A^{*}$, and from the map $s:E\times A^{*}\to B^{*}$ we
obtain a functor $\Sigma:\mathcal{E}[d^{*}]\to B^{*}$ as in Remark 2.12. So,
one can obtain a span

$\textstyle{A^{*}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{E}[d^{*}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{D}$$\scriptstyle{\Sigma}$$\textstyle{B^{*}}$
(2.11)

where the leg $D:\mathcal{E}[d^{*}]\to A^{*}$ is as in Remark 2.9 and $\Sigma$
is an in Remark 2.12. The functors
$\mathsf{opFib}/A^{*}\leftarrow\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},B^{*})\to\mathsf{Cat}/B^{*}$
project to each of the two legs. ∎

######  Corollary 2.15.

The universal property of the hom-categories
$\mathsf{Mac}^{\mathrm{s}}(\mathcal{A},\mathcal{B})$ exposed in Remark 2.10
yields the right-most functor in the composition

$\textstyle{\Gamma_{A,B}:\mathsf{Mly}_{\mathsf{Set}}(A,B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\,\rule{5.0pt}{0.4pt}\,)_{A,B}^{\flat}}$$\textstyle{\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},B^{*})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Pi_{A,B}}$$\textstyle{\mathsf{Mac}^{\mathrm{s}}(A^{*},B^{*})}$
(2.12)

######  Lemma 2.16 (Fugal extension preserves composition).

Let $A,B,C$ be sets, $s_{1}:E\times A\to B$ and $s_{2}:F\times B\to C$ parts
of Mealy machines $\langle s_{1},\,\rule{5.0pt}{0.4pt}\,\rangle$ and $\langle
s_{2},\,\rule{5.0pt}{0.4pt}\,\rangle$; then
$(s_{2}\mathbin{\diamondsuit}s_{1})^{\flat}=s_{2}^{\flat}\mathbin{\diamondsuit}s_{1}^{\flat}$.

###### Proof.

The proof is deferred to the appendix, p. A.2.444The argument is
straightforward but tedious (the difficult part is that the condition to
verify on $(s_{2}\mathbin{\diamondsuit}s_{1})^{\flat}$ involves
$d_{2}\mathbin{\diamondsuit}d_{1}$, the expression of which we recall from
(2.2), is the $\lambda$-term $\lambda efa.\langle
d_{2}(f,s_{1}(e,a)),d_{1}(e,a)\rangle$). ∎

This, together with the fact that the identity 1-cell $1\times A\to A\times 1$
is fugal (the proof is straightforward), yields that there exists a
2-subcategory $\mathsf{Mly}^{\flat}_{\mathsf{Set}}$ of
$\mathsf{Mly}_{\mathsf{Set}}$ where 0-cells are monoids, 1-cells are the
$\langle s,d\rangle$ where $s$ is fugal in the sense of Definition 2.11, and
we take all 2-cells.

######  Theorem 2.17.

The maps $\Gamma_{A,B}$ of Corollary 2.15 constitute the action on 1-cells of
a 2-functor $\Gamma:\mathsf{Mly}_{\mathsf{Set}}\to\mathsf{Mac}^{\mathrm{s}}$.
More precisely, there are 2-functors
$(\,\rule{5.0pt}{0.4pt}\,)^{\flat}:\mathsf{Mly}_{\mathsf{Set}}\to\mathsf{Mly}^{\flat}_{\mathsf{Set}}$
and $\Pi:\mathsf{Mly}^{\flat}_{\mathsf{Set}}\to\mathsf{Mac}^{\mathrm{s}}$
whose composition is $\Gamma$.

###### Proof.

The proof is deferred to the appendix, p. A.2. ∎

######  Theorem 2.18.

The 2-functor
$(\,\rule{5.0pt}{0.4pt}\,)^{\flat}:\mathsf{Mly}_{\mathsf{Set}}\to\mathsf{Mly}^{\flat}_{\mathsf{Set}}$
admits a right 2-adjoint; the 2-functor
$\Pi:\mathsf{Mly}^{\flat}_{\mathsf{Set}}\to\mathsf{Mac}^{\mathrm{s}}$
identifies $\mathsf{Mly}^{\flat}_{\mathsf{Set}}$ as the 1-full and 2-full
subcategory of $\mathsf{Mac}^{\mathrm{s}}$ spanned by monoids.

###### Proof.

The proof is deferred to the appendix, p. A.2. The last statement essentially
follows from (2.11): the span $(D,\Sigma)$ is essentially equivalent to the
fugal Mealy machine $\langle s,d\rangle$, since its left leg $D$ determines a
unique action of $A^{*}$ on the set of objects $\mathcal{E}[d^{*}]_{0}$, and
$\Sigma$ and $s$ are mutually defined. ∎

##  3 Bicategory-valued machines

A monoidal category is just a bicategory with a single 0-cell; then, do
Definition 1.1 and Definition 1.3 admit a generalisation when instead of
$\mathcal{K}$ we consider a bicategory $\mymathbb{B}$ with more than one
object? The present section answers in the positive. We also outline how,
passing to automata valued in a bicategory, a seemingly undiscovered way to
define morphisms between automata, different (from (1.2) and) from the
categories of ‘variable’ automata described in [22, §11.1]: we study this
notion in Definition 3.12.

In our setting, ‘automata’ become diagrams of _2-cells_ in $\mymathbb{B}$,
between input, output and state _1-cells_ , in contrast with previous studies
where automata appeared as objects, and with [60] (and our section 2), where
they appear as diagrams of 1-cells between input, output and state 0-cells.
This perspective suggests that 2-dimensional diagrams of a certain shape can
be thought of as state machines -so, they carry a computational meaning; but
also that state machines can be fruitfully interpreted as diagrams: in Example
3.11 we explore definitions of an automaton where input and output are
_relations_ , or functors (in Example 3.9), or profunctors (in Example 3.10);
universal objects that can be attached to the 2-dimensional diagram then admit
a computational interpretation (cf. (3.9) where a certain Kan extension
resembles a ‘reachability’ relation).

This idea is not entirely new: it resembles an approach contained in [10, 9]
where the author models the state space of abstract machines as a functor, of
which one can take the left/right Kan extension along an ‘input scheme’.
However, Bainbridge’s works are rather obscure (and quite ahead of their
time), so we believe we provide some advancement to state of the art by taking
his idea seriously and carrying to its natural development –while at the same
time, providing concrete examples of bicategories in which inputs/outputs
automata can be thought of as 1-cells, and investigating the structure of the
class of all such automata as a global object.

######  Definition 3.1.

Adapting from Definition 1.1 _verbatim_ , if $\mymathbb{B}$ is a bicategory
with 0-cells $A,B,X,Y,\dots$, 1-cells $i:A\to B,o:X\to Y,\dots$ and 2-cells
$\alpha,\beta,\dots$ the kind of object we want in $\mathsf{Mly}{B}(i,o)$ is a
span of the following form:

$\textstyle{e}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces
e\circ
i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\delta}$$\scriptstyle{\sigma}$$\textstyle{o}$
(3.1)

for 1-cells $i:X\to Y$, $e:A\to B$, $o:C\to D$. Note that with
$\,\rule{5.0pt}{0.4pt}\,\circ\,\rule{5.0pt}{0.4pt}\,$, we denote the
composition of 1-cells in $\mymathbb{B}$, which becomes a monoidal product in
$\mymathbb{B}$ has a single 0-cell.

######  Remark 3.2.

The important observation here is that the mere existence of the span
$(\delta,\sigma)$ ‘forces the types’ of $i,o,e$ in such a way that $i$ _must_
be an endomorphism of an object $A\in\mymathbb{B}$, and $e,o:A\to B$ are
1-cells. Interestingly, these minimal assumptions required even to consider an
object like (3.1) make iterated compositions $i\circ\dots\circ i$ as
meaningful as iterated tensors $I\otimes\dots\otimes I$, and in fact, the two
concepts coincide when $\mymathbb{B}$ has a single object $*$ and hom-category
$\mymathbb{B}(*,*)=\mathcal{K}$.

In the monoidal case, the fact that an input 1-cell stands on a different
level from an output was completely obscured by the fact that _every_ 1-cell
is an endomorphism.

Let us turn this discussion into a precise definition.

######  Definition 3.3 (Bicategory-valued Mealy machines).

Let $\mymathbb{B}$ be a bicategory, and fix two 1-cells $i:A\to A$ and $o:A\to
B$; define a category $\mathsf{Mly}{B}(i,o)$ as follows:

  1. bml1)

the objects are diagrams of 2-cells as in (3.1);

  2. bml2)

the morphisms
$(e,\delta,\sigma)\to(e^{\prime},\delta^{\prime},\sigma^{\prime})$ are 2-cells
$\varphi:e\Rightarrow e^{\prime}$ subject to conditions similar to Remark 1.2:

     * •

$\sigma^{\prime}\circ(\varphi*i)=\sigma$;

     * •

$\delta^{\prime}\circ(\varphi*i)=\varphi\circ\delta$.

######  Definition 3.4 (Bicategory-valued Moore machines).

Define a category $\mathsf{Mre}{B}(i,o)$ as follows:

  1. bmo1)

the objects are pairs of 2-cells in $\mymathbb{B}$, $\delta:e\circ
i\Rightarrow e$ and $\sigma:e\Rightarrow o$;

  2. bmo2)

the morphisms
$(e,\delta,\sigma)\to(e^{\prime},\delta^{\prime},\sigma^{\prime})$ are 2-cells
$\varphi:e\Rightarrow e^{\prime}$ such that diagrams of 2-cells similar to
those in Definition 3.3 are commutative.

######  Notation 3.5.

In the following, an object of $\mathsf{Mly}{B}(i,o)$ (resp.,
$\mathsf{Mre}{B}(i,o)$) will be termed a _bicategorical Mealy machine_ (resp.,
a _bicategorical Moore machine_) of input cell $i$ and output cell $o$, and
the objects $A,B$ are the _base_ of the bicategorical Mealy machine
$(e,\delta,\sigma)$. To denote that a bicategorical Mealy machine is based on
$A,B$ we write $(e,\delta,\sigma)_{A,B}$.

In [10] the author models the state space of abstract machines as follows: fix
categories $A,X,E$ and a functor $\Phi:X\to A$, of which one can take the
left/right Kan extension along an ‘input scheme’ $u:E\to X$; a _machine with
input scheme $u$_ is a diagram of 2-cells in $\mathsf{Cat}(E,A)$ of the form
$\mathcal{M}=(I\Rightarrow\Phi\circ u\Rightarrow J)$, and the _behaviour_
$B(\mathcal{M})$ of $\mathcal{M}$ is the diagram of 2-cells
$\mathrm{Lan}_{u}I\Rightarrow\Phi\Rightarrow\mathrm{Ran}_{u}J$.

All this bears some resemblance to the following remark, but at the same time
looks very mysterious, and not much intuition is given in _op. cit._ for what
the approach in study means; we believe our development starts from a similar
point (the intuition that a category of machines is, in the end, some category
of diagrams –a claim we substantiate in Proposition 3.8) but rapidly takes a
different turn (cf. Definition 3.12), and ultimately gives a cleaner account
of Bainbridge’s perspective (see also [9] of the same author).

######  Remark 3.6 (Behaviour as a Kan extension).

A more convenient depiction of the span in bmo1 will shed light on our
Definition 3.3 and 3.4, giving in passing a conceptual motivation for the
convoluted shape of finite products in $\mathsf{Mre}_{\mathcal{K}}(I,O)$ and
$\mathsf{Mly}_{\mathcal{K}}(I,O)$ (cf. [22, Ch. 11]): a bicategorical Moore
machine in $\mymathbb{B}$ of fixed input and output $i,o$ consists of a way of
filling the dotted arrows in the diagram

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\scriptstyle{e}$$\textstyle{\scriptstyle
o}$$\textstyle{\scriptstyle\sigma}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{\scriptstyle\delta}$$\textstyle{B}$
(3.2)

with $e:A\to B$ and two 2-cells $\delta,\sigma$. But then the ‘terminal way’
of filling such a span can be characterised by the right extension of the
output object along a certain 1-cell obtained from the input $i$. Let us
investigate how.

First of all, we have to assume something on the ambient hom-categories
$\mymathbb{B}(A,A)$, namely that each of these admits a left adjoint to the
forgetful functor

$\textstyle{\mymathbb{B}(A,A)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{Mnd}_{/A}}$
(3.3)

(cf. [21, Ch. II]) so that every endo-1-cell $i:A\to A$ has an associated
extension to an endo-1-cell $i^{\natural}:A\to A$ with a unit map
$i\Rightarrow i^{\natural}$ that is initial among all 2-cells out of $i$ into
a monad in $\mymathbb{B}$; $i^{\natural}$ is usually called the _free monad_
on $i$.

######  Construction 3.7.

Now, fix $i,o$ as in Definition 3.4; we claim that the terminal object of
$\mathsf{Mre}{B}(i,o)$ is obtained as the right extension in $\mymathbb{B}$ of
the output $o$ along $i^{\natural}$. We can obtain

  * •

from the unit $\boldsymbol{\eta}:\operatorname{id}_{A}\Rightarrow
i^{\natural}$ of the free monad on $i$, a canonical modification
$\mathrm{Ran}_{i}\Rightarrow\mathrm{Ran}_{\operatorname{id}}=\operatorname{id}_{A}$,
with components at $o$ given by 2-cells $\sigma:\mathrm{Ran}_{i}o\Rightarrow
o$; this is a choice of the right leg for a diagram like bmo1;

  * •

from the multiplication $\boldsymbol{\mu}:i^{\natural}\circ
i^{\natural}\Rightarrow i^{\natural}$ of the free monad on $i$, a canonical
modification
$\mathrm{Ran}_{i^{\natural}}\Rightarrow\mathrm{Ran}_{i^{\natural}}\circ\mathrm{Ran}_{i^{\natural}}$,
whose components at $o$ mate to a 2-cell
$\delta_{0}:\mathrm{Ran}_{i^{\natural}}o\circ
i^{\natural}\Rightarrow\mathrm{Ran}_{i^{\natural}}o$; the composite

$\textstyle{\delta:\mathrm{Ran}_{i^{\natural}}o\circ
i\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{Ran}_{i^{\natural}}o*\boldsymbol{\eta}}$$\textstyle{\mathrm{Ran}_{i^{\natural}}o\circ
i^{\natural}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathrm{Ran}_{i^{\natural}}o}$
(3.4)

The left leg is now chosen for a diagram like bmo1.

Together, $(\mathrm{Ran}_{i^{\natural}}o,\delta,\sigma)$ is a bicategorical
Mealy machine, and the universal property of the right Kan extension says it
is the terminal such. A similar line of reasoning yields the same result for
$\mathsf{Mly}{B}(i,o)$, only now $\sigma$ is the 2-cell obtained as mate of
$\epsilon\circ(\mathrm{Ran}_{i^{\natural}}o*\boldsymbol{\eta}):\mathrm{Ran}_{i^{\natural}}o\circ
i\Rightarrow\mathrm{Ran}_{i^{\natural}}o\circ i^{\natural}\Rightarrow o$ from
the counit of $\,\rule{5.0pt}{0.4pt}\,\circ
i^{\natural}\dashv\mathrm{Ran}_{i^{\natural}}$.

######  Proposition 3.8 ($\mathsf{Mre}{B}(i,o)$ and $\mathsf{Mly}{B}(i,o)$ as
categories of diagrams.).

There exists a 2-category $\mathcal{P}$ and a pair of strict 2-functors
$W,G:\mathcal{P}\to\mymathbb{B}$ such that bicategorical Moore machines with
‘variable output 1-cell’ i.e. the 2-dimensional diagrams like in (3.2) where
$o$ is variable, can be characterised as natural transformations $W\Rightarrow
G$.

###### Proof.

The proof is deferred to the appendix, p. A.2.

As explained therein, bicategorical Moore machines with fixed output $o$ can
be characterised as particular such natural transformations that take value
$o$ on one argument.

Also, minor adjustments to the shape of $G$ yield a similar result for
bicategorical Mealy machines. ∎

######  Example 3.9 (Bicategorical machines in $\mathsf{Cat}$).

Consider a span
$\mathcal{C}\xleftarrow{I}\mathcal{C}\xrightarrow{O}\mathcal{D}$ in the strict
2-category $\mymathbb{Cat}$ of categories, functors and natural
transformations, where $\mathcal{D}$ is a $\kappa$-complete category. The
category $\mathsf{Mre}_{\mathsf{Cat}}(I,O)$ has objects the triples
$(E,\delta,\sigma)$ where $E:\mathcal{C}\to\mathcal{D}$ is a functor and
$\sigma,\delta$ are natural transformations arranged as in (3.2); assuming
enough limits in $\mathcal{D}$, we can compute the action of the right Kan
extension of $O$ along $I^{\natural}$ (the free monad on the endofunctor $I$,
cf. [46], whose existence requires additional assumptions on $\mathcal{C}$) on
an object $C\in\mathcal{C}$ as the equaliser

$\textstyle{RC\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\prod_{C\in\mathcal{C}}OC^{\mathcal{C}(A,I^{\natural}C)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\prod_{C\to
B}OB^{\mathcal{C}(A,I^{\natural}C)}}$ (3.5)

or (better, cf. [52, 2.3.6]) as the end555Recall that if $S$ is a set and $C$
is an object of a category $\mathcal{C}$ with limits, by $C^{S}$ we denote the
_power_ of $C$ and $S$, i.e. the iterated product $\prod_{s\in S}C$ of as many
copies of $C$ as there are elements in $S$.
$A\mapsto\int_{C}OC^{\mathcal{C}(A,I^{\natural}C)}$, i.e. as the ‘space of
fixpoints’ for the conjoint action of the functor $O$ and of the presheaf
$C\mapsto\mathcal{C}(A,I^{\natural}C)$ on objects of $\mathcal{C}$; the free
monad $I^{\natural}$ sends an object $C$ to the initial algebra of the functor
$A\mapsto C+IA$, so that $I^{\natural}C\cong C+I(I^{\natural}C)$.

For the sake of simplicity, let us specialise the discussion when
$\mathcal{D}$ is the category of sets and functions: the input $I$ and the
output $O$ of the state machine in Definition 1.1 are now variable objects
‘indexed’ over the objects of $\mathcal{C}$, and the behaviour of the terminal
machine can be described as a known object: unpacking the end (3.5) we obtain
the functor

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{[\mathcal{C},\mathsf{Set}](\mathcal{C}(A,I^{\natural}\,\rule{5.0pt}{0.4pt}\,),O)}$
(3.6)

sending an object $A$ to the set of natural transformations
$\alpha:\mathcal{C}(A,I^{\natural}\,\rule{5.0pt}{0.4pt}\,)\Rightarrow O$; the
intuition here is that to each generalised $A$-element of $I^{\natural}C$
corresponds an element of the output space $\Upsilon_{C}(u)\in OC$, and that
this association is natural in $C$.

######  Example 3.10 (Bicategorical machines in profunctors).

We can reason similarly in the bicategory of categories and profunctors of
[41, 16, 17], [52, Ch. 5]; now an endo-1-cell $I:\mathcal{C}\to\mathcal{C}$ on
a category $\mathcal{C}$ consists of an ‘extension’ of the underlying graph of
$U\mathcal{C}$ to a bigger graph $(U\mathcal{C})^{+}$,666More precisely, to
the underlying graph of $\mathcal{C}$, made of ‘old’ arrows, we adjoin a
directed edge $e_{x}:C\to C^{\prime}$ for each $x\in I(C,C^{\prime})$. and the
free promonad $I^{\natural}$ (cf. [50, §5]) corresponds to the quotient of the
free category on $(U\mathcal{C})^{+}$ where ‘old’ arrows compose as in
$\mathcal{C}$, and ‘new’ arrows compose freely; moreover, all right extensions
$\langle P/Q\rangle:\mathcal{X}\rightsquigarrow\mathcal{Y}$ of
$Q:\mathcal{A}\rightsquigarrow\mathcal{Y}$ along
$P:\mathcal{A}\rightsquigarrow\mathcal{X}$ exist in the bicategory
$\mymathbb{Prof}$, as they are computed as the end in [52, 5.2.5],

$\textstyle{\langle
P/Q\rangle:(X,Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\int_{A}\mathsf{Set}(P(Y,A),Q(X,A)).}$
(3.7)

######  Example 3.11 (Bicategorical machines in relations).

When it is instantiated in the (locally thin) bicategory of relations between
sets, i.e. $\\{0,1\\}$-profunctors, given $I:A\rightsquigarrow A$,
$O:A\rightsquigarrow B$, $I^{\natural}$ is the reflexive-transitive closure of
$I$, and the above Kan extension is uniquely determined as the maximal $E$
such that $E\subseteq O$ and $E\circ I^{\natural}\subseteq E$ (here $\circ$ is
the relational composition). So $R=\mathrm{Ran}_{I^{\natural}}O$ is the
relation defined as

$(a,b)\in R\iff\forall a^{\prime}\in A.((a^{\prime},a)\in
I^{\natural}\Rightarrow(a^{\prime},b)\in O).$ (3.8)

This relation expresses _reachability_ of $b$ from $a$: it characterises the
sub-relation of $O$ connecting those pairs $(a,b)$ for which, for every other
$a^{\prime}\in A$, if there is a finite path (possibly of length zero, i.e.
$a=a^{\prime}$) connecting $a^{\prime},a$ through $I$-related elements, then
$(a^{\prime},b)\in O$. In pictures:

$a\,R\,b\iff\Big{(}(a^{\prime}=a)\lor(a^{\prime}\xrightarrow{I}a_{1}\xrightarrow{I}\dots\xrightarrow{I}a_{n}\xrightarrow{I}a)\Rightarrow
a^{\prime}\,O\,b\Big{)}$ (3.9)

When the above example is specialised to the case when $A=*$ is a singleton,
there are only two possible choices for $I$ (both reflexive and transitive),
and $O$ identifies to a subset of $B$; a bicategorical Moore machine is then a
subset $R\subseteq O$, and thus for both choices of $I$,
$\mathsf{Mre}_{\mymathbb{Rel}}(I,O)_{*,B}=2^{O}$. One can reason in the same
fashion for Mealy machines.

###  3.1 Intertwiners between bicategorical machines

In passing from $\mathsf{Mly}_{\mathcal{K}}(I,O)$ to $\mathsf{Mly}{B}(i,o)$ we
gain an additional degree of freedom by being able to index the category over
pairs of 0-cells of $\mymathbb{B}$, and this is particularly true in the sense
that the definition of $\mathsf{Mly}{B}(i,o)$ and its indexing over pairs of
objects $A,B$ of $\mathcal{K}$ leads to a seemingly undiscovered way to define
morphisms between automata:

######  Definition 3.12 (Intertwiner between bicategorical machines).

Consider two bicategorical Mealy machines
$(e,\delta,\sigma)_{A,B},(e^{\prime},\delta^{\prime},\sigma^{\prime})_{A^{\prime},B^{\prime}}$
on different bases (so in particular
$(e,\delta,\sigma)_{A,B}\in\mathsf{Mly}{B}(i,o)$ and
$(e^{\prime},\delta^{\prime},\sigma^{\prime})_{A^{\prime},B^{\prime}}\in\mathsf{Mly}{B}(i^{\prime},o^{\prime})$);
an _intertwiner_
$(u,v):(e,\delta,\sigma)\looparrowright(e^{\prime},\delta^{\prime},\sigma^{\prime})$
consists of a pair of 1-cells $u:A\to A^{\prime},v:B\to B^{\prime}$ and a
triple of 2-cells $\iota,\epsilon,\omega$ disposed as in (A.2), to which we
require to satisfy the identities in (A.1) (we provide a ‘birdseye’ view of
the commutativities that we require, as (A.2) is unambiguous about how the
2-cells $\iota,\delta,\sigma,\epsilon,\omega$ can be composed).

######  Remark 3.13.

Interestingly enough, when it is spelled out in the case when $\mymathbb{B}$
has a single 0-cell, this notion does not reduce to Remark 1.2, as an
intertwiner between a Mealy machine $(E,d,s)_{I,O}$ and another
$(E^{\prime},d^{\prime},s^{\prime})_{I^{\prime},O^{\prime}}$ consists of a
pair of objects $U,V\in\mathcal{K}$, such that

  1. ic1)

there exist morphisms $\iota:I^{\prime}\otimes U\to V\otimes
I,\epsilon:E^{\prime}\otimes U\to V\otimes E,\omega:O^{\prime}\otimes U\to
V\otimes O$;

  2. ic2)

the following two identities hold:

$\displaystyle\epsilon\circ(d^{\prime}\otimes U)=(V\otimes
d)\circ(\epsilon\otimes I)\circ(E^{\prime}\otimes\iota)$
$\displaystyle\omega\circ(s^{\prime}\otimes U)=(V\otimes
s)\circ(\epsilon\otimes I)\circ(E^{\prime}\otimes\iota)$

In the single-object case, this notion does not trivialise in any obvious way,
and –in stark contrast with the notion of morphism of automata given in (1.2)–
intertwiners between machines support a notion of higher morphisms _even in
the monoidal case_.

######  Definition 3.14 (2-cell between machines).

In the same notation of Definition 3.12, let
$(u,v),(u^{\prime},v^{\prime}):(e,\delta,\sigma)\looparrowright(e^{\prime},\delta^{\prime},\sigma^{\prime})$
be two parallel intertwiners between bicategorical Mealy machines; a 2-cell
$(\varphi,\psi):(u,v)\Rightarrow(u^{\prime},v^{\prime})$ consists of a pair of
2-cells $\varphi:u\Rightarrow u^{\prime}$, $\psi:v\Rightarrow v^{\prime}$ such
that the identities in (A.3) hold true.

######  Remark 3.15.

When it is specialised to the monoidal case, Definition 3.14 yields the
following notion: a 2-cell $(f,g):(U,V)\Rightarrow(U^{\prime},V^{\prime})$ as
in Remark 3.13 consists of a pair of morphisms $f:U\to U^{\prime}$ and $g:V\to
V^{\prime}$ subject to the conditions that the two squares in (A.4) commute:
intuitively speaking, in this particular case, the machine 2-cells correspond
to pairs $(f,g)$ of $\mathcal{K}$-morphisms such that both pairs
$(E^{\prime}\otimes I^{\prime}\otimes f,E^{\prime}\otimes f)$ and $(g\otimes
E\otimes I,g\otimes E)$ form morphisms in the arrow category of $\mathcal{K}$.

######  Remark 3.16.

Let $\mymathbb{B}$ be a bicategory; in [44] the authors exploit the universal
property of a bicategory
$\Omega\mymathbb{B}=\mathsf{Psd}(\textbf{N},\mymathbb{B})$ as the category of
pseudofunctors, lax natural transformations and modifications with domain the
monoid of natural numbers, regarded as a single object category. The typical
object of $\Omega\mymathbb{B}$ is an endomorphism $i:A\to A$ of an object
$A\in\mymathbb{B}$, and the typical 1-cell consists of a lax commutative
square

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{B.}$
(3.10)

This presentation begs the natural question of whether there is a tautological
functor $\mathsf{Mly}{B}\to\Omega\mymathbb{B}$ given by ‘projection’, sending
$(i,o;(e,\delta,\sigma))$ into $i$; the answer is clearly affirmative, and in
fact such functor mates to a unique 2-functor
$\textbf{N}\boxtimes\mathsf{Mly}{B}\to\mymathbb{B}$ under the isomorphism
given by Gray tensor product [31]; this somehow preserves the intuition (cf.
[66, §1]) of $\Omega\mymathbb{B}$ as a category of ‘lax dynamical systems’.

##  4 Conclusions

We sketch some directions for future research.

######  Conjecture 4.1.

Given a monad $T$ on $\mathsf{Set}$ and a quantale $\mathcal{V}$ [25, Ch. 2]
we can define the locally thin bicategory
$(T,\mathcal{V})\text{-}\mymathbb{Prof}$ as in [36, Ch. III]; as
$(T,\mathcal{V})$ vary we generate a plethora of bicategories, yielding the
categories of topological spaces, approach spaces [53], metric and
ultrametric, and closure spaces as the _$(T,\mathcal{V})$ -categories_ of [36,
§III.1.6]. We conjecture that when instantiated in
$(T,\mathcal{V})\text{-}\mymathbb{Prof}$, Equation 3.9 yields a 2-categorical
way to look at topological, metric and loosely speaking ‘fuzzy’ approaches to
automata theory.

######  Conjecture 4.2.

From Example 3.9 and 3.10 we argue that the ‘non-determinism via Kleisli
category’ approach of [34] can be carried over for the presheaf construction
on $\mathsf{Cat}$ and its Kleisli bicategory $\mymathbb{Prof}$: if automata
(classically intended) in the Kleisli category of the powerset monad are
nondeterministic automata in $\mathsf{Set}$, _bicategorical_ automata in the
Kleisli _bicategory_ of the _presheaf construction_ (cf. [26]) are
nondeterministic bicategorical automata: passing from Example 3.9 to Example
3.10 accounts for a form of non-determinism. But then one might be able to
address _nondeterministic_ bicategorical automata in $\mymathbb{B}$ as
_deterministic_ bicategorical automata in a generic proarrow equipment [61,
70, 71] for $\mymathbb{B}$!

## References

  * [1] J. Adámek, H. Herrlich, and G.E. Strecker.  Abstract and concrete categories: the Joy of cats, volume 17 of Reprints in Theory and Applications of Categories.  Theory and Applications of Categories, 2006.  Available online at http://www.tac.mta.ca/tac/reprints/articles/17/tr17.pdf.
  * [2] J. Adámek.  Realization theory for automata in categories.  Journal of Pure and Applied Algebra, 9:281–296, 1977.  doi:10.1016/0022-4049(77)90071-8.
  * [3] J. Adámek and V. Trnková.  Automata and Algebras in Categories.  Kluwer, 1990.
  * [4] B. Ahrens and P. L. Lumsdaine.  Displayed Categories.  Logical Methods in Computer Science, Volume 15, Issue 1, March 2019.  URL: https://lmcs.episciences.org/5252, doi:10.23638/LMCS-15(1:20)2019.
  * [5] M.A. Arbib and E.G. Manes.  Adjoint machines, state-behavior machines, and duality.  Journal of Pure and Applied Algebra, 6(3):313–344, 1975.  doi:10.1016/0022-4049(75)90028-6.
  * [6] M.A. Arbib and E.G. Manes.  A categorist’s view of automata and systems.  In Lecture Notes in Computer Science, pages 51–64. Springer Berlin Heidelberg, 1975.  doi:10.1007/3-540-07142-3_61.
  * [7] M.A. Arbib and E.G. Manes.  Fuzzy machines in a category.  Bulletin of the Australian Mathematical Society, 13(2):169–210, 1975.  doi:10.1017/S0004972700024412.
  * [8] M.A. Arbib and E.G. Manes.  Machines in a category.  Journal of Pure and Applied Algebra, 19:9–20, December 1980.  doi:10.1016/0022-4049(80)90090-0.
  * [9] E.S. Bainbridge.  A unified minimal realization theory, with duality, for machines in a hyperdoctrine.  In Technical Report. Computer and Communication Sciences Department, University of Michigan, 1972.
  * [10] E.S. Bainbridge.  Addressed machines and duality.  In Ernest Gene Manes, editor, Category Theory Applied to Computation and Control, pages 93–98, Berlin, Heidelberg, 1975. Springer Berlin Heidelberg.
  * [11] R. Betti and S. Kasangian.  A quasi-universal realization of automata.  Università degli Studi di Trieste. Dipartimento di Scienze Matematiche, 1981.
  * [12] R. Betti and S. Kasangian.  Una proprietà del comportamento degli automi completi.  Università degli Studi di Trieste. Dipartimento di Scienze Matematiche, 1982.
  * [13] G. Boccali, A. Laretto, F. Loregian, and S. Luneia.  Completeness for categories of generalized automata.  mar 2023.  arXiv:2303.03867.
  * [14] R Brown.  Topology and groupoids.  www.groupoids.org, rev., updated, and expanded version edition, 2006.
  * [15] E. Burroni.  Lois distributives. applications aux automates stochastiques.  Theory and Applications of Categories, 22:199–221, 2009.
  * [16] J. Bénabou and T. Streicher.  Distributors at work.  Lecture notes written by Thomas Streicher, 2000.
  * [17] G.L. Cattani and G. Winskel.  Profunctors, open maps and bisimulation.  Mathematical Structures in Computer Science, 15(03):553–614, 2005\.
  * [18] T. Colcombet and D. Petrisan.  Automata Minimization: a Functorial Approach.  In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of Leibniz International Proceedings in Informatics (LIPIcs), pages 8:1–8:16, Dagstuhl, Germany, 2017.  doi:10.4230/LIPIcs.CALCO.2017.8.
  * [19] P.R. D’Argenio and J.-P. Katoen.  A theory of stochastic systems part i: Stochastic automata.  Information and Computation, 203(1):1–38, November 2005.  doi:10.1016/j.ic.2005.07.001.
  * [20] M. Droste, W. Kuich, and H. Vogler, editors.  Handbook of Weighted Automata.  Springer Berlin Heidelberg, 2009.  doi:10.1007/978-3-642-01492-5.
  * [21] E.J. Dubuc.  Kan extensions in enriched category theory.  Lecture Notes in Mathematics, Vol. 145. Springer-Verlag, Berlin-New York, 1970.  doi:10.1007/BFb0060485.
  * [22] H. Ehrig, K.-D. Kiermeier, H.-J. Kreowski, and W. Kühnel.  Universal theory of automata. A categorical approach.  doi:10.1007/978-3-322-96644-5.
  * [23] S. Eilenberg.  Automata, Languages and Machines, volume A.  Academic Press, New York, 1974.
  * [24] S. Eilenberg and J.B. Wright.  Automata in general algebras.  Information and Control, 11(4):452–470, October 1967.  doi:10.1016/s0019-9958(67)90670-5.
  * [25] P. Eklund, J. Gutiérrez Garciá, U. Höhle, and J. Kortelainen.  Semigroups in Complete Lattices.  Springer International Publishing, 2018.  doi:10.1007/978-3-319-78948-4.
  * [26] M. Fiore, N. Gambino, M. Hyland, and G. Winskel.  Relative pseudomonads, kleisli bicategories, and substitution monoidal structures.  Selecta Mathematica, 24(3):2791–2830, November 2017.  doi:10.1007/s00029-017-0361-3.
  * [27] T.M. Fiore.  Pseudo Limits, Biadjoints, And Pseudo Algebras: Categorical Foundations of Conformal Field Theory.  Memoirs AMS 860. American Mathematical Society, 2006.
  * [28] J.A. Goguen.  Realisation is universal.  Mathematical System Theory, 6(4), 1973.
  * [29] J.A. Goguen.  Discrete-time machines in closed monoidal categories. I.  Journal of Computer and System Sciences, 10(1):1–43, February 1975\.  doi:10.1016/s0022-0000(75)80012-2.
  * [30] J.A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright.  Factorizations, congruences, and the decomposition of automata and systems.  In Lecture Notes in Computer Science, pages 33–45. Springer Berlin Heidelberg, 1975.  doi:10.1007/3-540-07162-8_665.
  * [31] J.W. Gray.  Formal Category Theory: Adjointness for 2-Categories.  Springer Berlin Heidelberg, 1974.  doi:10.1007/bfb0061280.
  * [32] R. Guitart.  Remarques sur les machines et les structures.  Cahiers de Topologie et Géométrie Différentielle Catégoriques, 15:113–144, 1974.
  * [33] R. Guitart.  Des machines aux bimodules.  Univ. Paris 7, apr 1978.  URL: http://rene.guitart.pagesperso-orange.fr/textespublications/rg30.pdf.
  * [34] R. Guitart.  Tenseurs et machines.  Cahiers de topologie et géométrie différentielle, 21(1):5–62, 1980.  URL: http://www.numdam.org/item/CTGDC_1980__21_1_5_0/.
  * [35] R. Guitart and L. Van den Bril.  Décompositions et Lax-complétions.  Cahiers de topologie et géométrie différentielle, 18(4):333–407, 1977.  URL: http://www.numdam.org/item/CTGDC_1977__18_4_333_0/.
  * [36] D. Hofmann, G.J. Seal, and W. Tholen.  Monoidal Topology: A Categorical Approach to Order, Metric, and Topology, volume 153.  Cambridge University Press, 2014.  doi:10.1017/CBO9781107517288.
  * [37] B. Jacobs.  Categorical Logic and Type Theory.  Number 141 in SLFM. Elsevier, 1999.
  * [38] B. Jacobs.  A bialgebraic review of deterministic automata, regular expressions and languages.  In Algebra, Meaning, and Computation, pages 375–404. Springer Berlin Heidelberg, 2006.  doi:10.1007/11780274_20.
  * [39] B. Jacobs.  New directions in categorical logic, for classical, probabilistic and quantum logic.  Logical Methods in Computer Science, 11(3):76, 2015.  Id/No 24.  doi:10.2168/LMCS-11(3:24)2015.
  * [40] B. Jacobs.  Introduction to Coalgebra: Towards Mathematics of States and Observation.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016.  doi:10.1017/CBO9781316823187.
  * [41] M. B. Justesen.  Bikategorien af profunktorer.  Naturvidenskabelig embedseksamen, Aarhus University, 1968.
  * [42] S. Kasangian, G.M. Kelly, and F. Rossi.  Cofibrations and the realization of non-deterministic automata.  Cahiers de topologie et géométrie différentielle catégoriques, 24(1):23–46, 1983.
  * [43] S. Kasangian and R. Rosebrugh.  Glueing enriched modules and composition of automata.  Cahiers de topologie et géométrie différentielle catégoriques, 31(4):283–290, 1990.
  * [44] P. Katis, N. Sabadini, and R.F.C. Walters.  Bicategories of processes.  Journal of Pure and Applied Algebra, 115(2):141–178, February 1997\.  doi:10.1016/s0022-4049(96)00012-6.
  * [45] P. Katis, N. Sabadini, and R.F.C. Walters.  Feedback, trace and fixed-point semantics.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 36(2):181–194, 2002.  URL: http://www.numdam.org/articles/10.1051/ita:2002009/, doi:10.1051/ita:2002009.
  * [46] G.M. Kelly.  A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on.  Bulletin of the Australian Mathematical Society, 22(01):1–83, 1980\.  doi:10.1017/S0004972700006353.
  * [47] A. Kock.  Limit monads in categories.  The University of Chicago, 1967.
  * [48] A. Kock.  Closed categories generated by commutative monads.  J. Austral. Math. Soc., 12:405–424, 1971.
  * [49] A. Kock.  Strong functors and monoidal monads.  Archiv der Mathematik, 23(1):113–120, 1972.
  * [50] S. Lack.  Note on the construction of free monoids.  Applied Categorical Structures, 18(1):17–29, October 2008.  doi:10.1007/s10485-008-9167-y.
  * [51] E. Di Lavore, A. Gianola, M. Román, N. Sabadini, and P. Sobociński.  A canonical algebra of open transition systems.  In Gwen Salaün and Anton Wijs, editors, Formal Aspects of Component Software - 17th International Conference, FACS 2021, Virtual Event, October 28-29, 2021, Proceedings, volume 13077 of Lecture Notes in Computer Science, pages 63–81. Springer, 2021.  doi:10.1007/978-3-030-90636-8\\_4.
  * [52] F. Loregian.  Coend Calculus, volume 468 of London Mathematical Society Lecture Note Series.  Cambridge University Press, first edition, jul 2021.  ISBN 9781108746120.
  * [53] R. Lowen.  Approach Spaces: The Missing Link in the Topology-uniformity-metric Triad.  Oxford mathematical monographs. Clarendon Press, 1997.
  * [54] J. Meseguer and U. Montanari.  Petri nets are monoids.  Information and Computation, 88(2):105–155, October 1990.  doi:10.1016/0890-5401(90)90013-8.
  * [55] J. Meseguer and I. Sols.  Automata in semimodule categories.  In Lecture Notes in Computer Science, pages 193–198. Springer Berlin Heidelberg, 1975.  doi:10.1007/3-540-07142-3_81.
  * [56] G. Naudé.  On the adjoint situations between behaviour and realization.  Quaestiones Mathematicae, 2:245–267, 1977.  doi:10.1080/16073606.1977.9632546.
  * [57] G. Naudé.  Universal realization.  Journal of Computer and System Sciences, 19(3):277–289, 1979.  doi:10.1016/0022-0000(79)90005-9.
  * [58] P. Perrone and W. Tholen.  Kan extensions are partial colimits.  Applied Categorical Structures, 30(4):685–753, January 2022.  doi:10.1007/s10485-021-09671-9.
  * [59] I. Pohl and M.A. Arbib.  Theories of abstract automata.  Mathematics of Computation, 24(111):760, jul 1970.  doi:10.2307/2004866.
  * [60] R. Rosebrugh, N. Sabadini, and R.F.C. Walters.  Minimal realization in bicategories of automata.  Mathematical Structures in Computer Science, 8(2):93–116, 1998\.  doi:10.1017/S0960129597002454.
  * [61] R. Rosebrugh and R.J. Wood.  Proarrows and cofibrations.  Journal of Pure and Applied Algebra, 53(3):271–296, 1988.  doi:10.1016/0022-4049(88)90128-4.
  * [62] J.M. Rutten.  Universal coalgebra: a theory of systems.  Theoretical Computer Science, 249(1):3–80, October 2000.  doi:10.1016/s0304-3975(00)00056-6.
  * [63] S. Singh and S.P. Tiwari.  On the category of L-fuzzy automata, coalgebras and dialgebras.  Fuzzy Sets and Systems, 420:1–28, September 2021.  doi:10.1016/j.fss.2020.07.013.
  * [64] R. Street.  Fibrations and Yoneda lemma in a 2-category.  In G.M. Kelly, editor, Proceedings Sydney Category Theory Seminar 1972/1973, volume 420 of Lecture Notes in Mathematics, pages 104–133. Springer, 1974.  doi:10.1007/BFb0063096.
  * [65] R. Street.  Fibrations in bicategories.  Cahiers de topologie et géométrie différentielle catégoriques, 21(2):111–160, 1980.
  * [66] M. Tierney.  Categorical Constructions in Stable Homotopy Theory.  Springer Berlin Heidelberg, 1969.  doi:10.1007/bfb0101425.
  * [67] Y. Venema.  Automata and fixed point logic: A coalgebraic perspective.  Information and Computation, 204(4):637–678, April 2006.  doi:10.1016/j.ic.2005.06.003.
  * [68] VV.AA.  Fugal: definition & meaning.  URL: https://www.merriam-webster.com/dictionary/fugal.
  * [69] R.F.C. Walters.  A note on context-free languages.  Journal of Pure and Applied Algebra, 62(2):199–203, December 1989\.  doi:10.1016/0022-4049(89)90151-5.
  * [70] R.J. Wood.  Abstract pro arrows I.  Cahiers de topologie et géométrie différentielle, 23(3):279–290, 1982.  URL: http://www.numdam.org/item/CTGDC_1982__23_3_279_0/.
  * [71] R.J. Wood.  Proarrows II.  Cahiers de Topologie et Géométrie Différentielle Catégoriques, 26(2):135–168, 1985.  URL: http://www.numdam.org/item/CTGDC_1985__26_2_135_0/.

##  Appendix A Appendix A: Proofs

###  A.1 Diagrams

$=$$\delta$$\delta^{\prime}$$\epsilon$$\epsilon$$\iota$$=$$\sigma$$\sigma^{\prime}$$\omega$$\epsilon$$\iota$and;
(A.1)
$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\iota}$$\scriptstyle{u}$$\scriptstyle{i}$$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i^{\prime}}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\epsilon}$$\scriptstyle{u}$$\scriptstyle{e}$$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e^{\prime}}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\scriptstyle\omega}$$\scriptstyle{u}$$\scriptstyle{o}$$\textstyle{A^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{o^{\prime}}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u}$$\textstyle{A^{\prime}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\textstyle{B^{\prime}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\textstyle{B^{\prime}}$
(A.2)
$\iota^{\prime}$$\varphi$$\iota$$\varphi$$=$$\epsilon^{\prime}$$\varphi$$\epsilon$$\psi$$=$$\omega^{\prime}$$\varphi$$\omega$$\psi$$=$
(A.3) $\textstyle{E^{\prime}\otimes I^{\prime}\otimes
U\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d^{\prime}\otimes
U}$$\scriptstyle{E^{\prime}\otimes I^{\prime}\otimes
f}$$\textstyle{E^{\prime}\otimes
U\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E^{\prime}\otimes
f}$$\textstyle{V\otimes E\otimes
I\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V\otimes
d}$$\scriptstyle{g\otimes E\otimes I}$$\textstyle{V\otimes
E\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g\otimes
E}$$\textstyle{E^{\prime}\otimes I^{\prime}\otimes
U^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{d^{\prime}\otimes
U^{\prime}}$$\textstyle{E^{\prime}\otimes
U^{\prime}}$$\textstyle{V^{\prime}\otimes E\otimes
I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V^{\prime}\otimes
d}$$\textstyle{V^{\prime}\otimes E}$ (A.4)

###  A.2 Proofs

###### Proof of Lemma 2.13.

In order to prove that the assignment $s\mapsto s^{\flat}$ is well defined in
the set of fugal automata, we proceed by induction on the length of a string
$\ell$. We have to prove that

$s^{\flat}(e,\ell\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}as)=s^{\flat}(e,\ell)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}s^{\flat}(d^{*}(e,\ell),as)$
(A.5)

The base case $\ell=[\,]$ is evidently true, so suppose that
$\ell=x\mathbin{::}xs$ is not empty and the claim is true for every choice of
a shorter $xs$: then,

$\displaystyle
s^{\flat}(e,(x\mathbin{::}xs)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}as)$
$\displaystyle=s^{\flat}(e,(x\mathbin{::}xs)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}as)$
$\displaystyle=s^{\flat}(e,x\mathbin{::}(xs\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}as))$
$\displaystyle=s(e,x)\mathbin{::}s^{\flat}(d(e,x),xs\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}as)$
$\displaystyle=s(e,x)\mathbin{::}\big{(}s^{\flat}(d(e,x),xs)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}s^{\flat}(d^{*}(e,xs),as)\big{)}$
$\displaystyle=\big{(}s(e,x)\mathbin{::}s^{\flat}(d(e,x),xs)\big{)}\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}s^{\flat}(d(x,d^{*}(e,xs)),as)$
$\displaystyle=s^{\flat}(e,x\mathbin{::}xs)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}s^{\flat}(d^{*}(e,x\mathbin{::}xs),as)$
$\displaystyle=s^{\flat}(e,\ell)\mathbin{\scalebox{0.8}{$+\kern-1.99997pt+$}}s^{\flat}(d^{*}(e,\ell),as).$

We now have to show that any 2-cell $f:(E,d,s)\to(F,c,t)$ is in fact a 2-cell
$(E,d^{*},s^{\flat})\to(F,c^{*},t^{\flat})$. This can be done by induction as
well, with completely similar reasoning.∎

###### Proof of Lemma 2.16.

We have to prove that

$(s_{2}\mathbin{\diamondsuit}s_{1})^{\flat}=s_{2}^{\flat}\mathbin{\diamondsuit}s_{1}^{\flat}.$
(A.6)

The two functions coincide on the empty list by definition; hence, let
$\ell=a\mathbin{::}as$ be a nonempty list and $(e,f)\in E\times F$ a generic
element. The right-hand side of the equation is

$\displaystyle(s_{2}^{\flat}\mathbin{\diamondsuit}s_{1}^{\flat})((e,f),a\mathbin{::}as)$
$\displaystyle=s_{2}^{\flat}(f,s_{1}^{\flat}(e,a\mathbin{::}as))$
$\displaystyle=s_{2}^{\flat}\big{(}f,s_{1}(e,a)\mathbin{::}s_{1}^{\flat}(d_{1}(e,a),as)\big{)}$
$\displaystyle=s_{2}(f,s_{1}(e,a))\mathbin{::}s_{2}^{\flat}(d_{2}(f,s_{1}(e,a)),s_{1}^{\flat}(d_{1}(e,a),as))$
$\displaystyle=(s_{2}\mathbin{\diamondsuit}s_{1})((e,f),a)\mathbin{::}(s_{2}\mathbin{\diamondsuit}s_{1})^{\flat}((d_{2}\mathbin{\diamondsuit}d_{1})((e,f),a),as)$

which concludes the proof. ∎

###### Proof of Theorem 2.17.

Similarly to Lemma 2.16, we have to prove that
$d_{2}^{*}\mathbin{\diamondsuit}d_{1}^{*}=(d_{2}\mathbin{\diamondsuit}d_{1})^{*}$
whenever $d_{2},d_{1}$ are two dynamic maps of composable Mealy machines
$\langle s_{1},d_{1}\rangle:E\times M\to N\times E$ and $\langle
s_{2},d_{2}\rangle:F\times N\to P\times F$. This, together with Lemma 2.16,
will establish functoriality on 1-cells of
$(\,\rule{5.0pt}{0.4pt}\,)^{\flat}$. Functoriality on 2-cells is very easy to
establish. For what concerns $\Pi$, the proof amounts to showing that the
composition of (fugal) Mealy machines gets mapped into the composition of
spans in $\mathsf{Mac}^{\mathrm{s}}$; this can be checked with ease and
follows from the fact that the translation category of the action
$d_{2}\mathbin{\diamondsuit}d_{1}$ as defined in (2.2) has the universal
property of the pullback $\mathcal{Z}$ in

---
$\textstyle{\mathcal{Z}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{E}[d_{1}^{*}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Sigma_{1}}$$\scriptstyle{D_{1}}$$\textstyle{\mathcal{E}[d_{2}^{*}]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Sigma_{2}}$$\scriptstyle{D_{2}}$$\textstyle{M}$$\textstyle{N}$$\textstyle{R.}$
(A.7)

This is a straightforward check, and it is also straightforward to see that
the composition of $\Sigma_{2}$ with the right projection from $\mathcal{Z}$
coincides with the ‘Sigma’ functor induced by
$s_{2}\mathbin{\diamondsuit}s_{1}$, which concludes the proof. ∎

###### Proof of Theorem 2.18.

It is worthwhile to recall what a biadjunction is

$\textstyle{F:\mathsf{C}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\perp}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathsf{D}:G}$
(A.8)

if $\mathsf{C},\mathsf{D}$ are bicategories (cf. [27, Ch. 9]): for each two
objects $C,D$ we are given an equivalence between hom-categories
$\mathsf{D}(FC,D)\simeq\mathsf{C}(C,GD)$, i.e. a pair of functors
$H:\mathsf{D}(FC,D)\leftrightarrows\mathsf{C}(C,GD):K$ whose composition in
both directions is isomorphic to the identity functor of the respective hom-
category –and all this depends naturally on $C,D$.

In order to prove this, let’s fix a set $A$ and a monoid $M$, let’s build
functors

$\textstyle{\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},M)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{H}$$\textstyle{\mathsf{Mly}_{\mathsf{Set}}(A,UM)}$$\textstyle{\mathsf{Mly}_{\mathsf{Set}}(A,UM)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{K}$$\textstyle{\mathsf{Mly}^{\flat}_{\mathsf{Set}}(A^{*},M)}$
(A.9)

and prove that they form an equivalence of categories by explicitly showing
that $HK$ and $KH$ are isomorphic to the respective identities. We’ll often
adopt the convenient notation $\langle s,d\rangle:E\times X\to Y\times E$ for
a Mealy machine of input $X$ and output $Y$.

  * •

Let $\langle s,d\rangle:E\times A^{*}\to M\times E$ be a fugal Mealy machine;
$H\langle s,d\rangle$ is defined as the composition

$\textstyle{E\times
A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E\times\eta_{A}}$$\textstyle{E\times
A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
s,d\rangle}$$\textstyle{M\times E}$ (A.10)

where $\eta_{A}:A\to A^{*}$ is the unit of the free-forgetful adjunction
between $\mathsf{Set}$ and monoids. In simple terms, $H$ acts ‘restricting’ a
fugal Mealy machine to the set of generators of its input.

  * •

Let $\langle s_{0},d_{0}\rangle:F\times A\to UM\times F$ be any Mealy machine
on $\mathsf{Set}$, where $UM$ means that $M$ is regarded as a mere set;
$K\langle s_{0},d_{0}\rangle$ is defined as the composition

$\textstyle{F\times
A^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
s_{0},d_{0}\rangle^{\flat}}$$\textstyle{(UM)^{*}\times
F\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varepsilon\times
F}$$\textstyle{M\times F}$ (A.11)

where $\varepsilon:(UM)^{*}\to M$ is the counit of the free-forgetful
adjunction between $\mathsf{Set}$ and monoids, and $\langle
s_{0},d_{0}\rangle^{\flat}$ is the fugal extension of Lemma 2.13.

The claim is now that the fugal Mealy machine $KH\langle s,d\rangle$ coincides
with $\langle s,d\rangle$, and that the generic Mealy machine $HK\langle
s_{0},d_{0}\rangle$ coincides with $\langle s_{0},d_{0}\rangle$.

Both statements depend crucially on the following fact: if $s:E\times M\to N$
satisfies Equation (2.8), then for all $e\in E$ the element $s(1_{M},e)$ is
idempotent in $N$. In particular, if $N$ is free on a set $B$,
$s(1_{M},e)=[\,]$ is the empty list, and more in particular, for a generic
Mealy machine $\langle s,\,\rule{5.0pt}{0.4pt}\,\rangle$ the fugal extension
$s^{\flat}$ is such that for all $e\in E$, $s^{\flat}([\,],e)=[\,]$.

Given this, observe that the Mealy machine $HK\langle s_{0},d_{0}\rangle$
coincides with $\langle
s_{0}^{\flat}\circ(F\times\eta_{A}),d_{0}^{*}\circ(F\times\eta_{A})\rangle$;
now clearly the composition $d_{0}^{*}\circ(F\times\eta_{A})$ coincides with
$d_{0}:F\times A\to F$ and the two maps determine each other. As for
$s_{0}^{\flat}\circ(F\times\eta_{A})$, we have that for all $(f,a)\in F\times
A$

$\displaystyle s_{0}^{\flat}\circ(F\times\eta_{A})(f,a)$
$\displaystyle=s_{0}^{\flat}(f,a\mathbin{::}[\,])$
$\displaystyle=s_{0}(f,a)\mathbin{::}s^{\flat}_{0}(f,[\,])$
$\displaystyle=s_{0}(f,a)\mathbin{::}[\,]$

Reasoning similarly, one proves that the fugal Mealy machine $KH\langle
s,d\rangle$ has components
$\langle(s\circ(E\times\eta_{A}))^{\flat},(d\circ(E\times\eta_{A}))^{*}\rangle$:
again, since functions $E\times A\to E$ correspond bijectively to monoid
actions $E\times A^{*}\to E$, the map $(d\circ(E\times\eta_{A}))^{*}$
coincides with $d$; as for $(s\circ(E\times\eta_{A}))^{\flat}$, we can argue
by induction that

$\displaystyle(s\circ(E\times\eta_{A}))^{\flat}(e,[\,])$
$\displaystyle=[\,]=s(e,[\,])$
$\displaystyle(s\circ(E\times\eta_{A}))^{\flat}(e,a\mathbin{::}as)$
$\displaystyle=s(e,a)\mathbin{::}(s\circ(E\times\eta_{A}))^{\flat}(d(a,e),as)$
$\displaystyle=s(e,a)\mathbin{::}s(d(a,e),as)$
$\displaystyle=s(e,a\mathbin{::}as)$

where the last equality uses that $s$ was fugal to start with. This concludes
the proof. ∎

###### Proof of Proposition 3.8.

The category $\mathcal{P}$ is in fact 2-discrete (it has no 2-cells) and its
objects and morphisms are arranged as follows:

$\textstyle{1}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces
0\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{y}$$\scriptstyle{x}$$\scriptstyle{z}$$\scriptstyle{t}$$\textstyle{2}$
(A.12)

For lack of a better name, $\mathcal{P}$ is the _generic double span_.

The functors $W,G$ are then constructed as follows:

  * •

$G:\mathcal{P}\to\mathsf{Cat}$ is constant on objects at the category
$\mathcal{K}(A,B)$, and chooses the double span

$\textstyle{\mathcal{K}(A,B)}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathcal{K}(A,B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\operatorname{id}}$$\scriptstyle{\operatorname{id}}$$\scriptstyle{\,\rule{5.0pt}{0.4pt}\,\circ
i}$$\scriptstyle{\operatorname{id}}$$\textstyle{\mathcal{K}(A,B);}$ (A.13)

  * •

$W:\mathcal{P}\to\mathsf{Cat}$ chooses the double span

$\textstyle{\\{0\to
1\\}}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\\{\heartsuit,\spadesuit\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{j}$$\scriptstyle{j}$$\scriptstyle{c_{0}}$$\scriptstyle{c_{1}}$$\textstyle{\\{0\to
1\\}}$ (A.14)

where $\\{\heartsuit,\spadesuit\\}$ is a discrete category with two objects,
$j=\left(\begin{smallmatrix}\heartsuit\mapsto 0\\\ \spadesuit\mapsto
1\end{smallmatrix}\right)$, and $c_{k}$ is constant at $k\in\\{0,1\\}$.

Now, it is a matter of unwinding the definition of a natural transformation
$\alpha:W\Rightarrow G$ to find that we are provided with maps

$\displaystyle\\{e,\\#\\}$ $\displaystyle=\alpha_{0}:W0\to\mathcal{K}(A,B)$
$\displaystyle\sigma$ $\displaystyle=\alpha_{1}:W1\to\mathcal{K}(A,B)$ (A.15)
$\displaystyle\delta$ $\displaystyle=\alpha_{2}:W2\to\mathcal{K}(A,B)$

and with commutative diagrams arising from naturality as follows, if we agree
to label $\alpha_{0}(\heartsuit)=e$ and $\alpha_{0}(\spadesuit)=o$, and we
blur the distinction between $\alpha_{0}$ and the embedding of its image
$\\{e,o\\}$ in $\mathcal{K}(A,B)$:

$\textstyle{\\{e,o\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{j}$$\scriptstyle{\alpha_{0}}$$\textstyle{\\{0\to
1\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{1}}$$\textstyle{\\{e,o\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c_{0}}$$\scriptstyle{\alpha_{0}}$$\textstyle{\\{0\to
1\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{2}}$$\textstyle{\\{e,o\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c_{1}}$$\scriptstyle{\alpha_{0}}$$\textstyle{\\{0\to
1\\}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\alpha_{2}}$$\textstyle{\mathcal{K}(A,B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{K}(A,B)}$$\textstyle{\mathcal{K}(A,B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\,\rule{5.0pt}{0.4pt}\,\circ
i}$$\textstyle{\mathcal{K}(A,B)}$$\textstyle{\mathcal{K}(A,B)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathcal{K}(A,B)}$
(A.16)

Altogether, we have that these data yield a diagram of 2-cells

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\scriptstyle{e}$$\textstyle{\scriptstyle
o}$$\textstyle{\scriptstyle\sigma}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{\scriptstyle\delta}$$\textstyle{B}$
(A.17)

as in (3.2). Modifications between these natural transformations correspond to
suitable arrangements of 2-cells, in such a way that we recover the notion of
morphism of bicategorical Moore machine given in bmo2.

In case the output $o$ is fixed, we just constrain $\alpha_{0}(\spadesuit)$ to
be mapped in $o$ and modifications to be the identity at $\spadesuit$.

For bicategorical Mealy machines, redefine $Gx=Gz=\,\rule{5.0pt}{0.4pt}\,\circ
i$ and the rest of the argument is unchanged. ∎

######  Discussion A.1.

In a world of war and crippling inflation bytes are expensive, so page limits
shorten by the month. _This forces authors to shrink their papers, and the
only way to do that is remove text._

A simple interpolation suggests that _one day, the average submission will
consist of just the picture of a cat surrounded by a circle and a square_ ;
already today, we feel constrained to push in the appendix the email addresses
of the authors<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>and<EMAIL_ADDRESS>