# «A dissertation submitted in partial satisfaction of the requirements for the degree of Doctor of Philosophy in Electrical Engineering and Computer ...»

**Let π2 be a function from P to S deﬁned by the following mapping:**

0 → 0;

1, 1 → 1;

1, 2 → 2;

2, 1 → 1;

2, 2 → 2.

Then P, τ, together with π1 and π2, is a product of S, αS with itself in Pow-Coalg.

More generally, for every endofunctor F on class, all small products exist in F -Coalg (see [7, rem. 3.20]).

We are now ready to proceed with our promised example.

** Example 2.4.**

12. Let F be as in Example 2.3.3.

Call an F -coalgebra C, γ nameless if and only if for any c ∈ C,

The ﬁrst thing to notice about a nameless F -coalgebra C, γ is that if c1 and c2 are bisimilar in C, γ, and c2 and c3 are bisimilar in C, γ, then c1 and c3 are bisimilar in C, γ ; that is, bisimilarity in C, γ is a transitive concept, and thus, by Theorem 2.2.12, the largest bisimulation on C, γ is a bisimulation equivalence.

Let C, γ be a direct sum of all nameless F -coalgebras.

Clearly, C, γ is itself nameless. It is also weakly complete in F -Coalg. To see this, notice that every F -coalgebra C, γ is a homomorphic image of a nameless F -coalgebra C, γ such that

Weak completeness then follows from Theorem 2.2.10 and 2.4.9.

Let q be a quotient of C with respect to the largest bisimulation equivalence on C, γ.

By Proposition 2.3.1, there is exactly one F -coalgebra cod q, δ such that q is an epimorphism from C, γ to cod q, δ. And by an argument similar to that in ** Example 2.3.**

3, one can see that cod q, δ is also nameless. More importantly, cod q, δ is both weakly complete in F -Coalg, and strongly extensional. Weak completeness follows from weak completeness of C, f and Corollary 2.2.11, and strong extensionality by the straightforward observation that the inverse image of a bisimulation under a homomorphism from one nameless F -coalgebra to another is itself a bisimulation, which, by Theorem 2.3.2, is just a consequence of the fact that bisimilarity in a nameless F -coalgebra is transitive. However, cod q, δ is not ﬁnal in F -Coalg, lest it be isomorphic to S2, γ2, and thus, 0 and 1 bisimilar in S1, γ1 of Example 2.3.3.

This issue is just another manifestation of the aforementioned separation between the coalgebraic concepts of bisimulation and precongruence; had we used the latter to deﬁne the notion of strong extensionality, there would be no issue.

Fortunately, there is a simple way around this.

We say that C, γ is complete in F -Coalg if and only if for every F -coalgebra C, γ and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

** CHAPTER 2. TRANSITION SYSTEMS 41 By an easy corollary of Proposition 2.**

2.14, bisimilarity among L-labelled transition coalgebras is a transitive concept, and thus, an L-labelled transition coalgebra is both weakly complete in (Pow ◦ (L × Id))-Coalg, and strongly extensional, if and only if it is complete in (Pow ◦ (L × Id))-Coalg. Therefore, we may just as well forget about weak completeness and strong extensionality, and work with completeness instead, whose equivalence to ﬁnality generalizes nicely.

Apart from establishing this generalized equivalence, the following shows that when dealing

**with the two notions, one need only worry about coalgebras that are small:**

**Theorem 2.4.13. The following are equivalent:**

(a) C, γ is ﬁnal in F -Coalg;

(b) for every small F -coalgebra C, γ, there is exactly one homomorphism from C, γ to C, γ ;

(c) C, γ is complete in F -Coalg;

(d) for every small F -coalgebra C, γ, and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Proof. Trivially, (a) implies (b), and (c) implies (d). Therefore, it suﬃces to prove that (b) implies (c), and (d) implies (a).

Suppose that for every small F -coalgebra C, γ, there is exactly one homomorphism from C, γ to C, γ.

Assume an F -coalgebra C, γ.

Assume c ∈ C.

** By Lemma 2.4.**

8, there is a small F -coalgebra C, γ such that c ∈ C and C, γ ≤ C, γ. By hypothesis, there is exactly one homomorphism h from C, γ to C, γ.

Let R = (C → C )−1 ; h.

Then, by Theorem 2.2.10, R is a bisimulation between C, γ and C, γ. And clearly, c R h(c ). Thus, there is c ∈ C, namely h(c ), such that c and c are bisimilar among C, γ and C, γ.

