An exactification of the monoid of primitive recursive functions (Q817674)

Let \(\mathcal{R}\)\ be a partially ordered category with involution \(\ast\), assuming that the hom-sets are \(\wedge\)-semilattices. The category \(\mathcal{R}\) is to be regarded as a category of relations, in which we can find a non-null subcategory \(\mathcal{C}\)\ of functions, namely, relations \(f:A\rightarrow B\) with \(ff^{\ast}\leq1_{B}\) and \(1_{A}\leq f^{\ast}f\). The authors are interested in two special cases. The first case is that \(\mathcal{C}\)\ is the monoid \(\mathcal{N}\)\ of primitive recursive functions \(\mathbb{N}\rightarrow\mathbb{N}\) and \(\mathcal{R}\)\ is the category of recursively enumerable relations on \(\mathbb{N}\). The second case is that \(\mathcal{C}\)\ is a regular category and \(\mathcal{R}\)\ is the category of relations constructed from spans in \(\mathcal{C}\). The authors note a similarity between the construction \(\widetilde{\mathcal{N}}\) from \(\mathcal{N}\) in the first case and the exact completion of \(\mathcal{C}\)\ in the second case, so that they want to bring these two constructions under one hat. One possible way with the first case would be to first embed \(\mathcal{N}\)\ in its regular completion and then apply the methods in the second case, which was already implicit in [\textit{P. J. Freyd} and \textit{A. Scedrov}, Categories, allegories. North-Holland Mathematical Library, 39. Amsterdam etc.: North-Holland. (1990; Zbl 0698.18002)]. This article aims to handle the first case by a one-step construction, which is very akin to the construction of the category of modest sets (\textit{G. Rosolini}, [Int. J. Found. Comput. Sci. 1, No. 3, 341--353 (1990; Zbl 0729.18003)] and \textit{E. S. Bainbridge} [Theor. Comput. Sci. 70, No. 1, 35--64 (1990; Zbl 0717.18005)]) as well as the idempotent splitting construction (Karoubi envelope) used in [\textit{J. Lambek} and \textit{P. J. Scott}, Introduction to higher order categorical logic. Cambridge Studies in Advanced Mathematics, 7. Cambridge etc.: Cambridge University Press. (1986; Zbl 0596.03002)].