The previous three chapters have introduced some basic elements of the theory of coalgebras, focusing on coalgebraic system descriptions, homomorphisms, behaviour, finality and bisimilarity. So far, only relatively simple coalgebras have been used, for inductively defined classes of polynomial functors, on the category Sets of sets and functions. This chapter will go beyond these polynomial functors and will consider other examples. But more important, it will follow a different, more systematic approach, relying not on the way functors are constructed but on the properties they satisfy – and work from there. Inevitably, this chapter will technically be more challenging, requiring more categorical maturity from the reader.

The chapter starts with a concrete description of two new functors, namely the multiset and distribution functors, written as M and D, respectively. As we shall see, on the one hand, from an abstract point of view, they are much like powerset P, but on the other hand they capture different kinds of computation: D is used for probabilistic computation and M for resourcesensitive computation.

Subsequently, Sections 4.2–4.5 will take a systematic look at relation lifting – used in the previous chapter to define bisimulation relations. Relation lifting will be described as a certain logical operation, which will be developed on the basis of a moderate amount of categorical logic, in terms of so-called factorisation systems. This will give rise to the notion of ‘logical bisimulation’ in Section 4.5. It is compared with several alternative formulations. For weak pullback-preserving functors on Sets these different formulations coincide. With this theory in place Section 4.6 concentrates on the existence of final coalgebras. Recall that earlier we skipped the proof of Theorem 2.3.9, claiming the existence of final coalgebras for finite Kripke polynomial functors. Here we present general existence results, for ‘bounded’ endofunctors on Sets. Finally, Section 4.7 contains another characterisation of simple polynomial functors in terms of size and preservation properties. It also contains a characterisation of more general ‘analytical’ functors, which includes for instance the multiset functor M.

Multiset and Distribution Functors

A set is a collection of elements. Such an element, if it occurs in the set, occurs only once. This sounds completely trivial. But one can imagine situations in which multiple occurrences of the same element can be relevant.