Under consideration for publication in Math. Struct. in Comp. Science

Operations and Equations for Coalgebras

Alexander Kurz^{1}^{†} and Jiří Rosický^{2} ^{‡}

1 Department of Computer Science, University of Leicester, UK. 2 Masaryk University, Janáčkovo nám. 2a, 662 95 Brno, Czech Republic.

Received 2nd February 2004

We show how coalgebras can be presented by operations and equations. This is a special case of Linton’s approach to algebras over a general base category X, namely where X is taken as the dual of sets. Since the resulting equations generalise coalgebraic coequations to situations without cofree coalgebras, we call them coequations. We prove a general co-Birkhoff theorem describing covarieties of coalgebras by means of coequations. We argue that the resulting coequational logic generalises modal logic. This relies on the fact that coalgebraic operations respect an appropriate notion of bisimulation and can be considered as modal operators.

Introduction

Let us start with recalling that universal algebras are defined as sets equipped with operations subjected to equations. Operations can be infinitary. Given a set X, a mapping f : A^{X} → A is an X-ary operation on a set A. One is often working with Y -tuples f_{y} : A^{X} → A, y ∈ Y, of X-ary operations on a set A. These Y -tuples uniquely correspond to mappings f : A^{X} → A^{Y}. Starting with a set of operations one always has free algebras. But there are important examples of universal algebras given by a class of operations which still have free algebras (complete semilattices, compact Hausdorff spaces). Linton showed in (Linton, 1966) that equationally defined universal algebras are, under the existence of free algebras, precisely the monadic categories over Set. Moreover, in (Linton, 1969), he generalised the result from sets to any base category X. In that work, operations are still mappings

f : A^{X} → A^{Y}

where A, X, and Y are objects in X and A^{X} is the set of all morphisms X → A. Note that, in Set, A^{X} coincides with the X-fold product of A. In general, however, it is important to consider A^{X} as a set of morphisms because the other approach would be too special for a general base category X. In particular, it would be too special for

† Partially supported by the Ministry of Education of the Czech Republic under the project MSM

143100009. ‡ Supported by the Grant Agency of the Czech Republic under the grant 201/02/0148.

X = Set^{op}. (Davis, 1972) used Linton’s approach for introducing universal coalgebras over Set even without assuming the existence of cofree coalgebras (i.e., free algebras over Set^{op}). The second author then considered Linton’s algebras over a general base category, without the existence of free algebras, in (Rosický, 1981).

There is another way of defining universal algebras over a general base category. One starts with an endofunctor F : X → X and defines F -algebras as objects A equipped with a morphism α : F A → A. These algebras are called F -dynamics in (Manes, 1976) and were extensively studied by Trnková and her students in Prague, cf. (Adámek and Trnková, 1990). Notably, (Reiterman, 1983) compared F -algebras with algebras given by operations and equations.

There is a revived interest in universal coalgebra motivated by its connections with the theory of systems, see (Rutten, 2000). Coalgebras are here understood as F -algebras over X = Set^{op}, i.e., as sets A equipped with a mapping α : A → F A where F : Set → Set. Our aim is to show the potential of defining coalgebras by means of operations and equations.

Outline of the Paper We investigate coequational categories, that is, categories of coalgebras that are presented by operations and equations. It turns out that coequational categories subsume categories of coalgebras for a functor or for a comonad (Section 2). To understand the nature of coalgebraic operations we introduce a novel notion of behavioural equivalence (generalising Aczel-Mendler bisimulation) and establish that coalgebraic operations are predicate transformers that respect behavioural equivalence (Section 3). We then introduce equations in implicit operations for coalgebras. Since they generalise previous concepts of coalgebraic coequations to situations without cofree coalgebras, we call them coequations. We prove a general co-Birkhoff theorem showing that covarieties of coalgebras are always definable by coequations (Section 4). Since our coequations on the one hand dualise equations for algebras and on the other hand can be understood as modal formulae, a new account of the duality of modal logic and equational logic arises (Section 5). The last section provides a full explanation of the theorem of (Davis, 1972) saying that any conceivable category of coalgebras can be given by operations and coequations provided that we allow the arities of the operations to be proper classes.

Acknowledgements The first author wants to thank Alexandru Baltag for pointing out an example of a modal operator that is not an implicit operation and Yde Venema for the observation that the morphisms of monotone neighbourhood frames coincide with the morphisms of (2^{2^{−}})-coalgebras. The second author profited from discussions with H.P. Gumm. Diagrams were produced with Paul Taylor’s macro package.

1. Preliminaries

We work in Gödel-Bernays set theory with the axiom of choice for classes. It means that all proper classes are isomorphic, in particular to the class Ord of all ordinals. Categories are assumed to be locally small, which means that they have a class of objects and sets of morphisms between any two given objects. Occasionally we encounter categories which do not satisfy this requirement and we call them illegitimate.

Given an endofunctor F : X → X, an F -coalgebra A = (A, α) consists of an object A ∈ X and an arrow α : A → F A. F -coalgebras form a category FCoalg(F) where a F -morphism f : (A, α) → (B, β) is an arrow f : A → B ∈ X such that F f ∘ α = β ∘ f. The forgetful functor U : FCoalg(F) → X maps a coalgebra (A, α) to A and a morphism f : (A, α) → (B, β) to the arrow f : A → B in X. U creates and hence preserves colimits.

A comonad (M, ε, δ) is given by a functor M : X → X and two natural transformations ε : M → Id, δ : M → MM satisfying Mε_{X} ∘ δ_{X} = ε_{MX} ∘ δ_{X} = id_{MX} and Mδ_{X} ∘ δ_{X} = δ_{MX} ∘ δ_{X}. The category CCoalg(M) of coalgebras for the comonad M is the full subcategory of FCoalg(M) whose coalgebras ξ : X → MX satisfy Mξ ∘ ξ = δ_{X} ∘ ξ and ε_{X} ∘ ξ = id_{X}.

Set denotes the category of sets and functions and P : Set → Set the covariant powerset functor. We also use the convention 2 = {0, 1} and call the elements of 2 truth values.

Given A, X ∈ X, the set of arrows A → X is denoted by X^{A} or sometimes X (A, X). For f : X → Y, the function f^{A} : X^{A} → Y^{A} is defined as f^{A}(g : A → X) = f ∘ g. For f : A → B, the function X^{f} : X^{B} → X^{A} is defined as X^{f}(g : B → X) = g ∘ f. For instance, with X = Set, 2^{A} is the set of subsets of A and 2^{f} : 2^{B} → 2^{A} is the inverse-image-map of f : A → B. The assignment − ↦ X^{−} gives rise to a functor X^{−} : X^{op} → Set. We write X^{U} for the functor A^{op} → Set obtained from composing U : A → X and X^{−} : X^{op} → Set.

