Part of a presentation on Coalgebras over Lawvere Metric Spaces

Coalgebras over Sets

Given a functor

$T:\mathcal{X}\to \mathcal{X}$, the category

$Coalg(T)$ of

$T$-coalgebras

$X\to TX$ has as morphisms

$f:(X\stackrel{\xi }{\to }TX)\to (Y\stackrel{\nu }{\to }TY)$ the arrows

$f:X\to Y$ such that

$Tf\circ \xi =\nu \circ f$.

Intuitively,

$T$ describes the type of possible one-step behaviours of a dynamical system

$\xi :X\to TX$. In particular, for

$\mathcal{X}=Set$, we think of

$\xi (x)$ as the one-step behaviour of the dynamical system in state

$x$. Coalgebra morphisms preserve one-step (and hence 'global', 'ongoing') behaviours.

More generally, if

$\mathcal{X}$ has a forgetful functor to

$Set$ it makes sense to speak of 'states'

$x\in X$. In such a situation we can define behavioural equivalence as the smallest relation

$$x\sim y$$

on states that contains pairs

$x\sim f(x)$ where

$x$ ranges over all states of all coalgebras and

$f$ ranges over all coalgebra morphisms.

A final coalgebra

$(Z,\zeta )$ has the property that for every coalgebra

$(X,\xi )$ there is a unique coalgebra morphism

$!:X\to Z$.

Fact (Aczel and Mendler, 1989): For

$\mathcal{X}=Set$, if we admit proper classes as carriers, the final coalgebra exists for all functors

$T$. Moreover,

$x\sim y\iff !(x)=!(y)$.

Intuitively, elements of the final coalgebra classify behaviours of coalgebras. Another way to look at this is to think of final coalgebras as the canonical solutions, up to behavioural equivalence, of the 'domain equation'

$X\cong TX$.

What is the notion of behaviour that can be captured in this way?

Behavioural Equivalence via Bisimulations: The definition of behavioural equivalence quantifies over the proper class of all coalgebras. Importantly, for a large class of functors (including but not limited to the weakly pullback preserving ones) one can give a "local" charactersiation in terms of bisimulations: Two states

$x,y$ are behaviourally equivalent (or bisimilar) iff there is a bisimulation

$R$ such

$xRy$.

We will not dicuss here how to define bisimulation parametrically in

$T$. Instead, we only recall the well-known case

$T=\mathcal{P}$:

Example (Aczel, 1988): For

$\mathcal{C}=Set$ and

$T=\mathcal{P}$ the powerset functor, and two states

$x,y$ in two coalgebras

$\xi :X\to TX$ and

$\nu :Y\to TY$, we have that

$x\sim y$ iff there is a relation

$R$ with

$xRy$ satisfying

$$\begin{array}{c}\mathrm{\forall }{x}^{\prime }\in \xi (x).\mathrm{\exists }{y}^{\prime }\in \nu (y).x^{\prime }R{y}^{\prime }\\ \text{ and }\\ \mathrm{\forall }{y}^{\prime }\in \nu (y).\mathrm{\exists }{x}^{\prime }\in \xi (x).x^{\prime }R{y}^{\prime }\end{array}$$

Activity: Draw pictures of bisimulations. Make examples.

Remark: If you have not seen bisimulations before, the two clauses above should explain the terminology bi-simulation.

Summary: I only presented the most paradigmatic example, but, importantly, the above themes can be developed parametrically in the functor

$T:Set\to Set$.