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

8, there is a small F -coalgebra C, γ such that c ∈ C and C, γ ≤ C, γ. And by hypothesis, there is a 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, γ.

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

However, an F -coalgebra that is weakly complete in our sense need not be weakly complete in the sense of [2], [5], and [3].

** Example 2.4.**

1.2. Consider the left product endofunctor ω × Id, which assigns to every class C the class ω × C = { n, c | n ∈ ω and c ∈ C}, and to every class function f : C1 → C2, a class function ω × f : ω × C1 → ω × C2 such that for any n, c ∈ C1, (ω × f )( n, c ) = n, f (c).

Let C = { s, tailn s | s ∈ S inf ω and n ∈ ω}, and γ be a function from C to ω × C such that for any s, tailn s ∈ C, γ( s, tailn s ) = head tailn s, s, tailn+1 s.

then, by an easy induction, it is the only such inﬁnite sequence, and c and s, s are bisimilar in C, γ and C, γ. Thus, C, γ is weakly complete in (ω × Id)-Coalg.

Now let C be the set of all integers, and γ a function from C to ω × C such that for any integer i,

C, γ is a small (ω × Id)-coalgebra. However, there is no homomorphism from C, γ to C, γ, lest there be an order-embedding from the standardly ordered set of all integers to the standardly ordered set of all natural numbers.

Also, an F -coalgebra that is weakly complete in the sense of [2], [5], and [3] need not be weakly ﬁnal in F -Coalg.

** Example 2.4.**

1.3. Let C, γ be a direct sum of all small Pow-coalgebras.

Then for every small Pow-coalgebra C, γ, there is a homomorphism from C, γ to C, γ, namely the canonical injection map from C to C.

Let Ord be the class of all ordinal numbers, and a class function from Ord to Pow Ord such that for every ordinal number α, (α) = {β | β α}.

Then, by an easy transﬁnite induction argument, for every Pow-coalgebra C, γ, any homomorphism from Ord, to C, γ is injective. Also, again by an easy transﬁnite induction argument, if h is homomorphism from Ord, to C, γ, there is a small Pow-coalgebra C, γ such that if ι is the canonical injection map from C to C, then ran h ⊆ ran ι. Thus, there is no homomorphism from Ord, to C, γ, lest there be an injective class function from the class of all ordinal numbers to a set, and hence, C, γ is not weakly ﬁnal in Pow-Coalg.

**The following is immediate from Theorem 2.3.2:**

Proposition 2.4.1. If C, γ is ﬁnal in F -Coalg, then C, γ is weakly complete in F -Coalg.

two conditions of our enquiry. The one introduced next is meant as a coalgebraic generalization of the second.

We say that C, γ is strongly extensional if and only if for every c1, c2 ∈ C, c1 = c2 if and only if c1 and c2 are bisimilar in C, γ.

We use the term “strongly extensional” here in the same way that Rutten and Turi did in [57]. This choice of term was suggested by the special case of Pow, where it was used quite literally, in reference to a stronger form of the Axiom of Extensionality, one better suited to a theory of sets that need not be well founded (see [2]). All other uses of it in [2], [5], and [3] are ultimately equivalent to that in [57].

** Note 2.4.**

2. In [2] and [5], an F -coalgebra C, γ was called “strongly extensional” if and only if for every small F -coalgebra C, γ, there is at most one homomorphism from C, γ to C, γ, whereas in [3], if and only if for every F -coalgebra C, γ, there is at most one homomorphism from C, γ to C, γ. All three notions coincide.

**Proposition 2.4.2.1. The following are equivalent:**

(a) C, γ is strongly extensional;

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

(c) for every small F -coalgebra C, γ, there is at most one homomorphism from C, γ to C, γ.

contrary to our hypothesis.

Therefore, for every F -coalgebra C, γ, there is at most one homomorphism from C, γ to C, γ.

** Theorem 2.4.**

2. If C, γ is ﬁnal in F -Coalg, then C, γ is strongly extensional.

Proof. See [57, thm. 2.4].

** Theorem 2.4.**

2 is equivalent to the statement that any ﬁnal F -coalgebra C, γ satisﬁes what is now known as the coinduction proof principle, whereby for every c1, c2 ∈ C, in order to prove that c1 = c2, one need only ﬁnd a bisimulation B on C, γ such that c1 B c2 (see [56, thm. 9.2]).

