[Relation lifting, lax extension [1]}]

A relation lifting \(L\)  for a functor \(T\)  is an assignment
mapping every relation \(R \subseteq X\times Y\)  to a relation
\(LR \subseteq TX\times TY\)  such that converses are preserved:
\(L(S^\circ ) = (LS)^\circ  \) . A relation lifting \(L\)  is a lax
extension if for all relations \(R, R^{\prime } \subseteq X\times Z\) ,
\(S\subseteq Z\times Y\)  and functions \(f:X \rightarrow Z\) 
(identified with their graph relation) the following
hold:
\(R^{\prime } \subseteq R \Rightarrow LR^{\prime } \subseteq LR,\\LR;LS \subseteq L( R;S ),\\Tf \subseteq Lf.\) 
