Predicate Liftings Versus Nabla Modalities

We compare Moss' language and languages with predicate liftings. We prove that every monadic predicate lifting for a Kripke polynomial functor can be translated into Moss' language. We also prove that Moss' modality can always be translated into an appropriate language with predicate liftings.