A concrete category (A, U) (over X) is a faithful functor U : A → X. A functor F : A → A′ is a concrete functor between the concrete categories U : A → X and U : A′ → X if U′F = U. Concrete categories are concretely isomorphic if the isomorphisms are concrete functors.

2. Coalgebras for a Signature

Recall from the introduction that algebras over a category X are given by a carrier A ∈ X and operations A^{X} → A^{Y} where A^{X} = X (X, A) denotes the set of arrows A → X. Since universal coalgebra over X is universal algebra over X^{op} and X^{op}(X, A) = X (A, X), coalgebras over a category X can be introduced as carriers A ∈ X equipped with operations

f : X^{A} → Y^{A}.

Definition 2.1 (Coalgebras for a signature). A signature Σ over a category X is a class of operation symbols σ each equipped with a pair (X, Y) of objects of X. We call σ a (X, Y)-ary operation symbol. A Σ-coalgebra A is an object A ∈ X together with maps

σ_{A} : X^{A} → Y^{A}

for each (X, Y)-ary operation symbol σ ∈ Σ. A morphism of Σ-coalgebras is defined as an arrow h : A → B such that the following square commutes

[figure: X^{A}; σ_{A}; Y^{A}; X^{B}; X^{h}; σ_{B}; Y^{B}; Y^{h}]

for all σ in Σ. The resulting (illegitimate) category of coalgebras is denoted by SCoalg(Σ).

Example 2.2. 1 If X = Set and Σ consists of a single (1, 2)-operation symbol, then SCoalg(Σ) has

as objects pairs (A, A′ ⊆ A) and morphisms h : (A, A′) → (B, B′) are functions h : A → B such that h^{−1}(B′) = A′.

2 Let X = Set and consider the signature Σ consisting of a single (2, 2)-ary operation symbol □. Σ-coalgebras are predicate transformers □_{A} : 2^{A} → 2^{A}. f : A → B is a coalgebra morphism iff a ∈ □_{A}(f^{−1}(V)) ⇔ f(a) ∈ □_{B}(V). We can think of Σ-coalgebras as transition systems via the concrete isomorphism SCoalg(Σ) ≅ FCoalg(2^{(2^{−})}) which associates to each □_{A} : 2^{A} → 2^{A} the hypersystem (cf. (Rutten, 2000)) ⊡ : A → 2^{2^{A}} given by U ∈ ⊡_{A}(a) ⇔ a ∈ □_{A}(U). The condition on f to be a morphism can then be written more suggestively as a ⟶_{A} f^{−1}(V) ⇔ f(a) ⟶_{B} V.

3 Let X be a category of topological spaces containing the topological space 𝟚 = (2, {∅, {1}, {0, 1}}). The elements of X (A, 𝟚) are the open sets of A and a (𝟚, 𝟚)- ary operation □ is a topological predicate transformer, cf. (Smyth, 1983). Similarly, if 2 is the two-element discrete space, then the elements of X (A, 2) are the clopen (i.e., closed and open) subsets of A.

4 If X = Set^{op} then SCoalg(Σ) is dually isomorphic to the category of algebras over Set for the signature Σ.

Proposition 2.3. Let Σ be a signature over Set consisting of a set of operation symbols. Then there exist a functor F : Set → Set such that the categories SCoalg(Σ) and FCoalg(F) are concretely isomorphic.

Proof. Let σ be a (X, Y)-ary operation symbol from Σ and A a Σ coalgebra. Then the mapping

σ_{A} : X^{A} → Y^{A}

determines the mapping

σ̂_{A} : A → Y^{X^{A}}.

Let F be the product of functors Y^{X^{−}} over all σ ∈ Σ. Then A determines a F -coalgebra (A, α) where α : A → F A is induced by σ̂_{A}, σ ∈ Σ. Any F -coalgebra is given in this way. Let h : A → B be a morphism of Σ-coalgebras. Since Y^{h} ∘σ_{B} determines the composition

[figure: A; h; B; σ̂_{B}; Y^{X^{B}}]

and σ_{A} ∘ X^{h} determines

[figure: A; σ̂_{A}; Y^{X^{A}}; Y^{X^{h}}; Y^{X^{B}}.]

h is a morphism of F -coalgebras. Again, any F -coalgebra morphism is given in this way. Hence SCoalg(Σ) ≅ FCoalg(F).

As usual, a signature Σ gives rise to terms. Terms are also equipped with arities and defined as follows: 1 every (X, Y)-ary operation symbol is an (X, Y)-ary term, 2 every mapping f : X → Y determines an (X, Y)-ary term x_{f}, 3 having an (X, Y)-ary term t_{1} and an (Y, Z)-ary term t_{2}, we get an (X, Z)-ary term

t_{2} · t_{1}. For each (X, Y)-ary term t and a Σ-coalgebra A we get the mapping

t_{A} : X^{A} → Y^{A}

as follows: 2 (x_{f})_{A}(v) = f ∘ v for v : A → X, 3 (t_{2} · t_{1})_{A} = (t_{2})_{A} ∘ (t_{1})_{A}.

An equation is a pair (t_{1}, t_{2}) of (X, Y)-ary terms. We write t_{1} = t_{2}. A Σ-coalgebra A satisfies this equation iff (t_{1})_{A} = (t_{2})_{A}. To emphasise that these equations are evaluated in coalgebras, we call them coequations. A coequational theory E is a class of coequations. The category of all Σ-coalgebras satisfying all coequations from E is denoted by ECoalg(E). It may be an illegitimate category. We are interested in legitimate categories ECoalg(E). Each such category is equipped with a forgetful functor U : ECoalg(E) → X and thus it is a concrete category.

Definition 2.4 (Coequational category). A concrete category will be called coequational if it is concretely isomorphic to ECoalg(E) for some coequational theory E.

In case that X has products, we can reduce the number of operations and equations needed for a coequational presentation if we add the possibility of forming new terms by pairing: 4 If I is a set and t_{i} are (X, Y_{i})-ary terms, i ∈ I, then

⟨t_{i}⟩

is an (X, ∏_{I} Y_{i})-ary term which is interpreted by a Σ-coalgebra A as

