Covarieties of Coalgebras: Comonads and Coequations
by Ranald Clouston and Robert Goldblatt
Coalgebras provide effective models of data structures and
state-transition systems. A virtual
covariety is a class of coalgebras closed under coproducts,
images of coalgebraic morphisms, and subcoalgebras defined by
split equalisers. A covariety
has the stronger property of closure under all subcoalgebras, and
is behavioural if it is
closed under domains of morphisms, or equivalently under images of
bisimulations. There are many computationally interesting properties
that define classes of these kinds.
We identify conditions on the underlying category of a comonad $\G$
which ensure that there is an exact correspondence between
(behavioural/virtual) covarieties of $\G$-coalgebras and subcomonads of $\G$ defined by
comonad morphisms to $\G$ with natural categorical properties. We also
relate this analysis to notions of coequationally
defined classes of coalgebras.