Predicate and Relation Lifting for Parametric Algebraic Specifications

Relation lifting [6] extends an endofunctor F: C C to a functor Rel(F): Rel(C) Rel(C), where Rel(C) is a suitable category of relations over C. The relation lifting for the functor F can be used to define the notion of bisimulation for coalgebras X F (X). The related notion of predicate lifting can be used to define invariants for F-coalgebras. Predicate and relation lifting can be directly defined for a rich class of polynomial functors [5,6,19]. In this paper I investigate the case where the functor F is defined as the initial semantics of a (single sorted) parametric algebraic specification