⟨t_{i}⟩_{A} = X^{A}  \overline{⟨(t_{i})_{A}⟩} ∏_{I}(Y_{i}^{A}) ≅ (∏_{I} Y_{i})^{A}

This will be convenient in the following examples. Note that we can avoid pairing by adding instead new operation symbols ⟨t_{i}⟩ to the signature and also, for all j ∈ I, new equations x_{p_{j}} · ⟨t_{i}⟩ = t_{j} where p_{j} : ∏_{I} Y_{i} → Y_{j} is the j-th projection.

Example 2.5. 1 Let X = Set and consider the signature Σ consisting of a single (2, 2)-ary operation

symbol □. Using clause (2) we have (2 × 2, 2)-ary terms p_{1}, p_{2}, ∧, → induced by the maps 2 × 2 → 2 known as first and second projection, conjunction and implication; similarly, for each set I, a (∏_{I} 2, 2)-ary term ⋀_{I}; denote ⋀_{∅} by true. Using clause (4) we obtain terms (p_{1} → p_{2}) → (□p_{1} → □p_{2}), □(p_{1} ∧ p_{2}) ↔ (□p_{1} ∧ □p_{2}), ⋀_{I} □p_{i} ↔ □ ⋀_{I} p_{i}. In the following examples equations t = true are abbreviated as t.

(a) ECoalg({(p_{1} → p_{2}) → (□p_{1} → □p_{2})}) is concretely isomorphic to the full subcategory of those (2^{2^{−}})-coalgebras g : A → 2^{2^{A}} for which g(a) is closed under supersets for all a ∈ A. These coalgebras are known in modal logic as monotone neighbourhood frames.

(b) ECoalg({□true, □(p_{1} ∧ p_{2}) ↔ (□p_{1} ∧ □p_{2})}) is concretely isomorphic to the full subcategory of those (2^{2^{−}})-coalgebras g : A → 2^{2^{A}} for which g(a) is closed under supersets and finite intersections for all a ∈ A. These coalgebras are also known as coalgebras for the filter functor (Gumm, 2001b) or as normal neighbourhood frames.

(c) The equations E = {□true, □(p_{1} ∧ p_{2}) ↔ (□p_{1} ∧ □p_{2}), □p_{1} → p_{1}, □p_{1} → □□p_{1}} are the usual axioms of an interior operator. ECoalg(E) is concretely isomorphic to the category of topological spaces with open and continuous maps as morphisms.

(d) ECoalg({⋀_{I} □p_{i} ↔ □ ⋀_{I} p_{i} | I a set }) is concretely isomorphic to the category of

Kripke frames, i.e. FCoalg(P). 2 If X is the category of Stone spaces (Johnstone, 1982), 2 the (discrete) two-

element Stone space, and Σ consists of a single (2, 2)-ary operation symbol □, then ECoalg({□true, □(p_{1}∧p_{2}) ↔ (□p_{1}∧□p_{2})}) is isomorphic to the category of descriptive general frames (Goldblatt, 1976).

We show that FCoalg(F) is always coequational. This result is due to Reiterman. His paper (Reiterman, 1983), p. 62, formulates it, without proof, over Set^{op} only (i.e. for algebras over Set) and thus we present Reiterman’s proof sent to the second author in the late 70s.

Proposition 2.6 (Reiterman). Let F : X → X be a functor. Then FCoalg(F) is coequational.

Proof. Let Σ be a signature consisting of (X, F X)-ary operation symbols σ^{X} for every set X and let E consist of coequations

σ^{Y} · x_{f} = x_{F f} · σ^{X}  (1)

for every mapping f : X → Y. There is a concrete functor G : FCoalg(F) → ECoalg(E) given as follows: For A = (A, α), G(A) is the E-coalgebra (A, σ_{GA}^{X}) where

σ_{GA}^{X}(v) = F v ∘ α

for v : A → X. On the other hand there is a concrete functor H : ECoalg(E) → FCoalg(F) sending an E-coalgebra A = (A, σ_{A}^{X}) to the F -coalgebra (A, σ_{A}^{A}(id_{A})).

We have HG = Id because, for each F -coalgebra A = (A, α) we have σ_{GA}^{A}(id_{A}) = F id_{A} ∘ α = α. Conversely, GH = Id because, for each E-coalgebra A = (A, σ_{A}^{X}), we have GHA = G(A, σ_{A}^{A}(id_{A})) = (A, F (−) ∘ σ_{A}^{A}(id_{A})) which equals (A, σ_{A}^{X}) because for all v : A → X

[figure: A^{A}; σ_{A}^{A}; (F A)^{A}; X^{A}; (x_{v})_{A}; σ_{A}^{X}; (F A)^{A}; (x_{F v})_{A}]

commutes (due to the coequation σ^{X} · x_{v} = x_{F v} · σ^{A}) and thus F v ∘ σ_{A}^{A}(id_{A}) = σ_{A}^{X}(v ∘ id_{A}) = σ_{A}^{X}(v).

The just described procedure needs a proper class of operation symbols. In case of X = Set, this can be avoided for functors preserving cofiltered limits if we exclude the existence of arbitrarily large measurable cardinals (which is consistent with ZFC). Recall that a measurable cardinal κ is a cardinal on which a non-principal κ-complete ultrafilter exists. An ultrafilter is κ-complete if it is closed under intersections of cardinality < κ and it is non-principal if it does not contain a singleton-set. Let (M) denote the following set-theoretic statement, (see (Adámek and Rosický, 1994) for more information).

(M) There do not exist arbitrarily large measurable cardinals.

Proposition 2.7. Assume (M) and let F : Set → Set be a functor preserving cofiltered limits. Then FCoalg(F) is coequational in a signature consisting of a single operation symbol.

Proof. Let P be an infinite set whose cardinality is greater than any measurable cardinal. Then the full subcategory P of Set having a single object P is codense in Set (see (Adámek and Rosický, 1994) A.5). Let Σ consist of a single (P, F P)-ary operation symbol σ and E consist of coequations (1) for f : P → P (where σ = σ^{P}). Analogously to Proposition 2.6 , we get a functor G : FCoalg(F) → ECoalg(E) and our task is to define H : ECoalg(E) → FCoalg(F). Let (A, σ_{A}) ∈ ECoalg(E). Since P is infinite, the commacategory (A↓P) is cofiltered (⟨u, v⟩ serves as a lower bound for u, v : A → P). The codensity of P means that f : A → P forms a limit cone to the projection Q : (A↓P) → Set. Since F preserves cofiltered limits, F f : F A → F P forms a limit cone to F Q. Coequations in E say that σ_{A}(f) : A → F P is a cone to F Q. Thus there is a unique mapping α : A → F A such that F f ∘ α = σ_{A}(f) for each f : A → P. We put HA = (A, α). The rest is analogous to Proposition 2.6.

