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\leftarrow E\otimes I\to O$ that usually defines a deterministic automaton of input $I$ and output $O$ in a monoidal category $(\mathcal{K},\otimes )$ is replaced by a span $E\leftarrow FE\to O$ for a generic endofunctor $F:\mathcal{K}\to \mathcal{K}$ of a generic category $\mathcal{K}$: these automata exist in their `Mealy' and `Moore' version and form categories $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$; such categories can be presented as strict 2-pullbacks in $\mathsf{Cat}$ and whenever $F$ is a left adjoint, both $F\text{-}\mathsf{Mly}$ and $F\text{-}\mathsf{Mre}$ admit all limits and colimits that $\mathcal{K}$ admits. We mechanize some of of our main results using the proof assistant Agda and the library `agda-categories`.