** Note 2.4.**

3. The coinduction proof principle applies to every simple F -coalgebra, namely every F -coalgebra that has no proper quotient, or equivalently, every F -coalgebra C, γ such that for every F -coalgebra C, γ, if h is an epimorphism from C, γ to C, γ, then h is an isomorphism between C, γ to C, γ.

Dually, the induction proof principle applies to every minimal F -algebra, namely every F -algebra that has no proper subalgebra, or equivalently, every F -algebra C, α such that for every F -algebra C, α, if h is a monomorphism from C, α to C, α, then h is an isomorphism between C, α to C, α.

These statements appear explicitly in [57, sec. 6.3], which is, apparently, where the term “coinduction” was used for the ﬁrst time in this coalgebraic setting.

By [23, lem. 4.12], an F -coalgebra C, γ is simple, in the above sense, if and only if for any c1, c2 ∈ C, c1 = c2 if and only if c1 and c2 are congruent in C, γ.

Note that in [23], an F -coalgebra C, γ is called simple if and only if it satisﬁes the coinduction proof principle (see [23, def. 6.12]).

Now, by Proposition 2.2.15 and 2.4.1, and Theorem 2.4.2, any system having a coalgebraic representation that is ﬁnal in (Pow ◦ (L × Id))-Coalg will satisfy both conditions of our enquiry. So if we can prove that the converse is also true, then we need look no further.

Before attempting such a proof, there is a small issue that we need to resolve regarding the ﬁrst of these conditions and our coalgebraic generalization of it. By Proposition 2.2.1(b), CHAPTER 2. TRANSITION SYSTEMS 34 2.2.13, and 2.2.15, the former is equivalent to the statement, “for every small L-labelled transition coalgebra C, τ and any c ∈ C, there is s ∈ S such that c and s are bisimilar among C, τ and S, fun T ”. Because of the term “small” in the ﬁrst quantiﬁer of this statement, saying that S, fun T is weakly complete in (Pow ◦ (L × Id))-Coalg seems to impose a much stronger constraint on the system S, T. Whether this is in fact a stronger constraint is really a matter of whether an increase in the size of the carrier beyond that of a set can bring about new kinds of behaviour in a labelled transition coalgebra.

In [5], Aczel and Mendler introduced a general condition meant precisely to guard against this type of possibility. They called F set-based if and only if for every class C and any c ∈ F (C), there is a subset S of C, and s ∈ F (S), such that c = F (S → C)(s).14 Now, it is quite obvious that Pow ◦ (L × Id) is set-based. What is not so obvious is that, actually, every endofunctor on Class is set-based. Adamek, Milius, and Velebil proved this surprising fact in [7] for the standard set-theoretic model of Class, using a classical result from combinatorial set theory, but the same ideas extend to other models of Class (for example, see [15]).

Here, we will be using this fact under the guise of The Small Subcoalgebra Lemma of [5].

For example, if S, T is a transition system, and S, γ a subcoalgebra of S, fun T, then S is a set of states of S, T that is closed under the transition relation of S, T, and rel γ is the restriction of that transition relation onto that set of states.

As one might expect, the cooperation of a subcoalgebra is uniquely determined by its carrier.

Proposition 2.4.4. If C1, γ1 ≤ C, γ, C2, γ2 ≤ C, γ, and C1 = C2, then γ1 = γ2.

Proof. See [56, prop. 6.1].

**The following can be used as criteria for choosing an eligible carrier:**

** Theorem 2.4.**

5. If h is a homomorphism from C1, γ1 to C2, γ2, then there is a class function ρ : ran h → F (ran h) such that

Proof. See [56, thm. 6.3].

** Theorem 2.4.**

6. For every class-indexed family { Ci, γi }i∈I of subcoalgebras of C, γ, there is a class function υ : i∈I Ci → F ( i∈I Ci ) such that

Proof. See [23, thm. 4.7].

Finally, every homomorphism factorizes, in a unique fashion, through every subcoalgebra of its codomain F -coalgebra that contains its range.

