Incidentally, this also means that for finitary functors the
existence of a separating set of monotone predicate liftings is
equivalent to the existence of a strongly expressive set of monotone
singleton-preserving predicate liftings. The right-to-left
implication is trivial; the converse follows from prop:laxdescrpres,
prop:moss-strong-expr,
and the fact that for finitary functors the existence of a separating set of monotone
predicate liftings is equivalent to the existence of a lax extension
[1]}.

We have thus seen that given a fixed diagonal-preserving lax extension, from every natural
transformation \(\tau : (-)^n \rightarrow T\)  we obtain the corresponding Moss
lifting \(\lambda  ^\tau /n\) , which is a monotone singleton-preserving
predicate lifting. Conversely, every monotone singleton-preserving
predicate lifting \(\lambda  \)  yields a natural transformation
\(\tau  ^\lambda : (-)^n \rightarrow T\) 
(lem:pres.REF ). From
prop:laxdescrpres, it is immediate that for
\(\tau : (-)^n \rightarrow T\)  we have
\(\tau  = \tau  ^{(\lambda  ^\tau )}.\) 