Remark 2.8. 1 We can assume that there are no measurable cardinals. If V is a model of ZFC in

which measurable cardinals exist, let κ be the smallest such. Then V_{κ}, the restriction of V to sets of rank < κ, is a model of ZFC that contains no measurable cardinals.

2 If there are no measurable cardinals, we can take a countable set for P. 3 Since cofiltered limits are connected, Proposition 2.7 applies to polynomial functors

F : Set → Set.

We have seen that categories of coalgebras for a functor are coequational. But often, one is more interested in covarieties of these categories. Following (Manes, 1976), a full subcategory C of a coequational category (A, U) is called a covariety if C is closed under (existing) colimits, quotients and U-split subobjects. The last concept means a subobject m : A → B such that Um is a split monomorphism. Over Set covarieties correspond to the usual notion of full subcategories closed under coproducts, quotients and subobjects.

Most of the covarieties of coequational categories have cofree coalgebras. The forgetful functor is comonadic in these cases and therefore, following (Linton, 1969), coequational. We show that this easily follows from Reiterman’s proposition. Following (Mac Lane, 1971), we say that a concrete category (C, U) is comonadic if U has a right adjoint R and the canonical functor from C to the category of all coalgebras for the comonad UR is an isomorphism.

Proposition 2.9 (Linton). Every comonadic category is coequational.

Proof. Let F : X → X be a comonad with counit ε : F → Id and comultiplication δ : F → F F. Then coalgebras for the comonad F are specified in FCoalg(F) by

x_{ε_{X}} · σ^{X} = x_{id_{X}} ,
σ^{F X} · σ^{X} = x_{δ_{X}} · σ_{X}.

Moreover, comonadic categories coincide with coequational categories having cofree coalgebras. Let U : A → X be a functor. A U-split equaliser is an equaliser in A

[figure: A; e; B; f; g; C]

such that its U-image splits, i.e., it is equipped with t : UC → UB and s : UB → UA such that s ∘ Ue = id_{UA}, t ∘ Uf = id_{UB}, and t ∘ Ug = Ue ∘ s. U creates U-split equalisers if it creates equalisers of pairs f, g for which Uf, Ug has a split equaliser in X. Beck’s theorem (Mac Lane, 1971) says that U is comonadic iff it has a right-adjoint and creates U-split equalisers. We will say that a concrete category A is co-Beck if U creates colimits and U-split equalisers.

Proposition 2.10. Each covariety of a coequational category is co-Beck.

Proof. Straightforward, cf. (Rosický, 1981).

Corollary 2.11 (Linton). Every coequational category with cofree coalgebras is comonadic.

Proof. Follows from Proposition 2.10 and Beck’s theorem.

We have seen that every covariety (of a coequational category) with cofree coalgebras is coequational. Without this assumption this is an open problem.

Problem 2.12. Is every covariety in FCoalg(F), where F : Set → Set, coequational? More generally, is every covariety of a coequational category coequational?

Although important, the problem is not crucial for our approach. We will see in Section 4 that every covariety (of a coequational category over Set) can be defined by coequations in implicit operations.

3. Behavioural Equivalence

In case of algebras over Set, we think of operations as functions allowing to construct new elements of the carrier. We show that in case of coalgebras over Set, operations can be thought of as predicate transformers that respect behavioural equivalence. They will appear as modal operators in Section 5.

We first introduce a novel notion of behavioural equivalence. It formalises the idea that behavioural equivalence is the smallest equivalence relation that is invariant under morphisms. We define two notions, the second one taking ‘colourings’ into account: Given a functor U : A → Set and a set of ‘colours’ X, a colouring v for an object A ∈ A is a map UA → X.

Definition 3.1 (Behavioural Equivalence). Consider a functor U : A → Set. 1 ∼ is the smallest equivalence relation on the class of all pairs (A, a), A ∈ A, a ∈ UA,

satisfying

(A_{1}, a_{1}) ∼ (A_{2}, Uf(a_{1})) for all f : A_{1} → A_{2}.

2 Given X ∈ Set, ∼_{X} is the smallest equivalence relation on the class of all triples (A, v, a), A ∈ A, v : UA → X, a ∈ UA, satisfying

(A_{1}, v_{2} ∘ Uf, a_{1}) ∼_{X} (A_{2}, v_{2}, Uf(a_{1})) for all v_{2} : UA_{2} → X, f : A_{1} → A_{2}.

If (A, a) ∼ (B, b) we say that a and b are behaviourally equivalent. If (A, v, a) ∼_{X} (B, w, b) we say that a and b are X-behaviourally equivalent.

Categorically speaking, the equivalence classes of behavioural equivalence are the components of the category of elements of the forgetful functor; the equivalence classes of X-behavioural equivalence are the components of the category of elements of the functor (U↓X) → Set, (A, UA → X) ↦ UA.

Example 3.2. If A = FCoalg(F), F : Set → Set then (A, a) ∼ (B, b) iff a and b are identified by the morphisms into the final coalgebra. As it is well-known, this means that if F preserves weak pullbacks then (A, a) ∼ (B, b) iff a and b are related by a bisimulation in the sense of (Aczel and Mendler, 1989). In particular, in case of FCoalg(P) or FCoalg(P(− × L)), behavioural equivalence yields the familiar notion of bisimilarity for (labelled) transition systems.

The following gives an alternative characterisation of behavioural equivalence (the requirement on pushouts is satisfied by coequational categories).

Proposition 3.3. Suppose that A has pushouts and that U : A → Set preserves them. (A_{1}, v_{1}, a_{1}) ∼_{X} (A_{2}, v_{2}, a_{2}) iff there are B, w and morphisms f_{i} : A_{i} → B such that

\begin{aligned}& X \\ UA_{1} & \overline{Uf_{1}} & ^{v_{1}  \overline{}} & UB & ^{w} & Uf_{2} & UA_{2} & ^{\underline{}v_{2}} \end{aligned}  (2)

commutes and (Uf_{1})(a_{1}) = (Uf_{2})(a_{2}).

