Completeness for categories of generalized automata

Abstract: We present a slick proof of completeness and cocompleteness for categories of

F

-automata, where the span of maps

E l e f t a r r o w E o t i m e s I o O

that usually defines a deterministic automaton of input

I

and output

O

in a monoidal category

(m a t h c a l K, o t i m e s)

is replaced by a span

E l e f t a r r o w F E o O

for a generic endofunctor

F : m a t h c a l K o m a t h c a l K

of a generic category

m a t h c a l K

: these automata exist in their `Mealy' and `Moore' version and form categories

F e x t - m a t h s f M l y

and

F e x t - m a t h s f M r e

; such categories can be presented as strict 2-pullbacks in

m a t h s f C a t

and whenever

F

is a left adjoint, both

F e x t - m a t h s f M l y

and

F e x t - m a t h s f M r e

admit all limits and colimits that

m a t h c a l K

admits. We mechanize some of of our main results using the proof assistant Agda and the library `agda-categories`.

This page was built for publication: Completeness for categories of generalized automata