A Comonadic Account of Behavioural Covarieties of Coalgebras
A class K of coalgebras for an endofunctor T on the category of sets is a behavioural covariety if it is
closed under disjoint unions and images of bisimulation relations
(hence closed under images and domains of coalgebraic morphisms,
including subcoalgebras). K
may be thought of as the class of all coalgebras that satisfy some
computationally significant property. In any logical system suitable
for specifying properties of state-transition systems in the
Hennessy-Milner style, each formula will define a class of models that
is a behavioural variety.
Assume that the forgetful functor on T-coalgebras
has a right adjoint, providing for the construction of cofree
coalgebras, and let G^T be the comonad arising from this
adjunction. Then we show that behavioural covarieties K are (isomorphic to) the
Eilenberg-Moore categories of coalgebras for certain comonads G^K naturally associated with G^T.
These are called pure subcomonads
of G^T, and a categorical
characterization of them is given, involving a pullback condition on the
naturality squares of a transformation from G^K
to G^T.
We show that there is a bijective correspondence between
behavioural covarieties of T-coalgebras
and isomorphism classes of pure subcomonads of G^T.