Proof. Let ≈ denote the relation defined by condition (2). ≈ ⊆ ∼ is immediate. For the converse, note that ≈ contains the generating pairs of ∼ and is reflexive and symmetric. ≈ is transitive, since A has pushouts and U preserves them.

An (X, Y)-valued predicate transformer P_{A} maps X-valued predicates to Y -valued predicates, that is, P_{A} : X^{UA} → Y^{UA}. It is called behavioural if it respects behavioural equivalence.

Definition 3.4 (Behavioural Predicate Transformers). Consider a functor U : A → Set. An (X, Y)-valued predicate transformer P is an operation which determines for each A ∈ A, v : UA → X, a ∈ UA a value

P_{A}(v, a) ∈ Y.  (3)

P is called a behavioural predicate transformer iff

(A, v, a) ∼_{X} (B, w, b) ⇒ P_{A}(v, a) = P_{B}(w, b)  (4)

for all w : UB → X and a ∈ UA. In case that X = 1 and Y = 2 we call P a behavioural predicate.

Note that behavioural predicates are precisely those predicates which are invariant under behavioural equivalence. The following is immediate from the respective definitions.

Lemma 3.5. An operation P which determines for each A ∈ A, v : UA → X, a ∈ UA a value P_{A}(v, a) ∈ Y is a behavioural predicate transformer iff

P_{A}(w ∘ Uf, a) = P_{B}(w, Uf(a)).  (5)

for all morphisms f : A → B, all w : UB → X, and all elements a of A.

We now show that invariance of a predicate transformer X^{U} → Y^{U} under Xbehavioural equivalence is equivalent to the naturality of X^{U} → Y^{U}.

Theorem 3.6. Consider a functor U : A → Set. An operation P which determines for each A ∈ A, v : UA → X, a ∈ UA a truth value P_{A}(v, a) ∈ Y is a behavioural predicate transformer iff

P_{A} : X^{UA} ⟶ Y^{UA}

is a natural transformation.

Proof. Naturality of P means that for any morphism f : A → B

[figure: X^{UA}; P_{A}; 2^{UA}; X^{UB}; X^{Uf}; P_{B}; 2^{UB}; 2^{Uf}]

commutes. Given w : UB → X and spelling out the definition of the vertical arrows we obtain P_{A}(w ∘ Uf) = P_{B}(w) ∘ Uf, i.e., P_{A}(w ∘ Uf, a) = P_{B}(w, Uf(a)) for all a ∈ UA, yielding condition (5) in Lemma 3.5.

The theorem is important to us for the following reasons. First, it gives an abstract characterisation of invariance under behavioural equivalence as a naturality condition. For example, for any functor F : Set → Set, the behavioural predicates of FCoalg(F) are precisely the natural transformations U → 2 where U : FCoalg(F) → Set is the forgetful functor. Similarly, modal operators can be characterised as natural transformations as explained in detail in Section 5.

Second, since every (X, Y)-ary operation of a signature for coalgebras gives rise to a natural transformation X^{U} → Y^{U}, it shows that, in case of coalgebras over Set, coalgebraic operations are predicate transformers that respect behavioural equivalence.

The next section is devoted to a detailed study of natural transformations X^{U} → Y^{U}.

4. Implicit Operations

In universal algebra, an implicit operation is a natural transformation A^{X} → A. If free algebras exist, each implicit operation is explicit (i.e. given by a term). If free algebras do not exist, implicit operations are more powerful. For example, in case of algebras over finite sets, (Reiterman, 1982) showed that every variety is definable by equations in implicit operations (but not by equations in explicit operations). This section shows how to define covarieties of coequational categories using implicit operations.

If Σ is a signature and U : SCoalg(Σ) → X the forgetful functor then each (X, Y)-ary operation symbol σ ∈ Σ determines a natural transformation

σ : X^{U} → Y^{U}

So does each (X, Y)-ary term. It leads us to define (X, Y)-ary implicit operations, for every functor U : A → X as natural transformations

X^{U} → Y^{U}.

Definition 4.1 (Coequations in Implicit Operations). Let U : A → X be a faithful functor and X, Y ∈ X. Having two (X, Y)-ary implicit operations σ_{1} and σ_{2} in A, we say that an object A ∈ A satisfies the coequation σ_{1} = σ_{2} and write A ⊧ σ_{1} = σ_{2} iff (σ_{1})_{A} = (σ_{2})_{A}.

Remark 4.2. 1 If the functor U has a right adjoint R then (X, Y)-ary implicit operations correspond

to natural transformations

A(−, RX) → A(−, RY),

i.e., to morphisms RX → RY. Consider implicit operations σ_{1}, σ_{2} represented by s_{1}, s_{2} : RX → RY, respectively. Then an object A satisfies the coequation σ_{1} = σ_{2} iff every morphism h : A → RX is equalised by s_{1} and s_{2}, i.e., iff h factors through an equaliser

[figure: S; RX; s_{1}; s_{2}; RY]

(provided that the latter exists). This notion of a coequation as a subobject S of a cofree object RX is a special case of (Manes, 1976), Theorem 3.4, page 227. It was further investigated in (Rutten, 2000; Gumm, 2001a; Roşu, 2001; Kurz, 2000; Hughes, 2001). Conversely, for any subobject S → RX, take the cokernel pair f, g : RX → A and compose it with η_{A} : A → RUA given by the unit η of the adjunction U ⊣ R. Then the pair η_{A} ∘ f, η_{A} ∘ g produces the pair of natural transformations X^{U} → Y^{U} in our sense. Thus, in the presence of cofree coalgebras, our approach is equivalent to the coequations-as-subobjects-of-cofree-objects approach.

2 Without cofree coalgebras, there are related concepts of a coequation in (Adámek and Porst, 2001) and (Reiterman, 1983). They are subsumed by coequations in implicit operations.

The following fact is a consequence of (Rosický, 1981, 5.3). Covarieties are defined on page 8.

Proposition 4.3. Suppose that U : A → X is coequational. Then, for a collection E of coequations in implicit operations, the full subcategory of all objects satisfying each coequation from E is a covariety in A.

Proof. The closedness under colimits is clear. If m : B → A is a U-split subobject of A, then X^{Um} : X^{UA} → X^{UB} is epi which yields closedness under U-split subobjects.

We now show that over Set the converse holds. This is a co-Birkhoff theorem not relying on the existence of cofree coalgebras. The proof uses certain implicit operations defined in terms of the behavioural equivalence relations ∼_{X} introduced in Definition 3.1.