Proposition 2.4.7. If h is a homomorphism from C1, γ1 to C2, γ2, and C, γ is a subcoalgebra of C2, γ2 such that ran h ⊆ C, then there is exactly one homomorphism h from C1, γ1 to C, γ such that

Thus, if h, C1, γ1, C2, γ2, and C, γ are as in Proposition 2.4.7, then there is exactly

**one homomorphism h from C1, γ1 to C, γ such that the following diagram commutes:**

** Theorem 2.4.**

6 and Proposition 2.4.7 can be used to arrange the subcoalgebras of an F -coalgebra into a complete lattice (see [23, cor. 4.9]).

The Small Subcoalgebra Lemma was a key lemma in [5], and will be a key lemma here as well.

** Lemma 2.4.**

8. For every subset S of C, there is a small F -coalgebra C, γ such that S ⊆ C and C, γ ≤ C, γ.

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

Our ﬁst use of it is in resolving our last issue.

** Theorem 2.4.**

9. C, γ is weakly complete in F -Coalg if and only if for every small F -coalgebra C, γ and any c ∈ C, there is c ∈ C such that c and c are bisimilar among C, γ and C, γ.

Then, by Corollary 2.2.11, R is a bisimulation between C, γ and C, γ. And clearly, c R c. Thus, c and c are bisimilar among C, γ and C, γ.

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

By Proposition 2.2.1(b), 2.2.13, and 2.2.14, and Theorem 2.4.9, an L-labelled transition system S, T will satisfy the ﬁrst condition of our enquiry if and only if S, fun T is weakly complete in (Pow ◦ (L × Id))-Coalg, and by Proposition 2.2.14, it will satisfy the second if and only if S, fun T is strongly extensional. We are thus left with the problem of proving that if S, fun T is both weakly complete in (Pow ◦ (L × Id))-Coalg, and strongly extensional, then it is ﬁnal in (Pow ◦ (L × Id))-Coalg.

Although it is indeed possible to prove this, such proof does not generalize as one might expect: weak completeness and strong extensionality do not, in general, imply ﬁnality. But before we see an example attesting to this claim, we need to introduce a simple coalgebra construction that generalizes the notion of disjoint union, allowing us to merge diﬀerent coalgebras into a single whole.

Assume a class-indexed family { Ci, γi }i∈I of F -coalgebras.

Deﬁnition 2.4.10. The direct sum of { Ci, γi }i∈I is an F -coalgebra C, γ such that the

**following are true:**

(a) C is the disjoint union16 of {Ci }i∈I ;

(b) γ is a class function from C to F (C) such that for any j ∈ I and any c ∈ Cj,

Proposition 2.4.11. For every class-indexed family {hi }i∈I such that for any i ∈ I, hi is a homomorphism from Ci, γi to C, γ, there is exactly one homomorphism h from i∈I Ci, γi to C, γ such that for any j ∈ I,

Proof. See [23, lem. 4.1].

Thus, for every F -coalgebra C, γ and class-indexed family {hi }i∈I such that for any i ∈ I, hi is a homomorphism from Ci, γi to C, γ, there is exactly one mediating

**homomorphism h from i∈I Ci, γi to C, γ such that the following diagram commutes:**

The disjoint sum construction is one particular instance of the more abstract category-theoretic concept of coproduct, which is deﬁned by use of the property of Proposition 2.4.11, only generalized to a category of arbitrary objects and arrows. Another is the disjoint union construction.

**Note 2.4.4. What about the concept of product?In [55, p. 5], Rutten writes the following:**

The direct sum (or coproduct) of any collection of transition systems consists of the disjoint union of their carriers together with (the transition structure determined by) the disjoint union of their transition relations. In general, the product (in the category of transition systems) of two transition systems need not exist. For instance, let S = {0, 1, 2} with αS (0) = {0, 1}, and αS (1) = αS (2) = ∅. There does not exist a product of S, αS with itself.

Let P = {0, 1, 1, 1, 2, 2, 1, 2, 2 }, and τ be a class function from P to Pow P deﬁned

**by the following mapping:**

0 → {0, 1, 1 };

1, 1 → ∅;

1, 2 → ∅;

2, 1 → ∅;

2, 2 → ∅.

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

0 → 0;

1, 1 → 1;

1, 2 → 1;

2, 1 → 2;

2, 2 → 2.