  We study the semibicategory $\textsf{Mre}$ of "Moore automata": an
arrangement of objects, 1- and 2-cells which is inherently and irredeemably
nonunital in dimension one.
  Between the semibicategory of Moore automata and the better behaved
bicategory $\textsf{Mly}$ of "Mealy automata" a plethora of adjunctions insist:
the well-known essential equivalence between the two kinds of state machines
that model the definitions of $\textsf{Mre}$ and $\textsf{Mly}$ is appreciated
at the categorical level, as the equivalence induced between the fixpoints of
an adjunction, in fact exhibiting $\textsf{Mre}(A,B)$ as a coreflective
subcategory of $\textsf{Mly}(A,B)$; the comodality induced by this adjunction
is but the $0$th step of a `level-like' filtration of the bicategory
$\textsf{Mre}$ in a countable family of essential bi-localizations
$\textsf{s}^n\textsf{Mre}\subseteq\textsf{Mre}$. We outline a way to generate
intrinsically meaningful adjunctions of this form. We mechanize some of our
main results using the proof assistant Agda.