Suppose, toward contradiction, that there are c1, c2 ∈ C such that c and c1 are bisimilar among C, γ and C, γ, c and c2 are bisimilar among C, γ and C, γ, and c1 = c2.

Then there are bisimulations B1 and B2 between C, γ and C, γ such that c B1 c1 and CHAPTER 2. TRANSITION SYSTEMS 42 c B2 c2. By Theorem 2.2.12, there is a bisimulation B between C, γ and C, γ such that

Clearly, B is a bisimulation between C, γ and C, γ.

By Theorem 2.4.5, there is a class function ρ : ran dpr B → F (ran dpr B ) such that

Since graph B, β is small, ran dpr B, ρ is small. Thus, by hypothesis, there is exactly one homomorphism h from ran dpr B, ρ to C, γ. Then both h ◦ π and cpr B are homomorphisms from graph B, β to C, γ. However,

Thus, by generalization, C, γ is complete in F -Coalg.

We have thereby proved that (b) implies (c). It remains to prove that (d) implies (a).

Suppose that for every for every small F -coalgebra C, γ, and any c ∈ C, there is exactly one c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Assume an F -coalgebra C, γ.

For every small subcoalgebra C, γ of C, γ, let h C,γ be a class function from C, γ to C, γ such that for any c ∈ C, h C,γ (c ) is the unique c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Let h be a binary class relation between C, γ and C, γ such that

Thus, there is a bisimulation B1 between C1, γ1 and C, γ such that c B1 c1, and a bisimulation B2 between C2, γ2 and C, γ such that c B2 c2. Now, by Theorem 2.4.6, there is a function υ : C1 ∪ C2 → F (C1 ∪ C2 ) such that

Thus, by generalization, h is a homomorphism from C, γ to C, f.

Suppose, toward contradiction, that there are homomorphisms h1 and h2 from C, γ to C, γ such that h1 = h2. Then there is c ∈ C such that

And by Lemma 2.4.8, there is a small F -coalgebra C, γ such that c ∈ C and C, γ ≤ C, γ. By Theorem 2.3.2, both h1 ◦ (C → C ) and h2 ◦ (C → C ) are bisimulations between C, γ to C, γ. Thus, c and h1 (c ) are bisimilar among C, γ and C, γ, and c and h2 (c ) are bisimilar among C, γ and C, γ, contrary to our hypothesis.

Therefore, there is at most one homomorphism from C, γ to C, γ.

Thus, there is exactly one homomorphism from C, γ to C, γ.

Thus, by generalization, C, γ is ﬁnal in F -Coalg.

The equivalence of (a) and (b) was already sketched by Aczel in [2], whereas the implication from (a) to (c) can be found in [23, thm. 6.4]. But the one in the reverse direction is, to our knowledge, a new result. Altogether, Theorem 2.4.13 is a powerful characterization of ﬁnal coalgebras, justifying their prominent role as semantic models of behaviour.

2.5 Existence of ﬁnal coalgebras At this point, there are two questions left for us to answer. First, is there a ﬁnal L-labelled transition coalgebra? And second, if there is one, is it a coalgebraic representation of an L-labelled transition system?

The answer to the ﬁrst question was already contained in the Final Coalgebra Theorem of [2], which has since been generalized to assert the existence of a ﬁnal coalgebra for every endofunctor on Class.

** Theorem 2.5.**

1. There is an F -coalgebra that is ﬁnal in F -Coalg.

Proof. See [5, thm. 2.1] and [7, thm. 2.2].

By now, there have been several diﬀerent proofs of Theorem 2.5.1 (see [7] and references therein). Assuming [7, thm. 2.2], or equivalently, Lemma 2.4.8, the proof in [5] is perhaps the most elementary, and surely the most natural from the non-category-theorist point of view. It amounts to forming a direct sum of all small F -coalgebras, and constructing a CHAPTER 2. TRANSITION SYSTEMS 46 quotient of it with respect to the largest congruence on it, or equivalently in this case, the equivalence class relation generated by the largest bisimulation on it.

** Note 2.5.**

1. In [5], Aczel and Mendler constructed the quotient of a coproduct of all small coalgebras with respect to the largest congruence on it, which, by Proposition 2.3.3.2, is also the largest precongruence on it. That we can use the equivalence class relation generated by the largest bisimulation on it instead is not entirely obvious, but nevertheless, true.

Proposition 2.5.1.1. If for every small F -coalgebra C, γ, there is a homomorphism

