Comonads, coequations and behavioural covarieties

Abstract

Coalgebras are a category theoretic construction of interest to theoretical computer science, defined by an endofunctor T : C → C over a category C. A class K of T-coalgebras is a covariety if it is closed under coproducts, codomains of epi coalgebraic morphisms and subcoalgebras, and a behavioural covariety if it is also closed under images of bisimulations. Often the forgetful functor from the category of T-coalgebras to C has a right adjoint. This adjunction defines a comonad G T. Goldblatt [10] investigated this situation over the category Set, introducing the notion of a pure subcomonad of a comonad, and showing a bijective correspondence between (equivalence classes of) pure subcomonads of GT and behavioural covarieties of T-coalgebras. This thesis demonstrates what restrictions need to be applied to an arbitrary category C and endofunctor T : C → C to attain this bijection. All restrictions on C and T are shown to apply to an endofunctor ()I on a category Set that is useful for modelling automata. The thesis goes on to show that pure subcomonads give rise to subcoalgebras of the final coalgebra called coequations over 1, and demonstrates a bijective correspondence between behavioural co-varieties of T-coalgebras and coequations over 1. Finally the thesis demonstrates a bijective correspondence between covarieties of T-coalgebras and a class of subcomonads called regulating subcomonads.