Toposes of Coalgebras and Hidden Algebras
James Worrell · Electronic Notes in Theoretical Computer Science · 1998
There is a long tradition in computer science of modelling finite data types such as stacks and natural numbers by algebras. More recently coalgebras, which are dual to algebras, have been used to model infinite data types and in operational semantics. In this report we consider categories of coalgebras from the perspective of topos theory. A mild generalisation of a well known theorem about toposes of coalgebras of a comonad is given. This result is used to prove that if B is a pullback preserving functor on a topos ∊, and if the forgetful functor UB : ∊B → ∊ has a right adjoint then ∊B, the category of B-coalgebras, is itself a topos. We also show that, if B is a bounded functor on Set preserving weak pullbacks, then the category SetB of B-coalgebras has a subobject classifier and is a reflective full subcategory of a Grothendieck topos. We mention an elementary construction of this topos, pointed out to us by [12], as the reflection of SetB in the category of effective regular categories. We are particularly interested in hidden algebra, a formalism in the algebraic specification tradition with close links to coalgebra, capturing notions of state and behavioural equivalence. For a hidden destructor signature Σ we exhibit the topos structure of the category of hidden Σ-algebras.