**from C, γ to C, γ, then for every c1, c2 ∈ C, the following are equivalent:**

(a) c1 and c2 are congruent in C, γ ;

Assume c ∈ C.

Since C, γ is small, ran(q ◦ (C → C)), ρ is small. Thus, by hypothesis, there is a homomorphism h from ran(q ◦ (C → C)), ρ to C, γ.

Let B = (C → C)−1 ;(h ◦ h).

Then, by Theorem 2.2.10, both B and B −1 are bisimulations on C, γ. And clearly, c1 B h (h(c1 )) and h (h(c2 )) B −1 c2. However, h(c1 ) = h(c2 ), and hence, h (h(c1 )) = h (h(c2 )). Thus, there is c ∈ C, namely h (h(c1 )), such that c1 and c are bisimilar in C, γ, and c and c2 are bisimilar in C, γ.

Conversely, suppose that there is c ∈ C such that c1 and c are bisimilar in C, γ, and c and c2 are bisimilar in C, γ.

Then, by [5, prop. 6.1], c1 and c are congruent in C, γ, and c and c2 are congruent in C, γ. Thus, by [23, lem. 4.16] there is a congruence P on C, γ such that c1 P c and c P c2, and hence, c1 P c2. Thus, c1 and c2 are congruent in C, γ.

Thus, by generalization, (a) and (b) are equivalent.

By [5, lem. 4.3], there is a largest congruence, and by [56, cor. 5.6], a largest bisimulation on C, γ. What Proposition 2.5.1.1 then implies is that if for every small F -coalgebra C, γ, there is a homomorphism from C, γ to C, γ, as is the case with any coproduct of all small F -coalgebras, then the largest congruence on C, γ coincides with the equivalence class relation generated by the largest bisimulation on C, γ.

Note that according to Rutten, for every F -coalgebra, the largest bisimulation on it is an equivalence class relation (see [56, cor. 5.6]). This is false. For an easy counterexample, consider the direct sum of the F -coalgebras S1, γ1 and S2, γ2 of Example 2.3.3.

We could also forgo some of the generality of Theorem 2.5.1, in favour of an even simpler ﬁnal coalgebra construction, one that would be, for instance, more amenable to formal reasoning.

For example, if we assume that F is an ωop -continuous endofunctor on Class, namely one that preserves limits of ωop -indexed diagrams in Class, and let 1 be a terminal object of Class, or equivalently, a set with just one member, and ! the unique class function from F (1) to 1, then we can fashion a ﬁnal F -coalgebra out of a limit of the following diagram (see [60, lem.

**2]):**

CHAPTER 2. TRANSITION SYSTEMS 48 F (!) F (F (!)) !

··· 1 F (1) F (F (1)) Another, fascinating example is The Special Final Coalgebra Theorem of [2], which, under the hypothesis of a universe of sets that need not be well founded, asserts that if F preserves inclusion maps, and is uniform on maps, a condition capturing the informal idea of an endofunctor whose action on class functions is completely determined by its action on classes, then the largest ﬁxed point of the object part of F, which is readily obtained, in this case, as

together with the identity map on it, is a ﬁnal F -coalgebra.

All the same, it is only the existence of a ﬁnal F -coalgebra that will be of any interest to us here.

The answer to the second question is suggested by Lambek’s Lemma.

Proposition 2.5.2. If C, γ is ﬁnal in F -Coalg, then γ is bijective.

Proof. See [33, lem. 2.2].

If C, τ is ﬁnal in (Pow ◦ (L × Id))-Coalg, then τ is a bijective class function from C to Pow(L × C), which, for obvious cardinality reasons, is possible only if C is a proper class.

Thus, even though there is a ﬁnal L-labelled transition coalgebra, it, being large, cannot be a coalgebraic representation of an L-labelled transition system, and consequently, there is no L-labelled transition system satisfying both conditions of our enquiry.

Although perhaps disconcerting, this is not something that should come as a complete surprise. Having left the cardinality of the branching degree of a state in a system unchecked, it is only reasonable to expect that the diﬀerent types of branching structure be too many to collect inside a set. One could, for example, bound, in a suitable sense, the endofunctor F, to ensure that a ﬁnal coalgebra be small (see [31, cor. 3.3]). In the case of Pow ◦ (L × Id), this would correspond to bounding that branching degree cardinality, and for a model of process behaviour, this may or may not be a natural thing to do. But in the case of Pow, and for a model of a theory of sets, for example, it is deﬁnitely not.