where \(\mathsf {S^{\prime }}\)  is the functor sending a distributive lattice to the poset of its prime filters, and \(\mathsf {P}^{\prime }\)  is the functor sending a poset to the distributive lattice of its upsets. The following observation will be of fundamental importance in what follows: the adjunction \(\mathsf {S^{\prime }}\dashv \mathsf {P}^{\prime }: \mathbf {Pos}^{\mathrm {op}}\rightarrow \mathbf {DL}\)  which is the backbone of diagram (REF ) is in fact \(\mathbf {Pos}\) -enriched; that is to say \(\mathbf {DL}\)  and \(\mathbf {Pos}\)  are \(\mathbf {Pos}\) -enriched categories and \(\mathsf {S^{\prime }},\mathsf {P}^{\prime }\)  are \(\mathbf {Pos}\) -enriched functors ([1]}). Clearly, it would be a shame not to use this extra structure which comes for free. But more seriously, this enriched structure is not simply a mathematical quirk, it suggests that `doing logic' positively is quite different from `doing logic' in a boolean setting, in particular it is more than simply dropping negations. In fact inequations become the standard relation between terms on the syntax side, just as it is between elements on the model side. This is borne out by the existing axiomatization of positive modal logic originally proposed in [2]} which is entirely given by inequations. For these reasons, and following [3]}, [4]}, this paper will present positive coalgebraic logic as a \(\mathbf {Pos}\) -enriched coalgebraic logic. In a slogan: “in positive coalgebraic logic we remove negations but we add order”.