Theorem 4.4. Let E be a coequational theory over Set. Then every covariety C in ECoalg(E) is definable by coequations in implicit operations.

Proof. For a set X and a E-coalgebra A, define

φ_{A}^{X} : X^{UA} → 2^{UA}

as follows: for v : UA → X and a ∈ UA, let φ_{A}^{X}(v)(a) = 1 iff there are C ∈ C, u : UC → X, c ∈ UC, such that (A, v, a) ∼_{X} (C, u, c), see Definition 3.1. φ^{X} is an implicit operation by Theorem 3.6.

Consider coequations

φ^{X} = true  (6)

where true is the implicit operation true_{A} : X^{UA} → 2^{UA} induced by the constant function X → 2, x ↦ 1. Each C ∈ C satisfies (6). Conversely, assume that A satisfies all coequations (6). Then, due to Proposition 3.3, for each a ∈ UA, there are B_{a} ∈ ECoalg(E), C_{a} ∈ C, and homomorphisms f_{a}, g_{a} and mappings w_{a}, u_{a} such that

\begin{matrix}UA \\ UA & \overline{Uf_{a}} & ^{id^{UA}} \overline{} & UB_{a} & ^{w_{a} } & Ug_{a} & UC_{a} & ^{\underline{}u_{a}} \end{matrix}

commutes and (Uf_{a})(a) ∈ (Ug_{a})(UC_{a}). Using a multiple pushout of the f_{a}

B  UA

we get

[figure: A; f_{a}; f; B_{a}; f′_{a}; UA; Uf; ^{id^{UA}}; UB; w; U(f′_{a} ∘ g_{a}); UC_{a}; u_{a}]

with (Uf)(UA) ⊆ ⋃{U(f′_{a} ∘g_{a})(UC_{a}) : a ∈ UA}. Note that ⋃{U(f′_{a} ∘g_{a})(UC_{a}) : a ∈ UA} is the carrier of an E-coalgebra which is in C due to closure under coproducts and quotients. Since f is injective and C is closed under subobjects, it follows A ∈ C.

Remark 4.5. 1 If ECoalg(E) has cofree coalgebras, the implicit operation φ^{X} is induced by a mor-

phism h : RX → R2, U ⊣ R, or, equivalently, by a mapping h̃ : URX → 2. Then, for v : UA → X,

φ_{A}^{X}(v) = h̃ ∘ Uv^{♯}

with v^{♯} : A → RX being the transpose of v. 2 Our proof works in the universe of finite sets, i.e., every covariety of finite coalgebras

is given by coequations in implicit operations. This is the “Reiterman Theorem” (Reiterman, 1982) for coalgebras.

3 Note that it does not follow from the theorem that C is coequational. Hence the theorem does not solve Problem 2.12. The reason is that the interpretations of implicit operations do not need to be coequationally determined by equations from E.

5. Modal Logic

We associate to each category A equipped with a functor U : A → Set a modal logic, called the internal modal language of A, and show that modal formulae and coequations have the same expressive power. Since coequations for coalgebras dualise equations for algebras this leads to a new formalisation of the statement that modal logic for coalgebras is dual to equational logic for algebras.

To start with, let us take a brief look at the classical modal logic of Kripke frames, see e.g. (Blackburn et al., 2001) for details. We denote by KF the category of Kripke frames and bounded morphisms (a bounded morphism is a function whose graph is a bisimulation), that is, KF = FCoalg(P). Writing U : KF → Set for the forgetful functor mapping Kripke frames to their carriers, the semantics [[φ]] of a modal formula φ in propositional variables {p_{i} | i ∈ I} can be understood as a KF-indexed class of operations

[[φ]]_{A} : (∏_{I} 2)^{UA} → 2^{UA}, A ∈ KF,

that is, each [[φ]]_{A} maps valuations v ∈ (∏_{I} 2)^{UA} and elements a ∈ UA to truth values [[φ]]_{A}(v, a) ∈ 2 = {0, 1}. A central feature of modal logic is that formulae are invariant under bisimulation. That is, for a modal formula φ and two Kripke models (A, v), (B, w), and a ∈ A, b ∈ B it holds

a, b bisimilar ⇒ [[φ]]_{A}(v, a) = [[φ]]_{B}(w, b)  (7)

But we have seen in Theorem 3.6 that (7) is equivalent to [[φ]]_{A} being natural in A. If we take invariance under bisimulation as the essence of modal logic it makes therefore sense to consider any natural transformation (∏_{I} 2)^{U} → 2^{U} as a modal operator and any category A equipped with a functor U : A → Set as a semantic domain for modal logic. This leads us to the following definition.

Definition 5.1. The internal modal language of a functor U : A → Set is given follows. For each set I and each i ∈ I the propositional variables p_{i}^{I} are I-ary formulae. For each natural transformation μ : (∏_{I} 2)^{U} ⟶ 2^{U} there is an I-ary modal operator □_{μ}. If φ_{i} are J-ary formulae, then □_{μ}⟨φ_{i}⟩ is a J-ary formula. The semantics of formulae is given by

[figure: [[□_{μ}⟨φ_{i}⟩]]; =; (∏_{J} 2)^{U}; ⟨[[φ_{i}]]⟩; ∏_{I}(2^{U}); ≅; (∏_{I} 2)^{U}; μ; 2^{U}.]

Given an I-ary formula φ and v : UA → ∏_{I} 2, we write A, v, a ⊧ φ iff [[φ]]_{A}(v, a) = 2 and A ⊧ φ iff [[φ]]_{A}(v) = UA for all v : UA → ∏_{I} 2. For 0-ary formulae we drop v from the notation.

Remark 5.2. 1 Behavioural equivalence is characterised by formulae of the language, that is, for each

A ∈ A and a ∈ UA there is a (0-ary) formula φ_{a} such that B, b ⊧ φ_{a} ⇔ a ∼ b. 2 The restriction of sets of colours to products of 2 allows for a notion of substitution

of formulae for propositional variables. As usual in categorical logic, the semantics of substitution is given by composition.

3 The basic calculus for this modal logic is given by the axioms of infinitary propositional logic plus the rule ‘from φ ↔ ψ derive □φ ↔ □ψ’ for each modal operator □. If, for example, □ is a normal modal operator, that is the axioms □true = true and □(p_{1} ∧ p_{2}) ↔ □p_{1} ∧ □p_{2} are added, then we obtain a calculus that is equivalent to the basic modal logic K.

