Lax naturality through enrichment (Q1923539)

This paper has its origins in work of \textit{C. A. R. Hoare} (unpublished, 1987) on data refinement. Let \({\mathcal O}\)\textit{rd} denote the Cartesian monoidal category of ordered sets and order-preserving functions. Let \({\mathcal V}\) be the category of \({\mathcal O}\)\textit{rd}-categories and \({\mathcal O}\)\textit{rd}-functors. The interest here is in the closed structure on \({\mathcal V}\) where the left internal hom \([A,B]\) is the \({\mathcal O}\)\textit{rd}-category of \({\mathcal O}\)\textit{rd}-functors \(f : A \to B\) and lax natural transformations \(\alpha : f \Rightarrow g\). The paper describes how to present \({\mathcal V}\)-categories of Eilenberg-Moore algebras for finitary monads on a locally finitely presentable \({\mathcal V}\)-category \({\mathcal C}\) in terms of covariant operations and relations. To account for contravariant operations (such as internal homs) the paper makes use of those lax natural \(\alpha : f \Rightarrow g\) which have a left adjoint \(\lambda : g \Rightarrow f\) with identity counit (not merely the invertible \(\alpha)\).