Automata in W-Toposes, and General Myhill-Nerode Theorems

We extend the functorial approach to automata by Colcombet and Petrişan [7] from the category of sets to any W-topos and establish general Myhill-Nerode theorems in our setting, including an explicit relationship between the syntactic monoid and the transition monoid of the minimal automaton. As a special case we recover the result of Bojańczyk, Klin and Lasota [5] for orbit-finite nominal automata by considering automata in the Myhill-Schanuel topos of nominal sets.