Since coalgebras serve as generic
models of reactive systems, it is natural to specify properties of
coalgebras in terms of suitable modalities. The semantics of
coalgebraic modalities can be defined using predicate
liftings [1]}, [2]}, which specify
how a predicate on a base set \(X\)  induces a predicate on the set \(TX\) 
where \(T\)  is the coalgebraic type functor:
