(draft)
Extending a functor from functions to relations is important to coalgebra for at least two reasons. Relation lifting can be used to define bisimulations and also to define Moss's coalgebraic logic. In the latter case, the idea is to apply the lifted functor to the satisfiability relation.
Relation lifting can be defined in at least two ways, via spans and via cospans. In both cases the idea is to first represent a relation by a pair of arrows, and then to apply the functor to these arrows.
In the following let be the category which has sets as objects and relations as arrows.
The idea of the span-based relation lifting of a functor is to "tabulate" a relation by a span and then to apply the functor to the projections, obtaining .
Definition: Let and be a relation. Then
is the relation given by
Remark: This formulation is specific to set-functors, but can be generalised to other base categories.
Fact: preserves composition (and therefore is a functor on ) if preserves weak-pullbacks.
Example/Exercise: Let be the powerset functor. It is an interesting exercise to check that iff
Fact: is a functor. If is a partial order then is a partial order.
The cospan-based relation lifting starts from the cotabulation (or collage) of a relation by a cospan , where is an order on the disjoint union given by iff or or .
Thus, in order to apply a set-functor to and , we need extend from sets to orders. This follows the same idea as the relation lifting in the previous section, but now one closes under reflexivity and transitivity (and quotients by anti-symmetry in the case one works with posets).
Definition: Let be a pre-order. Write for the two projections. Then has carrier and the order on
is the smallest order containing
This defines a functor
where can be preorders or posets.
Remark: The surjection has a universal property as the universal solution to the inequation to . Category theoretically, we can say that is the coinserter of and also that is the (order-enriched) left Kan extension of along where is the embedding of sets into (discrete) ordered sets.
The following fact allows us to use known results about the span-based relation lifting to compute the order-extension of a set-functor in many examples.
Fact: If preserves weak pullbacks, then applying to a preorder agrees with applying the relation lifting to .
Example: Let be a preorder. For subsets we have iff
In domain theory, this is also known as the Egli-Milner order. When restricted to convex subsets (and modified wrt the empty subset) is known as the Plotkin powerdomain. See also my review of powerdomains.
To cotabulate a relation by a cospan
we need to recall the collage of a relation . This notion can also be defined in case and are ordered sets and is weakening-closed, that is,
We give the more general definition, because it shows that the cospan-based relation lifting cannot only be used to extend set-functors but also ordered functors.
If is a weakening relation, then the collage is an order on the disjoint union such that if (i) in or (ii) or (iii) in .
Given a functor , [1] we can use the collage to give a cospan-based definition of relation lifting.
Definition: Let . Then
is defined if in .
Fact: If preserves weak pullbacks then .
The span-based relation lifting can be generalised to ordered sets an is well-behaved if the functor preserves weak pullbacks.
The cospan-based relation lifting is ineherently order enriched, but can be applied to the discrete case if we extend the functor to ordered sets.
One application of relation lifting is to define coalgebraic bisimulation. Here the span-based and the cospan-based definition agree if the functor preserves weak pullbacks, but in general it is only cospan bisimilarity that captures coalgebraic behavioural equivalence/preorder.
The cospan-based relation lifting generalises from ordered sets to Lawvere metric spaces and other categories enriched over a quantale.
References can be found in the survey article
(or a functor on preorders or posets) ↩︎