4 The definition of the internal modal language makes sense not only over the category Set. For example, if we replace Set by the category of Stone spaces and let 2 be the discrete two-element space, then the continuity of the valuations v : UA → ∏_{I} 2 expresses that the extensions of the propositions p_{i} have to be admissible (i.e., clopen).

Example 5.3. The following examples illustrate our notion of modal operator as a natural transformation (∏_{I} 2)^{U} → 2^{U}. 1 An I-ary boolean operator is a modal operator f^{U} : (∏_{I} 2)^{U} ⟶ 2^{U} given by functions

f : ∏_{I} 2 → 2 as e.g. true, →, ⋀_{I}, compare Example 2.5. 2 Atomic propositions are 0-ary modal operators and are given by natural transforma-

tions 1 → 2^{U} (or also U → 2). 3 All commonly considered modal operators are examples. This includes non-normal

modal operators, polymodal operators, modal operators given by natural relations (Pattinson, 2001) or predicate liftings (Pattinson, ), and recursively defined modalities as in dynamic logic or the μ-calculus.

4 Examples of modalities which are not covered by Definition 5.1 can be obtained by definitions that require a ‘change of structure’. For instance, consider A = (A, α) ∈ FCoalg(P) and define

A, v, a ⊧ □(φ, ψ) = \{ \begin{matrix}A^{φ}, v^{φ}, a ⊧ ψ & if A, v, a ⊧ φ \\ true & otherwise \end{matrix}

where A^{φ} = (A^{φ}, α^{φ}) is given by A^{φ} = A \ \{a : A, v, a \begin{matrix}/ \\ ⊧ \end{matrix} φ\} and α^{φ}, v^{φ} are the restriction of α, v to A^{φ}. Modalities of this kind, often denoted by [!φ]ψ, arise in epistemic logic, see (Baltag et al., 1999).

We can now translate results about implicit operations into results about modal logic. For example, the following statement is a corollary of Theorem 4.4 and Remark 4.5.2. For its proof we just have to determine the modal language which is expressive enough to describe the formulas φ^{X} appearing in the proof of Theorem 4.4.

Proposition 5.4 (A Reiterman Theorem for Modal Logic). If a class K of finite Kripke frames is closed under finite coproducts, quotients and embeddings, then K is definable by a set {φ^{X} | X = 2^{n}, n ∈ ℕ} of formulae φ^{X}, each of which is a (countable) disjunction

φ^{X} = ⋁_{B∈K,w:B→X,b∈B} ψ^{(B,w,b)}

of finitary formulae ψ^{(B,w,b)}.

Finally, let us make precise the relationship between coequations in implicit operations and modal logic.

Proposition 5.5. Let U : A → Set be a functor. Coequations in implicit operations and formulae of the internal modal language have the same expressive power.

Proof. Each modal formula φ is logically equivalent to the coequation φ = true, which is to say that A ⊧ φ (Definition 5.1) iff A ⊧ φ = true (Definition 4.1) for all A ∈ A. Conversely, for a coequation t = s with t, s : X^{U} → Y^{U}, we find a set I and a surjective function e : ∏_{I} 2 → X and a modal formula t ∘ e ↔ s ∘ e : (∏_{I} 2)^{U} → 2^{U} such that A ⊧ t = s ⇔ A ⊧ t ∘ e ↔ s ∘ e for all A ∈ A.

Remark 5.6 (Duality of Modal and Equational Logic). Consider U : A → Set. A (coalgebraic) implicit operation for U is the same as an (algebraic) implicit operation for U^{op}. A^{op} ∈ A satisfies the (algebraic) equation σ_{1} = σ_{2} iff A satisfies the modal formula σ_{1} ↔ σ_{2}. A satisfies the modal formula φ iff A^{op} satisfies the equation φ = true.

6. Davis’s Theorem

We may allow signatures with (X, Y)-ary operation symbols where X and Y are classes. We call them meta-signatures. In the same way as signatures yield coequational categories, meta-signatures lead to meta-coequational categories. Every metacoequational category is co-Beck (page 8). (Davis, 1972) proved the converse. He overstated his result by claiming that every co-Beck category is coequational, which is not true as Example 6.3 shows. The second author observed Davis’s mistake in (Rosický, 1981); here we give a full explanation. First, we sketch an argument proving Davis’s theorem.

Theorem 6.1 (Davis). A concrete category is meta-coequational iff it is co-Beck.

Proof. Let U : C → Set create colimits and U-split equalisers. Let R : Class → Class be the density comonad of

Ū : C ⟶^{U} Set ↪ Class.

It means that RX is the colimit of the canonical diagram (Ū↓X) → Class

[figure: ŪA; v; X; RX; ε_{X}; c_{v}]

where ε_{X} is induced by the cone given by v’s. Since Ū creates colimits, (Ū↓X) is ∞-filtered (= every small subcategory of (Ū↓X) has an upper bound). Since the (illegitimate) category CCoalg(R) of coalgebras for the comonad R is coequational over Class, it suffices to prove that the image of the comparison functor

C  \overline{}CCoalg(R)

[figure: Class; V; Ū]

consists precisely of the R-coalgebras (X, ξ) with X a set. Any such coalgebra is given by a V -split equaliser

[figure: UB_{i}; UA_{i}; UC_{i}; RRX; \underline{Rξ}; \underline{δ_{X}}; RX; ξ; X; c_{i}]

where δ is the comultiplication. Since RRX and RX are given by ∞-filtered colimits, this equaliser is an ∞-filtered colimit of U-split equalisers in C (we are also using that U creates U-split equalisers). Since X is a set, some R-coalgebra homomorphism c_{i} : C_{i} → (X, ξ) splits, i.e., c_{i} ∘ s = id_{X} for some s : (X, ξ) → C_{i}. Hence (X, ξ) is isomorphic to some C-object.

Remark 6.2. Let C be a concrete category and σ : X^{U} → Y^{U} an implicit operation where X, Y are classes. Take mappings f : X_{1} → X and g : Y → Y_{1} where X_{1}, Y_{1} are sets. We get an implicit operation g^{U} ∘ σ ∘ f^{U} where arities are sets. If sets are codense in classes then Y is a canonical limit of the canonical diagram (Y ↓Set) → Class consisting of g : Y → Y_{1} where Y_{1} is a set. Hence, the implicit operation σ ∘ f^{U} is determined by implicit operations g^{U} ∘σ∘f^{U}. Moreover, since UC are sets, σ is determined by implicit operations g^{U} ∘ σ ∘ f^{U}. This is what Davis claimed. However, it does not mean that coequations of implicit operations whose arities are classes can be replaced by coequations of implicit operations whose arities are sets. There is a problem with compositions X^{U} ⟶^{σ_{1}} Z^{U} ⟶^{σ_{2}} Y^{U} where Z is a proper class. The precise result is Proposition 5.5 in (Rosický, 1981). As before (see the proof of Proposition 2.7), sets are codense in classes iff Ord is not measurable, i.e., iff each Ord-complete ultrafilter is principal. A model of such a set theory is V_{α} where α is inaccessible but not measurable. On the other hand, in the theory of finite sets, i.e., in V_{ω}, is Ord = ω measurable.

Example 6.3. Let Σ consist of a single (1, Ord)-ary operation symbol σ. Then Σcoalgebras A are sets A equipped with an operation σ_{A} : 1^{A} → Ord^{A}, i.e., with a mapping α : A → Ord. Homomorphisms h : (A, α) → (B, β) are mappings h : A → B such that β ∘h = α. SCoalg(Σ) is a (legitimate) meta-coequational category. It cannot be isomorphic to any full subcategory of FCoalg(F) for any functor F : Set → Set because it contains a proper class of one-element coalgebras. Each mapping f : Ord → m gives a (1, m)-ary term (i.e., a (1, m)-ary implicit operation) x_{f} · σ). In fact, every implicit operation φ : 1^{U} → m^{U} is of that kind. It suffices to take f : Ord → m given as f(p) = φ_{P}(id_{1}) where P is the one-element Σ-coalgebra with σ_{P} taking the value p (see (Rosický, 1981)7.2 for the easy calculation that φ = x_{f} · σ.) Let Σ_{1} be the collection of all (1, m)-ary operation symbols σ_{f}, f : Ord → m. Σ_{1} is not a signature because it is larger than a class. If Ord is not measurable then, following A. Kurz and J. Rosický 18

