Definition Mealy Machine [efr-0005]

In a dynamical systems theory, a Mealy machine with state space S and interface A consists of a costate lens TS \otimes A \leftrightarrows I. The category of Mealy machines with interface A is the comma category of the functor T(-) \otimes A over I---that is, a morphism of Mealy machines is S \to S' so that the obvious triangle commutes.