Working in a \(\mathbf {Pos}\) -enriched setting means that the syntax-building functor \(L^{\prime }:\mathbf {DL}\rightarrow \mathbf {DL}\)  and the coalgebra-building functor \(T^{\prime }:\mathbf {Pos}\rightarrow \mathbf {Pos}\)  will also need to be \(\mathbf {Pos}\) -enriched. The first main contributions of this paper is to show how well-known ordinary functors from BCL can be turned into \(\mathbf {Pos}\) -enriched functors performing analogous roles in PCL.
On the semantics side this means turning an ordinary functor \(T:\mathbf {Set}\rightarrow \mathbf {Set}\)  into a \(\mathbf {Pos}\) -enriched functor \(T^{\prime }:\mathbf {Pos}\rightarrow \mathbf {Pos}\)  by a process called posetification first developed in [1]}, for which we develop a practical understanding in Section  by computing the posetification of several well-known functors from modal logic: the neighbourhood, monotone neighbourhood, powerset and multiset functors. On the syntax side this means turning an ordinary functor \(L:\mathbf {BA}\rightarrow \mathbf {BA}\)  into a \(\mathbf {Pos}\) -enriched functor \(L^{\prime }:\mathbf {DL}\rightarrow \mathbf {DL}\) , a process which we call positivication and which is detailed in Section . We show how positivication can be applied to the functor defining normal modal logic, but also to functors which define non-monotone modal logics. In this case, the positivication procedure may not yield a logic at all, at least not in the usual meaning of the word. The second main contribution of this paper is to show how a semantic natural transformation \(\delta : L\mathsf {P}\rightarrow \mathsf {P}T\)  can also be lifted to define a \(\mathbf {Pos}\) -enriched semantic natural transformation \(\delta ^{\prime }: L^{\prime }\mathsf {P}^{\prime }\rightarrow \mathsf {P}^{\prime }T^{\prime }\) , where \(T^{\prime }\)  is the posetification of \(T\) , and \(L^{\prime }\)  is the positivication of \(L\) . This is done in Section , where we also prove that by construction of \(\delta ^{\prime }\) , if \(\delta \)  defines a weakly complete logic, then so does \(\delta ^{\prime }\) .