(Rosický, 1981)5.5, SCoalg(Σ) is described in Σ_{1} by coequations x_{g} · σ_{f} = σ_{g∘f}, for f : Ord → m and g : m → k. In fact, having a Σ_{1}-coalgebra (A, (σ_{f})_{A}) satisfying these equations, we get a cone (σ_{f})_{A} : A → m of the canonical diagram (Ord↓Set) and, therefore, the induced mapping α : A → Ord. (A, α) is the Σ-coalgebra determined by (A, (σ_{f})_{A}).

If Ord is measurable, then SCoalg(Σ) is not coequational. In fact, it is shown in (Rosický, 1981)7.2 that Ord-complete ultrafilters provide one-element coalgebras living in all coequational categories containing SCoalg(Σ).

References

Aczel, P. and Mendler, N. P. (1989). A final coalgebra theorem. In Pitt, D. H., Rydeheard, D. E., Dybjer, P., Pitts, A. M., and Poigné, A., editors, Category Theory and Computer Science, volume 389 of LNCS, pages 357–365. Springer.

Adámek, J. and Porst, H.-E. (2001). From varieties of algebras to covarieties of coalgebras. In Corradini, A., Lenisa, M., and Montanari, U., editors, Coalgebraic Methods in Computer Science (CMCS’01), volume 44.1 of ENTCS. Elsevier.

Adámek, J. and Rosický, J. (1994). Locally Presentable and Accessible Categories, volume 189

of London Mathematical Society Lecture Notes Series. Cambridge University Press. Adámek, J. and Trnková, V. (1990). Automata and Algebras in Categories. Kluwer Academic

Publishers. Baltag, A., Moss, L., and Solecki, S. (1999). The logic of public announcements, common

knowledge, and private suspicions. Technical Report SEN-R9922, CWI, Amsterdam. Blackburn, P., de Rijke, M., and Venema, Y. (2001). Modal Logic. Cambridge University Press. Davis, R. (1972). Quasi-cotripleable categories. Proceedings of the American Mathematical

Society, 35:43–38. Goldblatt, R. (1976). Metamathematics of modal logic I. Reports on Mathematical Logic, 6:41–

78. Gumm, H. P. (2001a). Equational and implicational classes of colgebras. Theoretical Computer

Science, 260. Gumm, H. P. (2001b). Functors for coalgebras. Algebra Universalis, 45:135–147. Hughes, J. (2001). A Study of Categories of Algebras and Coalgebras. PhD thesis, Carnegie

Mellon University, Pittsburgh. Johnstone, P. (1982). Stone Spaces. Cambridge University Press. Kurz, A. (2000). Logics for Coalgebras and Applications to Computer Science. PhD thesis,

Ludwig-Maximilians-Universität München. Linton, F. (1966). Some aspects of equational categories. In Eilenberg, S., Harrison, D., Lane,

S. M., and Röhrl, H., editors, Proceedings of the Conference on Categorical Algebra, La Jolla, 1965, pages 84–91. Springer.

Linton, F. (1969). An outline of functorial semantics. In Eckmann, B., editor, Seminar on triples and categorical homology theory, volume 80 of Lecture Notes in Mathematics, pages 7–52. Springer.

Mac Lane, S. (1971). Category Theory for the Working Mathematician. Springer. Manes, E. G. (1976). Algebraic Theories. Springer. Pattinson, D. Coalgebraic modal logic: Soundness, completeness and decidability of local con-

sequence. Theoretical Computer Science. To appear.

Operations and Equations for Coalgebras 19

Pattinson, D. (2001). Semantical principles in the modal logic of coalgebras. In Proceedings 18th International Symposium on Theoretical Aspects of Computer Science (STACS 2001), volume 2010 of LNCS, Berlin. Springer.

Reiterman, J. (1982). The Birkhoff theorem for finite algebras. Algebra Universalis, 14:1–10. Reiterman, J. (1983). Algebraic theories and varieties of functor algebras. Fundamenta Mathe-

maticae, 118:59–68. Roşu, G. (2001). Equational axiomatizability for coalgebra. Theoretical Computer Science,

260:229–247. Rosický, J. (1981). On algebraic categories. In Universal Algebra (Proc. Coll. Esztergom 1977),

volume 29 of Colloq. Math. Soc. J. Bolyai, pages 662–690. Rutten, J. (2000). Universal coalgebra: A theory of systems. Theoretical Computer Science,

249:3–80. Smyth, M. (1983). Power domains and predicate transformers: a topological view. In Diaz, J.,

editor, Proceedings 10th International Colloquium on Automata, Languages and Programming, volume 154 of LNCS, pages 662–675. Springer.