Completeness for categories of generalized automata

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{M}\mathsf{l}\mathsf{y}$ and $F\text{-}\mathsf{M}\mathsf{r}\mathsf{e}$; such categories can be presented as strict 2-pullbacks in $\mathsf{C}\mathsf{a}\mathsf{t}$ and whenever $F$ is a left adjoint, both $F\text{-}\mathsf{M}\mathsf{l}\mathsf{y}$ and $F\text{-}\mathsf{M}\mathsf{r}\mathsf{e}$ 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.