# The Exact Completion for Regular Categories enriched in Posets

Vasileios Aravantinos-Sotiropoulos

###### Abstract.

We construct an exact completion for regular categories enriched in the
cartesian closed category $\mathsf{Pos}$ of partially ordered sets and
monotone functions by employing a suitable calculus of relations. We then
characterize the embedding of any regular category into its completion and use
this to obtain examples of concrete categories which arise as such
completions. In particular, we prove that the exact completion in this
enriched sense of both the categories of Stone and Priestley spaces is the
category of compact ordered spaces of L. Nachbin. Finally, we consider the
relationship between the enriched exact completion and categories of internal
posets in ordinary categories.

##  1\. Introduction

The notions of regularity and (Barr-)exactness have been fundamental in
Category Theory for quite some time. Exactness was introduced by Barr[4] in
1970 and motivated by a result of Tierney which essentially exhibited the
notion as the non-additive part of the definition of abelian category. From
another perspective, it is the basic property which is common to both abelian
categories and elementary toposes. Regularity is a weaker property which can
be viewed as the requirement that the category affords a good calculus of
internal relations. Alternatively, from the perspective of Categorical Logic,
regular categories are those which correspond to the fragment of first-order
Logic on the operations $\land,\top,\exists$.

In this paper we look at these notions in an enriched setting. More precisely,
we work with versions of them that apply to categories enriched over the
cartesian closed category $\mathsf{Pos}$ of partially ordered sets and
monotone functions. Our main motivation comes from the paper [14] by A. Kurz
and J. Velebil, where $\mathsf{Pos}$-enriched regularity and exactness were
first explicitly considered. The authors employ these notions to obtain
categorical characterizations of (quasi-)varieties of ordered algebras in the
sense of Bloom & Wright[5], very much along the lines of the corresponding
characterizations for ordinary (quasi-)varieties of Universal Algebra. Broadly
speaking, varieties turn out to be the exact categories possessing a “nice”
generator, while quasivarieties can be characterized in a similar fashion by
replacing exactness with the weaker regularity.

Recall here that _ordered algebras_ in the sense of [5] are algebras over some
signature $\Sigma$ which consist of a poset $X$ together with a monotone map
$[\sigma]\colon X^{n}\to X$, for each specified $n$-ary operation $\sigma$. A
_homomorphism_ of such algebras is a monotone map which preserves the
operations. Then a _variety_ in this context is defined as a class of ordered
algebras satisfying a set of formal inequalities $s\leq t$, where $s,t$ are
$\Sigma$-terms. A _quasivariety_ is a class defined by more general formal
implications of the form $\bigwedge\limits_{i\in I}(s_{i}\leq t_{i})\implies
s\leq t$, where again the $s_{i},t_{i},s,t$ are $\Sigma$-terms.

The categories $\mathsf{OrdSGrp}$ and $\mathsf{OrdMon}$ of ordered semigroups
and ordered monoids respectively are both examples of varieties which play an
important role in the theory of automata. More generally, any quasivariety of
ordinary algebras gives rise to a quasivariety of ordered algebras defined by
the same axioms. A different example of quasivariety is given by the
_cancellative_ ordered monoids $\mathsf{OrdMon_{can}}$, i.e. the ordered
monoids $(M,\cdot,\leq)$ satisfying the implications $x\cdot z\leq y\cdot
z\implies x\leq y$ and $z\cdot x\leq z\cdot y\implies x\leq y$ for all
$x,y,z\in M$. A further source of examples is furnished by ordinary varieties
whose axioms contain those of semi-lattices, since they can be equipped with
the equationally definable order $x\leq y\iff x\vee y=y$. Yet more examples of
quasivarieties are given by the _Kleene algebras_ of Logic.

While (quasi-)varieties of ordered algebras are a central source of examples
of $\mathsf{Pos}$-enriched categories, there are other interesting examples
that will appear in the present paper. For one, we have the category
$S$-$\mathsf{Pos}$ [8] of monotone actions of an ordered monoid $S$ on a poset
and monotone equivariant maps between them. Furthermore, there are categories
of ordered topological spaces, such as Priestley spaces or the _compact
ordered spaces_ of Nachbin. These are all examples of categories which are
either themselves monadic over $\mathsf{Pos}$ or reflective in a monadic
category.

The thread of this paper can be seen as one continuation of the ideas
developed in [14] and is in part suggested by the authors at the end of the
latter paper. At the same time it is part of a growing recent interest in the
categorical treatment of ordered algebras, as for example in the recent
preprints [1] and [2]. Our main contribution here is a construction of the
_exact completion of a regular category_ for $\mathsf{Pos}$-categories which
employs a suitably enriched version of the _calculus of relations_. We then
identify varieties of ordered algebras which occur as such completions of
corresponding (quasi-)varieties of ordered or unordered algebras. Furthermore,
we prove that the exact completion of the category of _Priestley spaces_ is
precisely the category of _Nachbin spaces_. This provides an ordered version
of the folklore result which identifies the category of compact Hausdorff
spaces as the exact completion (in the ordinary sense) of the regular category
of Stone spaces. In fact, it will follow by the same token that the exact
completion of Stone spaces in the enriched sense is also the category of
Nachbin spaces.

### Organization of the paper

In section 2 we collect some preliminaries involving regularity for categories
enriched over $\mathsf{Pos}$, mostly for the convenience of the reader. There
is only one original contribution here, 2, which provides a simplification of
the definition of regularity that was presented in [14]. More precisely, we
prove that one of the defining conditions is a consequence of the other three
and can thus be omitted.

Section 3 discusses the main aspects of the calculus of relations which is
available in any regular category. The main result in this section is 3, which
identifies the morphisms of a regular category as the left adjoints in a
suitable bicategory of relations.

Section 4 represents the crux of the paper and is where we construct the exact
completion of a regular category. After the initial definition, we prove in a
sequence of steps that our proposed construction indeed satisfies the required
properties, culminating in 4. The arguments here make extensive use of the
calculus of relations relying on the previous section.

In section 5 we characterize the embedding of a regular category into its
completion. This is subsequently used to obtain examples of categories which
arise as exact completions of one or more of their regular subcategories. In
particular, we show that the category of Nachbin spaces is exact and can be
obtained as the completion of either the category of Priestley or Stone
spaces.

Finally, in section 6 we examine the relationship between the process of exact
completion and that of taking internal posets in an ordinary category. We
prove that, in a suitable sense, these two commute.

##  2\. Preliminaries on Regularity

In this section we collect some preliminaries concerning the notion of
regularity for categories enriched over the cartesian closed category
$\mathsf{Pos}$ of posets and order-preserving functions, as defined by Kurz
and Velebil in [14]. After recalling some basic facts about finite limits, we
reexamine the definition of regularity and observe that one of the conditions
therein is in fact redundant.

Throughout the paper by ‘a category $\mathcal{C}$’ we shall always mean a
category that is enriched over the cartesian closed category $\mathsf{Pos}$ of
partially ordered sets and monotone functions. Explicitly, this means that
$\mathcal{C}$ is a category such that each $\mathop{\rm
Hom}_{\mathcal{C}}(X,Y)$ is equipped with a partial order relation and such
that composition of morphisms is order-preserving in each variable. If we wish
to refer to categories in the usual non-enriched sense we will always use the
adjective ‘ordinary’.

A functor $F\colon\mathcal{C}\to\mathcal{D}$ will always mean a
$\mathsf{Pos}$-functor, i.e. an ordinary functor that furthermore preserves
the order of morphisms.

Similarly, whenever we speak of limits or colimits in a category
$\mathcal{C}$, these will always mean _weighted_ (co-)limits (also called
_indexed_ (co-)limits in [13]). We know from [13] that completeness of a
category $\mathcal{C}$, i.e. the existence of all small weighted limits, is
equivalent to the existence in $\mathcal{C}$ of all small conical limits and
all powers. The former of these can in turn be constructed via products and
equalizers, so that $\mathcal{C}$ is complete if and only if it possesses
products, equalizers and powers. Recall here that the power of an object
$X\in\mathcal{C}$ to a poset $P$ is an object $X^{P}\in\mathcal{C}$ for which
there exists a natural isomorphism

$\mathcal{C}(C,X^{P})\cong\mathrm{Hom}_{\mathsf{Pos}}(P,\mathcal{C}(C,X))$

When the base of enrichment is locally finitely presentable as a monoidal
category[11], as in our case with $\mathsf{Pos}$, there is also a useful
notion of _finite_ weighted limit. In particular, we have that $\mathcal{C}$
is finitely complete if and only if it has finite products, equalizers and
finite powers. By _finite power_ here we mean a power object $X^{P}$ where $P$
is a finitely presentable object in $\mathsf{Pos}$, i.e. a finite poset.

We begin by recalling some basic notions, most of which can also be found in
[14]. First, the notion of monomorphism that is more appropriate in the
ordered context and which will form part of the factorization system leading
to the notion of regularity for $\mathsf{Pos}$-categories.

  * 2.1 Definition.

A morphism $m\colon X\to Y$ in a category $\mathcal{C}$ is called an
_$\mathsf{ff}$ -morphism_ (or _representably fully faithful_ , or an _order-
monomorphism_) if for every $Z\in\mathcal{C}$ the monotone map
$\mathcal{C}(Z,m)\colon\mathcal{C}(Z,X)\to\mathcal{C}(Z,Y)$ in $\mathsf{Pos}$
also reflects the order.

We shall use the terms “$\mathsf{ff}$-morphism” and “order-monomorphism”
interchangeably throughout the paper. Furthermore, we will use the term
‘order-epimorphism’ for the dual notion.

Explicitly, $m\colon X\to Y$ is an $\mathsf{ff}$-morphism when for every
$f,g\colon Z\to X$ the implication $mf\leq mg\implies f\leq g$ holds. In
$\mathsf{Pos}$, $m$ is an $\mathsf{ff}$-morphism precisely when it is an
order-embedding, i.e. a map which preserves and reflects the order. Any such
map is of course a monomorphism, but the converse is not true.

The shift from monomorphisms to $\mathsf{ff}$-morphisms is also essentially
the difference between the notion of conical (weighted) limit in a category
$\mathcal{C}$ and the ordinary limit of the same type in the underlying
ordinary category $\mathcal{C}_{0}$. For example, consider two objects
$X,Y\in\mathcal{C}$. Then a diagram $\textstyle{X}$$\textstyle{X\times
Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{X}}$$\scriptstyle{\pi_{Y}}$$\textstyle{Y}$
is a product diagram if the usual unique factorization property is satisfied,
along with the following additional condition: given any two morphisms
$u,v\colon Z\to X\times Y$, the pair of inequalities $\pi_{X}u\leq\pi_{X}v$
and $\pi_{Y}u\leq\pi_{Y}v$ together imply that $u\leq v$. In other words, the
pair of projections $\pi_{X},\pi_{Y}$ must be jointly _order_ -monomorphic,
rather than just jointly monomorphic. This stems from the fact that the
universal property is a natural isomorphism $\mathop{\rm Hom}(Z,X\times
Y)\cong\mathop{\rm Hom}(Z,X)\times\mathop{\rm Hom}(Z,Y)$ in $\mathsf{Pos}$,
rather than in $\mathsf{Set}$. A similar observation applies to colimits in
$\mathcal{C}$.

Let us record below a few basic properties of $\mathsf{ff}$-morphisms familiar
for monomorphisms in an ordinary category.

  * 2.2 Lemma.

Consider morphisms $f\colon X\to Y$ and $g\colon Y\to Z$ in a category
$\mathcal{C}$. Then:

    1. (1)

If $f,g$ are $\mathsf{ff}$-morphisms, then so is $gf$.

    2. (2)

If $gf$ is an $\mathsf{ff}$-morphism, then so is $f$.

    3. (3)

$\mathsf{ff}$-morphisms are stable under pullback.

###### Proof.

Perhaps only item (3) needs some details, so consider the following pullback
square in $\mathcal{C}$ where $f$ is an $\mathsf{ff}$-morphism and assume that
$u,v\colon A\to P$ are such that $qu\leq qv$.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{q}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{Z}$

We then have $gqu\leq gqv\implies fpu\leq fpv\implies pu\leq pv$, since $f$ is
an $\mathsf{ff}$-morphism. Then, because we have both $pu\leq pv$ and $qu\leq
qv$, we conclude by the limit property of the pullback that $u\leq v$. ∎

We recall next two particular examples of weighted limits which are not
conical and which play an important role in the context of
$\mathsf{Pos}$-categories. See also [14].

The _comma object_ of an ordered pair of morphisms $(f,g)$ with common
codomain is a square

${C}$${Y}$${X}$${Z}$$\scriptstyle{c_{1}}$$\scriptstyle{c_{0}}$${\leq}$$\scriptstyle{g}$$\scriptstyle{f}$

such that $fc_{0}\leq gc_{1}$ and which is universal with this property, the
latter meaning precisely the following two properties:

  1. (1)

Given $u_{0}\colon W\to X$ and $u_{1}\colon W\to Y$ in $\mathcal{C}$ such that
$fu_{0}\leq gu_{1}$, there exists a $u\colon W\to C\in\mathcal{C}$ such that
$c_{0}u=u_{0}$ and $c_{1}u=u_{1}$.

  2. (2)

The pair $(c_{0},c_{1})$ is jointly order-monomorphic.

Note in particular that the factorization given in (1) will be unique by (2).
We will usually denote the comma object $C$ by $f/g$. In $\mathsf{Pos}$, the
comma object is given by $f/g=\\{(x,y)\in X\times Y|f(x)\leq g(y)\\}$ with the
order induced from the product.

The _inserter_ of an ordered pair $(f,g)$ of parallel morphisms
${X}$${Y}$$\scriptstyle{f}$$\scriptstyle{g}$ is a morphism $e\colon E\to
X\in\mathcal{C}$ such that $fe\leq ge$ and universal in the following sense:

  1. (1)

If $h\colon Z\to X\in\mathcal{C}$ is such that $fh\leq gh$, then there exists
a $u\colon Z\to A$ such that $eu=h$.

  2. (2)

$e$ is an $\mathsf{ff}$-morphism.

Again, note that the factorization posited in (1) is unique by property (2).
In $\mathsf{Pos}$, the inserter is precisely $E=\\{x\in X|f(x)\leq g(x)\\}$
with the order induced from $X$.

It will be convenient for us to have an alternative way of constructing all
finite weighted limits using inserters along with some conical limits. This is
then the content of the following proposition, which should be well-known and
in any case follows from more general facts about 2-categorical limits. We
nevertheless include a proof for the sake of completeness.

  * 2.3 Proposition.

A category $\mathcal{C}$ is finitely complete if and only if it has finite
products and inserters.

###### Proof.

Suppose that $\mathcal{C}$ has finite products and inserters. To have all
finite conical limits it suffices to construct equalizers. So consider any
parallel pair of morphisms
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{g}$$\textstyle{Y}$
in $\mathcal{C}$. Let $m\colon M\to X$ be the inserter of the pair $(f,g)$ and
then let $n\colon E\to M$ be the inserter of $(gm,fm)$. We claim that now
$e\coloneqq mn\colon E\to X$ is the desired equalizer. Indeed, note first that
$gmn\leq fmn$ and also $fm\leq gm\implies fmn\leq gmn$, so that $fmn=gmn$.
Then suppose that $h\colon Z\to X$ is such that $fh=gh$. Since in particular
$fh\leq gh$, there exists a unique $u\colon Z\to M$ such that $mu=h$. Now $u$
is such that $gmu=gh\leq fh=fmu$, so we have a unique $v\colon Z\to E$ such
that $nv=u$. So $ev=mnv=mu=h$. Finally, it is clear that $e$ is order-
monomorphic, since both $m,n$ are so.

Second, we need to construct finite powers, so let $P$ be a finite poset and
consider any $X\in\mathcal{C}$. Consider the product $\prod\limits_{a\in P}X$
(i.e. the ordinary power) and for every pair of elements $a,b\in P$ with
$a\leq b$ form the inserter of $(\pi_{a},\pi_{b})$, say
$\textstyle{E_{ab}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{ab}}$$\textstyle{\prod\limits_{a\in
P}X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{a}}$$\scriptstyle{\pi_{b}}$$\textstyle{X}$
in $\mathcal{C}$. Set $E\coloneqq\prod\limits_{a\leq b}E_{ab}$. We claim the
$E$ is the power $X^{P}$.

To show this, consider any family of morphisms $(f_{a}\colon C\to X)_{a\in P}$
such that $a\leq b\implies f_{a}\leq f_{b}$, i.e. a homomorphism
$P\to\mathcal{C}(C,X)$ in $\mathsf{Pos}$. There is then a unique $f\colon
C\to\prod\limits_{a\in P}X$ such that $\pi_{a}f=f_{a}$ for all $a\in P$. Now
for each pair of elements $a,b\in P$ with $a\leq b$ we have $f_{a}\leq f_{b}$,
which is to say $\pi_{a}f\leq\pi_{b}f$. Hence, there is a unique $u_{ab}\colon
C\to E_{ab}$ with $e_{ab}u_{ab}=f$. This in turn induces a unique $u\colon
C\to E$ such that $\pi_{ab}u=u_{ab}$ whenever $a,b\in P$ with $a\leq b$.

Finally, let’s show that this assignment is order-preserving and order
reflecting. So consider another family $(g_{a}\colon C\to X)_{a\in P}$, with
$g\colon C\to\prod\limits_{a\in P}X$ and $v\colon C\to E$ corresponding to $f$
and $u$ as defined above for $(f_{a})_{a\in P}$. If $(f_{a})_{a\in
P}\leq(g_{a})_{a\in P}$, then $f_{a}\leq g_{a}$ for all $a\in P$, i.e.
$\pi_{a}f\leq\pi_{a}g$ for all $a\in P$ and hence $f\leq g$ by the universal
property of the product. This in turn means that whenever $a\leq b$ we have
$e_{ab}u_{ab}=f\leq g=e_{ab}v_{ab}$ and so $u_{ab}\leq v_{ab}$, hence $u\leq
v$. It is clear that these implications can also be reversed. ∎

If a category $\mathcal{C}$ has comma objects, then in particular for any
morphism $f\colon X\to Y\in\mathcal{C}$ we can form the comma of the pair
$(f,f)$. This comma measures the extent to which $f$ fails to be an
$\mathsf{ff}$-morphism and ultimately connects with the notions of regularity
and exactness to be introduced shortly.

  * 2.4 Definition.

Given any morphism $f\colon X\to Y$ in a category $\mathcal{C}$, the comma
object $f/f$ is called the _kernel congruence_ of $f$.

  * 2.5 Lemma.

For any morphism $f\colon X\to Y$ with kernel congruence
$\textstyle{f/f\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\scriptstyle{f_{1}}$$\textstyle{X}$
in a category $\mathcal{C}$, the following are equivalent:

    1. (1)

$f$ is an $\mathsf{ff}$-morphism.

    2. (2)

$f_{0}\leq f_{1}$.

    3. (3)

The canonical morphism $\iota_{f}\colon 1_{X}/1_{X}\to f/f$ is an isomorphism.

###### Proof.

If $f$ is an $\mathsf{ff}$-morphism, then $ff_{0}\leq ff_{1}\implies f_{0}\leq
f_{1}$.

If $f_{0}\leq f_{1}$, then $1_{X}f_{0}\leq 1_{X}f_{1}$ implies that
$(f_{0},f_{1})$ must factor through $1_{X}/1_{X}$ via a morphism which is then
easily seen to be inverse to $1_{X}/1_{X}\rightarrow f/f$.

Finally, assume that $f/f\cong 1_{X}/1_{X}$ and let $u_{0},u_{1}\colon Z\to X$
be such that $fu_{0}\leq fu_{1}$. Then $(u_{0},u_{1})$ factors through $f/f$
and so through $1_{X}/1_{X}$. But the latter means precisely that $u_{0}\leq
u_{1}$. ∎

As we have mentioned already, the class of $\mathsf{ff}$-morphisms will be the
“mono part” of a factorization system for regular categories. The other class
of morphisms is taken to be the class of morphisms orthogonal to all
$\mathsf{ff}$-morphisms, as has to be the case in any orthogonal factorization
system. Let us first recall the definition of orthogonality in this enriched
context.

  * 2.6 Definition.

Given morphisms $e\colon A\to B$ and $m\colon X\to Y$ in a category
$\mathcal{C}$, we say that $e$ is _left orthogonal_ to $m$ and write $e\perp
m$ if the square

$\textstyle{\mathcal{C}(B,X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{-\circ
e}$$\scriptstyle{m\circ-}$$\textstyle{\mathcal{C}(A,X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m\circ-}$$\textstyle{\mathcal{C}(B,Y)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{-\circ
e}$$\textstyle{\mathcal{C}(A,Y)}$

is a pullback in $\mathsf{Pos}$.

To make things more explicit, the statement $e\perp m$ means two things:

  1. (1)

The usual diagonal fill-in property.

  2. (2)

Given two commutative squares
$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{u_{1}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v_{1}}$$\scriptstyle{d_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{u_{2}}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v_{2}}$$\scriptstyle{d_{2}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$

in $\mathcal{C}$ with $u_{1}\leq u_{2}$ and $v_{1}\leq v_{2}$, the diagonal
fill-ins must also satisfy $d_{1}\leq d_{2}$.

Then, as in [14] we introduce the following class of morphisms, which in some
sense are the $\mathsf{Pos}$-enriched analogue of strong epimorphisms for
ordinary categories.

  * 2.7 Definition.

A morphism $e\colon A\to B$ is called an _$\mathsf{so}$ -morphism_ (or
_surjective on objects_) if $e\perp m$ for every $\mathsf{ff}$-morphism
$m\colon X\to Y\in\mathcal{C}$.

  * 2.8 Remark.

We note here that, in the special case of checking a condition $e\perp m$ with
$m$ an $\mathsf{ff}$-morphism, the 2-dimensional part of the definition of
orthogonality (property 2 above) follows for free. Indeed, in the notation of
the above diagrams, the fact that $md_{1}=v_{1}\leq v_{2}=md_{2}$ then implies
$d_{1}\leq d_{2}$.

We record here two basic properties of $\mathsf{so}$-morphisms which will be
used throughout the paper. These follow simply because the class of
$\mathsf{so}$-morphisms is defined by a left orthogonality condition.

  * 2.9 Lemma.

Consider morphisms $f\colon X\to Y$ and $g\colon Y\to Z$ in a category
$\mathcal{C}$. Then:

    1. (1)

If $f,g$ are $\mathsf{so}$-morphisms, then so is $gf$.

    2. (2)

If $gf$ is an $\mathsf{so}$-morphism, then so is $g$.

The $\mathsf{so}$-morphisms will be the “epimorphism part” of the
factorization system on regular categories. Indeed, given the existence of
some limits, every $\mathsf{so}$-morphism is an order-epimorphism.

  * 2.10 Lemma.

If $\mathcal{C}$ has inserters, then every $\mathsf{so}$-morphism in
$\mathcal{C}$ is an
order-epimorphism.

###### Proof.

Let $e\colon A\to B$ be an $\mathsf{so}$-morphism and consider $f,g\colon B\to
C$ such that $fe\leq ge$. Let $m\colon M\to B$ be the inserter of $(f,g)$.
Then there exists a unique $u\colon A\to M$ such that $mu=e$. But we have
$e\perp m$ and so we obtain a $v\colon B\to M$ such that $ve=u$, $mv=1_{B}$.
Now $m$ is both a split epimorphism and a monomorphism, hence an isomorphism
and so $fm\leq gm\implies f\leq g$. ∎

The notion of regularity for ordinary categories, as is well known, can be
defined either in terms of strong epimorphisms or in terms of regular
epimorphisms. In fact, one can argue that a significant part of the power of
regularity is that it forces these two classes of epimorphisms to coincide.
From another perspective, the regular epimorphisms are the categorical notion
of quotient that is usually appropriate in ordinary categories. For
$\mathsf{Pos}$-categories the corresponding notion is that of _coinserter_ ,
which is dual to the notion of inserter defined earlier. Intuitively, whereas
taking a coequalizer corresponds to adding new equalities, constructing a
coinserter should be thought of as adding new _inequalities_.

Now, just as every regular epimorphism is always strong, so too we have the
following.

  * 2.11 Lemma.

Every coinserter is an $\mathsf{so}$-morphism.

###### Proof.

Consider the following commutative diagram, where $e$ is assumed to be the
coinserter of $(f_{0},f_{1})$ and $m$ is an $\mathsf{ff}$-morphism.

$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\scriptstyle{f_{1}}$$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\scriptstyle{u}$$\textstyle{B\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$

Now we have $muf_{0}=vef_{0}\leq vef_{1}=muf_{1}$, so by virtue of $m$ being
an $\mathsf{ff}$-morphism we get $uf_{0}\leq uf_{1}$. Then by the coinserter
property there exists a unique $d\colon B\to X$ such that $de=u$. It follows
also that $md=v$ because $e$ is an order-epimorphism. ∎

  * 2.12 Definition.

A morphism $q\colon X\to Y$ is called an _effective_ (epi-)morphism if it is
the coinserter of some pair of parallel morphisms.

The notion of regularity of a category is essentially an exactness property
relating kernel congruences and coinserters. There are however some exactness
properties involving these notions that always hold, regardless of regularity.
This is the content of the following proposition, which again should be
compared to the corresponding facts involving kernel pairs and coequalizers in
an ordinary category (see [6]).

  * 2.13 Proposition.

    1. (1)

If an effective epimorphism has a kernel congruence, then it must be the
coinserter of that kernel congruence.

    2. (2)

If a kernel congruence has a coinserter, then it is also the kernel congruence
of that coinserter.

###### Proof.

  1. (1)

Suppose
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\scriptstyle{f_{1}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{Q}$
is a coinserter diagram and assume $q$ has a kernel congruence
$\textstyle{q/q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q_{0}}$$\scriptstyle{q_{1}}$$\textstyle{Y}$
in $\mathcal{C}$. Then $qf_{0}\leq qf_{1}\implies(\exists!u\colon X\to
q/q)q_{0}u=f_{0},q_{1}u=f_{1}$, by the universal property of kernel
congruence.

Now let $g\colon Y\to Z$ be such that $gq_{0}\leq gq_{1}$. Then $gq_{0}u\leq
gq_{1}u\implies gf_{0}\leq gf_{1}$ and so $(\exists!v\colon Q\to Z)vq=g$.
Finally, $q$ is already an order-epimorphism by virtue of being a coinserter
of some pair of morphisms.

  2. (2)

Suppose that
$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{0}}$$\scriptstyle{r_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{Q}$
is a coinserter diagram and that $(r_{0},r_{1})$ is the kernel congruence of
some $f\colon X\to Y$. Then $fr_{0}\leq fr_{1}$ implies the existence of a
unique $u\colon Q\to Y$ such that $uq=f$.

Now let $a,b\colon A\to X$ be such that $qa\leq qb$. Then also $uqa\leq uqb$,
i.e. $fa\leq fb$ and so $(\exists!v\colon A\to R)r_{0}v=a,r_{1}v=b$.

∎

We now come to the definition of regularity for $\mathsf{Pos}$-enriched
categories, as presented by Kurz and Velebil in [14]. We label it as
‘provisional’ in the context of this paper for reasons that will be justified
shortly.

  * 2.14 Definition.

(provisional) A category $\mathcal{C}$ is _regular_ if it satisfies the
following:
(R1) $\mathcal{C}$ has all finite (weighted) limits.
(R2) $\mathcal{C}$ has ($\mathsf{so}$,$\mathsf{ff}$)-factorizations.
(R3) $\mathsf{so}$-morphisms are stable under pullback in $\mathcal{C}$.
(R4) Every $\mathsf{so}$-morphism is effective in $\mathcal{C}$.

A main feature of this definition is that it posits the existence of a stable
($\mathsf{so}$,$\mathsf{ff}$) factorization system in $\mathcal{C}$. The
authors go on to state that the ‘gist of the definition’ is property (R4),
i.e. the assumption that $\mathsf{so}$-morphisms and effective morphisms
coincide, which essentially states that it is equivalent to require the stable
factorization system to be (effective,$\mathsf{ff}$). However, we shall show
that condition (R4) in fact follows from the first three conditions, much like
in the case of ordinary regularity one can state the definition equivalently
either in terms of regular epimorphisms or strong epimorphisms. In fact, the
proof is essentially a direct adaptation of the corresponding one in the
ordinary context (see [6]).

Before making good on our claim, we need a preparatory result on the pasting
of a pullback square with a comma square. This is well-known from the realm of
2-categories, but we include its proof for the sake of making this paper more
self-contained.

  * 2.15 Lemma.

Consider the following diagram in a category $\mathcal{C}$, where the right-
hand square is a comma square and the left-hand square commutes.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q_{1}}$$\scriptstyle{q_{0}}$$\scriptstyle{\leq}$$\textstyle{Z\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g}$$\textstyle{X^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{x}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\textstyle{Y}$

Then the outer rectangle is a comma square if and only if the left-hand square
is a pullback.

###### Proof.

Assume first that the left-hand square is a pullback. Note first that by our
assumptions on the diagram we have $fxp_{0}=fq_{0}p_{1}\leq gq_{1}p_{1}$. Now
suppose that $u\colon A\to X^{\prime}$ and $v\colon A\to Z$ are such that
$fxu\leq gv$. Since the right-hand square is a comma, $(\exists!w\colon A\to
Q)q_{0}w=xu,q_{1}w=v$. The first of these equalities by virtue of the pullback
property gives that $(\exists!z\colon A\to P)p_{0}z=u,p_{1}z=w$. Then we have
$q_{1}p_{1}z=q_{1}w=v$ as well.

Finally, assume that $z,z^{\prime}\colon A\to P$ are such that $p_{0}z\leq
p_{0}z^{\prime}$ and $q_{1}p_{1}z\leq q_{1}p_{1}z^{\prime}$. Then we also have
$xp_{0}z\leq xp_{0}z^{\prime}\implies q_{0}p_{1}z\leq q_{0}p_{1}z^{\prime}$,
so that by the universal property of the comma square we get $p_{1}z\leq
p_{1}z^{\prime}$. The latter inequality together with $p_{0}z\leq
p_{0}z^{\prime}$ yield $z\leq z^{\prime}$ by the universal property of the
pullback.

Conversely, assume that the outer square is a comma and let $u\colon A\to
X^{\prime}$ and $v\colon A\to Q$ be such that $xu=q_{0}v$. Then we have
$fxu=fq_{0}v\leq gq_{1}v$, so the outer rectangle being a comma says that
$(\exists!w\colon A\to P)p_{0}w=u,q_{1}p_{1}w=q_{1}v$. But since also
$q_{0}p_{1}w=xp_{0}w=xu=q_{0}v$ and $q_{0},q_{1}$ are jointly monomorphic, we
obtain also that $p_{1}w=v$. Finally, it is clear that $p_{0},p_{1}$ are
jointly order-monomorphic because $p_{0},q_{1}p_{1}$ are so. ∎

Now we can prove that condition (R4) in the definition of regularity is
superfluous. The proof that follows is almost identical to that of Proposition
2.2.2 in [6], concerning ordinary regularity, where we replace some uses of
the familiar lemma on pasting of pullback squares with 2.

  * 2.16 Proposition.

If $\mathcal{C}$ is a category satisfying conditions (R1),(R2) and (R3) of 2,
then it also satisfies (R4).

###### Proof.

Let $f\colon X\to Y$ be an $\mathsf{so}$-morphism and consider its kernel
congruence
$\textstyle{f/f\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{k_{0}}$$\scriptstyle{k_{1}}$$\textstyle{X}$,
which exists in $\mathcal{C}$ by (R1). We want to show that $f$ is the
coinserter of $(k_{0},k_{1})$.

So let $g\colon X\to Z\in\mathcal{C}$ be such that $gk_{0}\leq gk_{1}$. We can
consider then the induced morphism $\langle f,g\rangle\colon X\to Y\times Z$.
By (R2) we can factor this morphism as an $\mathsf{so}$-morphism followed by
an $\mathsf{ff}$-morphism, say
$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i}$$\textstyle{Y\times
Z}$. We then form the following diagram in $\mathcal{C}$, where we begin by
forming the bottom right-hand square as a comma square and then the remaining
three squares are pullbacks.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v_{1}}$$\scriptstyle{v_{0}}$$\textstyle{P_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{x_{1}}$$\scriptstyle{u_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{P_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u_{0}}$$\scriptstyle{x_{0}}$$\textstyle{C\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{c_{1}}$$\scriptstyle{c_{0}}$$\scriptstyle{\leq}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{Y}i}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{Y}i}$$\textstyle{Y}$

By an application of 2 and its order-dual as well as the usual pullback gluing
lemma we deduce that the big outer square resulting from the pasting of all
four smaller ones is also a comma square. Then, since $\pi_{Y}ip=f$, we have
$P\cong f/f$ and we can assume that $x_{0}v_{0}=k_{0}$ and $x_{1}v_{1}=k_{1}$.
Also, observe that by (R3) we have that $u_{0},u_{1}$ and then also
$v_{0},v_{1}$ are $\mathsf{so}$-morphisms.

Now we want to show that $\pi_{Y}i$ is an iso. Since $(\pi_{Y}i)p=f$ is an
$\mathsf{so}$-morphism, we already know, by 2, that $\pi_{Y}i$ is an
$\mathsf{so}$-morphism as well. Thus, it suffices to show that it is also an
$\mathsf{ff}$-morphism, which is equivalent to showing $c_{0}\leq c_{1}$.
Since $u_{0}v_{0}=u_{1}v_{1}$ is an $\mathsf{so}$-morphism, so in particular
an order-epimorphism, the latter inequality is equivalent to having
$c_{0}u_{0}v_{0}\leq c_{1}u_{0}v_{0}$. This is in turn equivalent to
$ic_{0}u_{0}v_{0}\leq ic_{1}u_{0}v_{0}$, because $i$ is an
$\mathsf{ff}$-morphism. To prove this last inequality we now observe the
following:

$\pi_{Y}ic_{0}u_{0}v_{0}=\pi_{Y}ipx_{0}v_{0}=fx_{0}v_{0}=fk_{0}\leq
fk_{1}=fx_{1}v_{1}=\pi_{Y}ipx_{1}v_{1}=\pi_{Y}ic_{1}u_{0}v_{0}$
$\pi_{Z}ic_{0}u_{0}v_{0}=\pi_{Z}ipx_{0}v_{0}=gx_{0}v_{0}=gk_{0}\leq
gk_{1}=gx_{1}v_{1}=\pi_{Z}ipx_{1}v_{1}=\pi_{Z}ic_{1}u_{0}v_{0}$

Then the universal property of the product yields the desired inequality.

Finally, we now have a morphism $\pi_{Z}i(\pi_{Y}i)^{-1}\colon Y\to Z$ such
that $\pi_{Z}i(\pi_{Y}i)^{-1}f=\pi_{Z}i(\pi_{Y}i)^{-1}\pi_{Y}ip=\pi_{Z}ip=g$.
Furthermore, we know already that $f$ is an order-epimorphism because it is an
$\mathsf{so}$-morphism by assumption. ∎

Thus, we can officially strike condition (R4) from the definition of
regularity and henceforth adopt the following more economical one.

  * 2.17 Definition.

A category $\mathcal{C}$ will be called _regular_ if it satisfies the
following:
(R1) $\mathcal{C}$ has all finite (weighted) limits.
(R2) $\mathcal{C}$ has ($\mathsf{so}$,$\mathsf{ff}$)-factorizations.
(R3) $\mathsf{so}$-morphisms are stable under pullback in $\mathcal{C}$.

Similarly, we can now furthermore establish another equivalent
characterization of regularity in terms of the existence of quotients for
kernel congruences.

  * 2.18 Proposition.

A finitely complete category $\mathcal{C}$ is regular if and only if the
following hold:

    1. (1)

Every kernel congruence in $\mathcal{C}$ has a coinserter.

    2. (2)

Effective morphisms are stable under pullback in $\mathcal{C}$.

###### Proof.

If $\mathcal{C}$ is regular, then it is easy to see that it satisfies the two
conditions above by definition and by an appeal to part (2.) of 2.

Conversely, let us assume that $\mathcal{C}$ satisfies the two conditions in
the statement. Consider any $f\colon X\to Y\in\mathcal{C}$, its kernel
congruence
$\textstyle{f/f\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f_{0}}$$\scriptstyle{f_{1}}$$\textstyle{X}$
and the coinserter $q\colon X\to Q$ in $\mathcal{C}$ of the latter, which
exists by condition 1. Since $ff_{0}\leq ff_{1}$, there exists a unique
$m\colon Q\to Y$ such that $f=mq$. It now suffices to show that $m$ is an
$\mathsf{ff}$-morphism.

For this, consider the kernel congruence
$\textstyle{m/m\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{0}}$$\scriptstyle{m_{1}}$$\textstyle{Q}$
and form the following diagram where the bottom right-hand square is a comma
and the other three are pullbacks.

$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v_{1}}$$\scriptstyle{v_{0}}$$\textstyle{P_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{x_{1}}$$\scriptstyle{u_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{P_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u_{0}}$$\scriptstyle{x_{0}}$$\textstyle{m/m\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m_{1}}$$\scriptstyle{m_{0}}$$\scriptstyle{\leq}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{Y}$

Similarly to the proof of 2, we have $P\cong f/f$ and we can assume that
$x_{0}v_{0}=f_{0}$ and $x_{1}v_{1}=f_{1}$. Furthermore, by the assumed
stability of effective morphisms under pullback, we can deduce that
$u_{0}v_{0}=u_{1}v_{1}$ is an order-epimorphism. Now we have that

$m_{0}u_{0}v_{0}=qx_{0}v_{0}=qf_{0}\leq qf_{1}=qx_{1}v_{1}=m_{1}u_{1}v_{1}$

whence we deduce that $m_{0}\leq m_{1}$ and so that $m$ is an
$\mathsf{ff}$-morphism. ∎

To end this section, let us list a few examples of regular categories. For
more details on most of these one can consult [14].

  * 2.19 Example.

    1. (1)

$\mathsf{Pos}$ is regular as a $\mathsf{Pos}$-category. So is any category of
enriched presheaves $[\mathcal{C}^{op},\mathsf{Pos}]$ for $\mathcal{C}$ a
small category.

    2. (2)

Any ordinary regular category $\mathcal{C}$ is also regular in the
$\mathsf{Pos}$-enriched sense when equipped with the discrete order on its
Hom-sets. Indeed, in this case $\mathsf{ff}$-morphisms coincide with
monomorphisms and $\mathsf{so}$-morphisms with strong epimorphisms. Note that
$\mathsf{Pos}$ is an example of a category which is not regular in the
ordinary sense, but is regular as an enriched category.

    3. (3)

_Quasivarieties of ordered algebras_ in the sense of Bloom and Wright[5] are
regular categories[14]. As particular examples here we have the categories
$\mathsf{OrdMon}$ of ordered monoids, $\mathsf{OrdSGrp}$ of ordered semi-
groups, $\mathsf{OrdCMon}$ of commutative ordered monoids and
$\mathsf{OrdMon_{0}}$ of ordered monoids with the neutral element $0$ of the
monoid operation as the minimum element for the order. These are all in fact
varieties. An example of a quasivariety which is not a variety is the category
$\mathsf{OrdMon_{can}}$ of cancellative monoids, i.e. those ordered monoids
$(M,\cdot,\leq)$ satisfying the implications $x\cdot z\leq y\cdot z\implies
x\leq y$ and $z\cdot x\leq z\cdot y\implies x\leq y$ for all $x,y,z\in M$.

    4. (4)

The categories $\mathsf{Nach}$ of _Nachbin_ spaces (or compact ordered spaces)
and $\mathsf{Pries}$ of _Priestley_ spaces with continuous order-preserving
functions in both instances are examples of regular categories. We shall have
more to say on these in section 5.

    5. (5)

If $\mathcal{C}$ is monadic over $\mathsf{Pos}$ for a monad
$T\colon\mathsf{Pos}\to\mathsf{Pos}$ which preserves $\mathsf{so}$-morphisms
(i.e. surjections), then $\mathcal{C}$ is regular. An example of this kind is
given by the category $S$-$\mathsf{Pos}$ of $S$-posets for any ordered monoid
$S$ (see [8]). The objects in the latter category are monoid actions $S\times
X\to X$ on a poset $X$ which are monotone in both variables, while the
morphisms are the monotone equivariant functions.

##  3\. Calculus of Relations and Exactness

Recall that in an ordinary regular category $\mathcal{C}$, the existence of a
stable (regular epi,mono) factorization system allows for a well-behaved
calculus of relations in $\mathcal{C}$. More precisely, the existence of the
factorization system allows one to define the composition of two internal
relations and then the stability of regular epimorphisms under pullback is
precisely equivalent to the associativity of this composition. Essentially the
same facts hold also in our $\mathsf{Pos}$-enriched setting.

If $\mathcal{E}$ is a regular category, then by a _relation_ in $\mathcal{E}$
we shall mean an order-subobject $R\rightarrowtail X\times Y$, i.e. a
subobject of a product represented by an $\mathsf{ff}$-morphism. We shall
write $R\colon X\looparrowright Y$ to denote that $R$ is a relation from $X$
to $Y$ in $\mathcal{E}$. The factorization system
($\mathsf{so}$,$\mathsf{ff}$) in $\mathcal{E}$ and the stability of
$\mathsf{so}$-morphisms under pullback allow us to have a well-defined
composition of relations in $\mathcal{E}$: given $R\colon X\looparrowright Y$
and $S\colon Y\looparrowright Z$ in $\mathcal{C}$, the relation $S\circ
R\colon X\looparrowright Z$ is defined by first constructing the pullback
square below

$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t_{0}}$$\scriptstyle{t_{1}}$$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{0}}$$\scriptstyle{r_{1}}$$\textstyle{S\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s_{0}}$$\scriptstyle{s_{1}}$$\textstyle{X}$$\textstyle{Y}$$\textstyle{Z}$

and then taking the ($\mathsf{so}$,$\mathsf{ff}$) factorization of $\langle
r_{0}t_{0},s_{1}t_{1}\rangle\colon T\to X\times Z$, say

$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{M\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
m_{0},m_{1}\rangle}$$\textstyle{X\times Z}$

In other words, in our notation $S\circ R$ is the relation represented by the
$\mathsf{ff}$-morphism $\langle m_{0},m_{1}\rangle$.

This leads to the locally posetal bicategory (a.k.a $\mathsf{Pos}$-category)
$\mathrm{Rel}(\mathcal{E})$, whose objects are those of $\mathcal{E}$ and
whose morphisms are the relations $R\colon X\looparrowright Y$ in
$\mathcal{E}$. The identity morphism on the object $X$ in
$\mathrm{Rel}(\mathcal{E})$ is the diagonal relation $\langle
1_{X},1_{X}\rangle\colon\Delta_{X}\rightarrowtail X\times X$ and composition
of morphisms is given by composition of relations in $\mathcal{E}$.

If we forget about the 2-dimensional nature of the properties that define the
two classes of morphisms in the factorization system
($\mathsf{so}$,$\mathsf{ff}$), then the structure and basic properties of
$\mathrm{Rel}(\mathcal{E})$ are essentially the calculus of relations
_relative to a stable factorization system_ , as explicated by Meisen [17],
Richter[20], Kelly[12] and others. Thus, we shall feel free to take for
granted many of the basic facts concerning the structure of
$\mathrm{Rel}(\mathcal{E})$ without proving them here. As an exception to this
rule, we include the proof of the following lemma because it describes a way
in which one can argue about relations in a regular category using generalized
elements which will be particularly useful to us in subsequent proofs. Recall
here that, given a relation $R\colon X\looparrowright Y$ and generalized
elements $x\colon A\to X$, $y\colon A\to Y$ in $\mathcal{E}$, we write
$(x,y)\in_{A}R$ to indicate that $\langle x,y\rangle\colon A\to X\times Y$
factors through $\langle r_{0},r_{1}\rangle$. Observe also that, given an
$\mathsf{so}$-morphism $q\colon B\twoheadrightarrow A$ in $\mathcal{E}$, we
have that $(x,y)\in_{A}R$ if and only if $(xq,yq)\in_{B}R$. Indeed, while the
“only if” direction is obvious, for the converse note that $(xq,yq)\in_{B}R$
means the existence of a commutative square of the following form.

${B}$${A}$${R}$${X\times Y}$$\scriptstyle{q}$$\scriptstyle{\langle
x,y\rangle}$

Then by the orthogonality between $\mathsf{so}$ and $\mathsf{ff}$-morphisms we
have an induced diagonal $A\to R$ exhibiting $(x,y)\in_{A}R$.

  * 3.1 Lemma.

Let $R\colon X\looparrowright Y$ and $S\colon Y\looparrowright Z$ be relations
in a regular category $\mathcal{E}$ and consider any generalized elements
$x\colon P\to X$ and $z\colon P\to Z$. Then $(x,z)\in_{P}S\circ R$ if and only
if there exists an effective epimorphism $q\colon Q\twoheadrightarrow P$ and a
generalized element $y\colon Q\to Y$ such that $(xq,y)\in_{Q}R$ and
$(y,zq)\in_{Q}S$.

###### Proof.

Consider the diagram below, where the square is a pullback.

$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{t_{0}}$$\scriptstyle{t_{1}}$$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{0}}$$\scriptstyle{r_{1}}$$\textstyle{S\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s_{0}}$$\scriptstyle{s_{1}}$$\textstyle{X}$$\textstyle{Y}$$\textstyle{Z}$

Then $S\circ R$ is given by the following image factorization

$\langle r_{0}t_{0},s_{1}t_{1}\rangle=\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.61632pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
18.97363pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{e}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 41.61636pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise 0.0pt\hbox{\hbox{\kern-1.99997pt\lower
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
41.61636pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{I\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
52.7969pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
57.52425pt\raise 8.0pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern 0.0pt\raise-2.5pt\hbox{$\scriptstyle{\langle
i_{0},i_{1}\rangle}$}}}\kern 3.0pt}}}}}}\ignorespaces{\hbox{\kern
87.79695pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}{\hbox{\kern
87.79695pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{X\times
Z}$}}}}}}}\ignorespaces\ignorespaces}}}}$

.

Assume first that $(x,z)\in_{P}S\circ R$, i.e. there exists a morphism
$u\colon P\to I$ such that $\langle i_{0},i_{1}\rangle u=\langle x,z\rangle$.
We then form the pullback square below.

$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{v}$$\scriptstyle{q}$$\textstyle{P\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u}$$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e}$$\textstyle{I}$

Note that $q$ is an effective epimorphism because $e$ is such. Now set
$y\coloneqq r_{1}t_{0}v=s_{0}t_{1}v\colon Q\to Y$. Then $\langle
xq,y\rangle=\langle i_{0}uq,r_{1}t_{0}v\rangle=\langle
i_{0}ev,r_{1}t_{0}v\rangle=\langle r_{0}t_{0}v,r_{1}t_{0}v\rangle=\langle
r_{0},r_{1}\rangle t_{0}v$ and $\langle y,zq\rangle=\langle
s_{0}t_{1}v,i_{1}uq\rangle=\langle s_{0}t_{1}v,i_{1}ev\rangle=\langle
s_{0}t_{1}v,s_{1}t_{1}v\rangle=\langle s_{0},s_{1}\rangle t_{1}v$, so that
$(xq,y)\in_{Q}R$ and $(y,zq)\in_{Q}S$.

Conversely, assume that $(xq,y)\in_{Q}R$ and $(y,zq)\in_{Q}S$ for some
$y\colon Q\to Y$ and effective epimorphism $q\colon Q\twoheadrightarrow P$.
This means that there exist morphisms $u\colon Q\to R$ and $v\colon Q\to S$
such that $\langle r_{0},r_{1}\rangle u=\langle xq,y\rangle$ and $\langle
s_{0},s_{1}\rangle v=\langle y,zq\rangle$. Since $r_{1}u=y=s_{0}v$, there
exists a unique $w\colon Q\to T$ such that $t_{0}w=u$ and $t_{1}w=v$. Then
$\langle i_{0},i_{1}\rangle ew=\langle r_{0}t_{0},s_{1}t_{1}\rangle w=\langle
r_{0}u,s_{1}v\rangle=\langle xq,zq\rangle$, so that $(xq,zq)\in_{Q}SR$. Since
$q$ is an $\mathsf{so}$-morphism, we can conclude that also $(x,z)\in_{P}SR$.
∎

The above lemma can actually be used to prove many of the fundamental
properties of $\rm{Rel}(\mathcal{E})$. In general, $\rm{Rel}(\mathcal{E})$ is
a _tabular allegory with a unit_ (see e.g. [10],[9]), where the anti-
involution
$(-)^{\circ}\colon\mathrm{Rel}(\mathcal{E})^{op}\to\mathrm{Rel}(\mathcal{E})$
is given by taking the _opposite_ relation. In particular, we have that
Freyd’s _Modular Law_ holds in $\mathrm{Rel}(\mathcal{E})$, i.e.

$QP\cap S\subseteq Q(P\cap Q^{\circ}S)$

for any relations $P\colon X\looparrowright Y$, $Q\colon Y\looparrowright Z$
and $S\colon X\looparrowright Z$ in $\mathcal{E}$. The presence of the anti-
involution $(-)^{\circ}$ implies that the Modular Law is equivalent to its
dual form, namely the inclusion

$QP\cap S\subseteq(Q\cap SP^{\circ})P$

for any relations $P,Q,S$ as above.

Every morphism $f\colon X\to Y\in\mathcal{E}$ defines a relation
$X\looparrowright Y$ represented by the ff-morphism $\langle
1_{X},f\rangle\colon X\to X\times Y$, which we call its _graph_ and denote by
the same letter. This assignment defines a faithful ordinary functor
$\mathcal{E}_{0}\to\mathrm{Rel}(\mathcal{E})$ on the underlying ordinary
category of $\mathcal{E}$ which is the identity on objects. Furthermore, in
$\mathrm{Rel}(\mathcal{E})$ we have an adjunction $f\dashv f^{\circ}$, which
means that the inclusions $f^{\circ}f\supseteq\Delta_{X}$ and
$ff^{\circ}\subseteq\Delta_{Y}$ hold. We say then that the morphisms of
$\mathcal{E}$ are _maps_ in the bicategory $\mathrm{Rel}(\mathcal{E})$. We
should perhaps stress here that taking the graph of a morphism does not define
a functor $\mathcal{E}\to\mathrm{Rel}(\mathcal{E})$ because the order of
morphisms is not preserved. In fact, since $\mathrm{Rel}(\mathcal{E})$ is an
allegory, the anti-involution $(-)^{\circ}$ forces any inclusion $f\subseteq
g$ for morphisms $f,g\colon X\to Y$ to be an equality (see e.g. A3.2.3 in
[10]).

The modular law also implies some restricted versions of distributivity of
composition over binary intersections in $\mathrm{Rel}(\mathcal{E})$ (see e.g.
A3.1.6 of [10]). Two particular instances of this which we would like to
explicitly record for future reference are the following:

$(R\cap S)f=Rf\cap Sf$ $g^{\circ}(R\cap S)=g^{\circ}R\cap g^{\circ}S$

where $R,S$ are relations $Y\looparrowright Z$ and $f\colon X\to Y$ and
$g\colon X\to Z$ are morphisms in $\mathcal{E}$.

While $\mathrm{Rel}(\mathcal{E})$ is a very useful category in terms of
performing calculations with relations in $\mathcal{E}$, it does not really
capture the enriched nature of $\mathcal{E}$. As we have mentioned earlier,
$\mathrm{Rel}(\mathcal{E})$ in some sense only involves an ordinary category
with a stable factorization system. In order to also capture the
$\mathsf{Pos}$-enriched aspects of a regular category $\mathcal{E}$ we will
also need to work in a different bicategory of relations. In terms of our
goals in this paper, this need is related to our desire to identify the
morphisms of $\mathcal{E}$ as the maps in a certain bicategory of relations,
thus generalizing a familiar fact for ordinary regular categories. Indeed,
while certainly any morphism $f\colon X\to Y\in\mathcal{E}$ has as its right
adjoint in $\mathrm{Rel}(\mathcal{E})$ the opposite relation $f^{\circ}$, this
is not a complete characterization of (graphs of) morphisms. As can be deduced
by arguments essentially contained in [12], being a map in
$\mathrm{Rel}(\mathcal{E})$ is a weaker property than being the graph of a
morphism in $\mathcal{E}$.

Another reason for moving to a different bicategory of relations is dictated
by the form of _congruences_ in this enriched setting and the way in which
exactness is defined. This will become apparent a little bit later.

  * 3.2 Definition.

A relation $R\colon X\looparrowright Y$ in the regular category $\mathcal{E}$
is called _weakening_ or _weakening-closed_ if, whenever $x,x^{\prime}\colon
A\to X$ and $y,y^{\prime}\colon A\to Y$ are generalized elements in
$\mathcal{E}$, the following implication holds

$x^{\prime}\leq x\hskip 2.84526pt\wedge\hskip 2.84526pt(x,y)\in_{A}R\hskip
2.84526pt\wedge\hskip 2.84526pty\leq
y^{\prime}\implies(x^{\prime},y^{\prime})\in_{A}R$

  * 3.3 Remark.

The property of a relation being weakening-closed can be viewed as an order-
compatibility condition, especially if one thinks of a relation $R\colon X\to
Y$ in this poset-enriched context as specifying that certain elements of $X$
are less than or equal to certain elements of $Y$. If one follows the
terminology of 2-category theory, as the authors of [14] do, this property
would be referred to by saying that $R$ is a _two-sided discrete fibration_.
Since we have generally chosen to not really stress the 2-categorical
viewpoint in this paper, we have accordingly adopted the above terminology
which is inspired from logic.

For any given object $X\in\mathcal{E}$, there is a weakening-closed relation
$I_{X}\colon X\looparrowright X$ given by the comma $I_{X}\coloneqq
1_{X}/1_{X}$. Then it is easy to see that a relation $R\colon X\looparrowright
Y$ is weakening-closed if and only if we have $R=I_{Y}RI_{X}$ in
$\mathrm{Rel}(\mathcal{E})$. In particular, the relations $I_{X}$ act as
identity elements for composition of weakening-closed relations. Thus, we can
define a bicategory $\mathrm{Rel}_{w}(\mathcal{E})$ where the objects are
again those of $\mathcal{E}$ but now the morphisms are the weakening-closed
relations.

  * 3.4 Remark.

Perhaps we should note here that, although every morphism of
$\mathrm{Rel}_{w}(\mathcal{E})$ is also a morphism in
$\mathrm{Rel}(\mathcal{E})$ and composition in both categories is the same,
this is not a functorial inclusion
$\mathrm{Rel}_{w}(\mathcal{E})\hookrightarrow\mathrm{Rel}(\mathcal{E})$
because identity morphisms are not preserved.

Now to any given morphism $f\colon X\to Y\in\mathcal{E}$ we can canonically
associate two weakening-closed relations $f_{*}\colon X\looparrowright Y$ and
$f^{*}\colon Y\looparrowright X$ via the following commas: $f_{*}\coloneqq
f/1_{Y}$ and $f^{*}\coloneqq 1_{Y}/f$. We sometimes call $f_{*}$ and $f^{*}$
the _hypergraph_ and _hypograph_ of $f$ respectively. In terms of generalized
elements $x\colon A\to X$ and $y\colon A\to Y$ in $\mathcal{E}$ we have
$(x,y)\in_{A}f_{*}\iff fx\leq y$ and $(y,x)\in_{A}f^{*}\iff y\leq fx$.

The following are then easy to see, for example by arguing with generalized
elements.

  * 3.5 Lemma.

Let $\mathcal{E}$ be a regular category. Then for any $f\colon X\to Y$ and
$g\colon Y\to Z$ in $\mathcal{E}$ we have

    1. (1)

$(gf)_{*}=g_{*}f_{*}$.

    2. (2)

$(gf)^{*}=f^{*}g^{*}$.

It is also easy to see that, for any $f,g\colon X\to Y\in\mathcal{E}$, we have
equivalences

$f\leq g\iff g_{*}\subseteq f_{*}\iff f^{*}\subseteq g^{*}$

We can thus define two fully order-faithful functors
$(-)_{*}\colon\mathcal{E}^{co}\hookrightarrow\mathrm{Rel}_{w}(\mathcal{E})$
and
$(-)^{*}\colon\mathcal{E}^{op}\hookrightarrow\mathrm{Rel}_{w}(\mathcal{E})$,
where $\mathcal{E}^{co}$ denotes the “order-dual” category, i.e. the category
obtained from $\mathcal{E}$ by reversing the order on morphisms. Similarly,
arguing with generalized elements we easily deduce the following.

  * 3.6 Lemma.

For any $f\colon X\to Y$ in a regular category $\mathcal{E}$ we have
$f^{*}f_{*}=f/f$ as relations in $\mathcal{E}$.

In particular, we see that $f\colon X\to Y$ is an $\mathsf{ff}$-morphism in
$\mathcal{E}$ if and only if $f^{*}f_{*}=I_{X}$ in
$\mathrm{Rel}_{w}(\mathcal{E})$. Similarly, a pair of morphisms
${Y}$${X}$${Z}$$\scriptstyle{f}$$\scriptstyle{g}$ is jointly $\mathsf{ff}$
precisely when $f^{*}f_{*}\cap g^{*}g_{*}=I_{X}$.

Now just as the graph of every morphism $f\colon X\to Y$ induces an adjunction
$f\dashv f^{\circ}$ in $\rm{Rel}(\mathcal{E})$, so do the hypergraph and
hypograph of that morphism form an adjunction in the bicategory
$\rm{Rel}_{w}(\mathcal{E})$.

  * 3.7 Lemma.

For any $f\colon X\to Y$ in a regular category $\mathcal{E}$, there is an
adjunction $f_{*}\dashv f^{*}$ in $\mathrm{Rel}_{w}(\mathcal{E})$.

###### Proof.

We saw above that $f^{*}f_{*}$ is precisely the kernel congruence of $f$, so
clearly we have $I_{X}\subseteq f^{*}f_{*}$. To form the composition
$f_{*}f^{*}$ we consider the diagram below, where the top square is a pullback
and the other two are commas.

$\textstyle{Q\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q_{1}}$$\scriptstyle{q_{2}}$$\textstyle{f^{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{s_{1}}$$\scriptstyle{s_{2}}$$\textstyle{f_{*}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{r_{1}}$$\scriptstyle{r_{2}}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\leq}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{f}$$\scriptstyle{\leq}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y}$$\textstyle{Y}$

Now by definition we have that $f_{*}f^{*}$ is given by the image of $\langle
s_{1}q_{1},r_{2}q_{2}\rangle$. But $s_{1}q_{1}\leq fs_{2}q_{1}=fr_{1}q_{2}\leq
r_{2}q_{2}$, so that $\langle s_{1}q_{1},r_{2}q_{2}\rangle$ factors through
$I_{Y}=1_{Y}/1_{Y}$. This yields the inclusion $f_{*}f^{*}\subseteq I_{Y}$. ∎

In other words, every morphism $f\colon X\to Y$ in a regular category
$\mathcal{E}$ is a map in $\mathrm{Rel}_{w}(\mathcal{E})$ via its hypergraph
$f_{*}$. Our first result in this paper is that in any regular category
$\mathcal{E}$ this is now indeed a complete characterization of morphisms,
i.e. every map in $\rm{Rel}_{w}(\mathcal{E})$ is of the form $f_{*}$ for a
(necessarily unique) morphism $f\colon X\to Y\in\mathcal{E}$.

  * 3.8 Theorem.

If $\phi\colon X\looparrowright Y\in\rm{Rel}_{w}(\mathcal{E})$ has a right
adjoint in $\rm{Rel}_{w}(\mathcal{E})$, then there exists a (necessarily
unique) morphism $f\colon X\to Y\in\mathcal{E}$ such that $\phi=f_{*}$.

###### Proof.

Let $\psi\colon Y\looparrowright X\in\mathrm{Rel}_{w}(\mathcal{E})$ be the
right adjoint, so that we have $I_{X}\subseteq\psi\phi$ and $\phi\psi\subseteq
I_{Y}$. Suppose also that $\phi$ and $\psi$ are represented respectively by
the ff-morphisms $\langle\phi_{0},\phi_{1}\rangle\colon T\rightarrowtail
X\times Y$ and $\langle\psi_{0},\psi_{1}\rangle\colon
T^{\prime}\rightarrowtail Y\times X$. We next form the pullback square below,
so that
$\langle\phi_{0}u,\phi_{1}u\rangle=\langle\psi_{1}u^{\prime},\psi_{0}u^{\prime}\rangle\colon
S\rightarrowtail X\times Y$ represents the relation
$\phi\cap\psi^{\circ}\colon X\looparrowright Y\in\rm{Rel}(\mathcal{E})$. We
first want to show that $\phi_{0}u=\psi_{1}u^{\prime}$ is an isomorphism, in
which case we will have $\phi\cap\psi^{\circ}=f$ for the morphism
$f\coloneqq\phi_{1}u(\phi_{0}u)^{-1}\colon X\to Y$.

$\textstyle{S\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{u^{\prime}}$$\scriptstyle{u}$$\textstyle{T^{\prime}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle\psi_{1},\psi_{0}\rangle}$$\textstyle{T\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle\phi_{0},\phi_{1}\rangle}$$\textstyle{X\times
Y}$

First of all, since $I_{X}\subseteq\psi\phi$, we have
$(1_{X},1_{X})\in_{X}\psi\phi$ and hence there exist an effective epimorphism
$e\colon P\twoheadrightarrow X$ and a $y\colon P\to Y$ such that
$(e,y)\in_{P}\phi$ and $(y,e)\in_{P}\psi$. Then we have
$(e,y)\in_{P}\phi\cap\psi^{\circ}$ and so there exists a $v\colon P\to S$ such
that $\langle\phi_{0}u,\phi_{1}u\rangle v=\langle e,y\rangle$. In particular,
since $\phi_{0}uv=e$ is an effective epimorphism, we deduce that $\phi_{0}u$
is an effective epimorphism as well.

Now it suffices to show that $\phi_{0}u$ is also an $\mathsf{ff}$-morphism. So
let $a,b\colon A\to S$ be such that $\phi_{0}ua\leq\phi_{0}ub$. Then
$(\phi_{0}ua,\phi_{0}ub)\in_{A}I_{X}$ and hence
$(\phi_{0}ua,\phi_{0}ub)\in_{A}\psi\phi$, so there is an effective epimorphism
$e\colon P\twoheadrightarrow A$ and a $z\colon P\to Y$ such that
$(\phi_{0}uae,z)\in_{P}\phi$ and $(z,\phi_{0}ube)\in_{P}\psi$. Since we also
clearly have

$(\phi_{1}uae,\phi_{0}uae)=(\psi_{0}u^{\prime}ae,\psi_{1}u^{\prime}ae)\in_{P}\psi,$

we get $(\phi_{1}uae,z)\in_{P}\phi\psi$, which implies
$(\phi_{1}uae,z)\in_{P}I_{Y}$, i.e. that $\phi_{1}uae\leq z$.

Similarly, since $(\phi_{0}ube,\phi_{1}ube)\in_{P}\phi$ and
$(z,\phi_{0}ube)\in\psi$, we consequently have that
$(z,\phi_{1}ube)\in_{P}\phi\psi$ and hence $(z,\phi_{1}ube)\in_{P}I_{Y}$,
which is to say that $z\leq\phi_{1}ube$. We now have $\phi_{1}uae\leq
z\leq\phi_{1}ube$, hence $\phi_{1}uae\leq\phi_{1}ube$, which in turn implies
that $\phi_{1}ua\leq\phi_{1}ub$, because $e$ is an order-epimorphism. Since
also $\phi_{0}ua\leq\phi_{0}ub$, we obtain $a\leq b$ because
$\langle\phi_{0}u,\phi_{1}u\rangle$ is an $\mathsf{ff}$-morphism.

We now claim that $\phi=f_{*}$. To see this, observe first that
$f_{*}=I_{Y}f=I_{Y}(\phi\cap\psi^{\circ})\subseteq I_{Y}\phi=\phi$, where the
last equality follows because $\phi$ is weakening-closed. Thus,
$f_{*}\subseteq\phi$. But by an application of the modular law 3 in
$\mathrm{Rel}(\mathcal{E})$ we also have $\psi
f=\psi(\phi\cap\psi^{\circ})\supseteq\psi\phi\cap\Delta_{X}\supseteq
I_{X}\cap\Delta_{X}=\Delta_{X}$ and so that $\phi\psi f\supseteq\phi$. Then
$f_{*}=I_{Y}f\supseteq\phi\psi f\supseteq\phi$ and so we conclude that
$f_{*}=\phi$.

Finally, for the uniqueness claim let us assume that $f,g\colon X\to Y$ are
such that $f_{*}=g_{*}$. By an earlier observation we know that the inclusion
$f_{*}\subseteq g_{*}$ is equivalent to the inequality $g\leq f$. Then we have
both $f\leq g$ and $g\leq f$, whence $f=g$. ∎

Next, let us comment here on how the calculus of relations in a regular
category $\mathcal{E}$ can be used to express various limit properties
therein. For example, the statement that a pair of morphisms
${X}$${Z}$${Y}$$\scriptstyle{f}$$\scriptstyle{g}$ represents a given relation
$R\colon X\looparrowright Y$ is equivalent to the following two equalities
between relations:

  1. (1)

$R=gf^{\circ}$.

  2. (2)

$f^{*}f_{*}\cap g^{*}g_{*}=I_{Z}$.

Note here that we cannot replace condition (1.) by $R=g_{*}f^{*}$, even if $R$
is weakening-closed. Similarly, we cannot replace (2.) by $f^{\circ}f\cap
g^{\circ}g=\Delta_{Z}$, because the latter means that $(f,g)$ are only jointly
monomorphic instead of jointly order-monomorphic.

Based on the above observation, now consider the statement that a commutative
square

${P}$${Y}$${X}$${Z}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$$\scriptstyle{g}$$\scriptstyle{f}$

is a pullback. It is easy to see that this is equivalent to the following pair
of equalities:

  1. (1)

$g^{\circ}f=p_{1}p_{0}^{\circ}$.

  2. (2)

$p_{1}^{*}p_{1*}\cap p_{0}^{*}p_{0*}=I_{P}$.

Similarly, the statement that the square

${P}$${Y}$${X}$${Z}$$\scriptstyle{p_{1}}$$\scriptstyle{p_{0}}$${\leq}$$\scriptstyle{g}$$\scriptstyle{f}$

is a comma is equivalent to:

  1. (1)

$g^{*}f_{*}=p_{1}p_{0}^{\circ}$.

  2. (2)

$p_{1}^{*}p_{1*}\cap p_{0}^{*}p_{0*}=I_{P}$.

Now we turn to discussing exactness for $\mathsf{Pos}$-categories. First, let
us recall the definition of congruence relation from [14]. This can be seen as
the ordered analogue of equivalence relations in an ordinary category. It is
also a special case of a more general notion of congruence for 2-categories.

  * 3.9 Definition.

Let $X$ be an object of the regular category $\mathcal{E}$. A _congruence_ on
$X$ is a relation $E\colon X\looparrowright X\in\mathrm{Rel}_{w}(\mathcal{E})$
which is reflexive and transitive.

We say that the congruence $E$ is _effective_ if there exists a morphism
$f\colon X\to Y\in\mathcal{E}$ such that $E=f/f$.

Equivalently, we can say that $E\colon X\looparrowright X$ is a congruence if
it is a transitive relation such that $E\supseteq I_{X}$. In essence, a
congruence is a pre-order relation on $X$ which is compatible with the
canonical order relation on $X$, the latter expressed by the requirement that
it is weakening-closed. We think of a congruence as imposing additional
inequalities on $X$, just as an equivalence relation corresponds to the idea
of imposing new equalities.

With the notion of congruence in hand, we are lead naturally to the notion of
(Barr-)exactness for $\mathsf{Pos}$-categories as considered by Kurz-Velebil
in [14].

  * 3.10 Definition.

A regular category $\mathcal{E}$ is called _exact_ if every congruence in
$\mathcal{E}$ is effective.

  * 3.11 Example.

    1. (1)

$\mathsf{Pos}$ is exact and so is any presheaf category
$[\mathcal{C},\mathsf{Pos}]$ for any small category $\mathcal{C}$.

    2. (2)

The locally discrete category $\mathsf{Set}$ is an example of a category which
is regular but not exact (see [14]).

    3. (3)

Generalizing the case of $\mathsf{Pos}$, any _variety of ordered algebras_ ,
always in the sense of Bloom & Wright[5], is an exact category. Particular
examples here are furnished by the categories $\mathsf{OrdSGrp}$,
$\mathsf{OrdMon}$, $\mathsf{OrdMon_{0}}$ and $\mathsf{OrdCMon}$. On the other
hand, the quasivariety $\mathsf{OrdCMon_{t.f.}}$ is not exact.

    4. (4)

There are also examples of exact categories which are not varieties, but are
monadic over $\mathsf{Pos}$. One such, which will appear in more detail in
section 5, is the category $\mathsf{Nach}$ of Nachbin spaces. Another is given
by the category $S$-$\mathsf{Pos}$ for any ordered monoid $S$.

A congruence in a regular category $\mathcal{E}$, being a transitive relation,
is an idempotent when considered as a morphism in either of
$\mathrm{Rel}(\mathcal{E})$ and $\mathrm{Rel}_{w}(\mathcal{E})$. When it is
moreover effective, then it actually is a _split_ idempotent in the latter
bicategory. Indeed, if $E=f/f$ for some $f\colon X\to Y$, then we can assume
that $f$ is actually the coinserter of $E$ by 2. Then we have
$f^{*}f_{*}=f/f=E$ and $f_{*}f^{*}=I_{Y}$. The next proposition shows that
this splitting actually characterizes effective congruences. This is analogous
to a familiar fact for ordinary regular categories, where an equivalence
relation splits in the bicategory of relations if and only if it occurs as a
kernel pair.

  * 3.12 Proposition.

Let $E\colon X\looparrowright X$ be a congruence in the regular category
$\mathcal{E}$. Then $E$ is effective if and only if it splits as an idempotent
in $\mathrm{Rel}_{w}(\mathcal{E})$.

###### Proof.

Suppose that $E=\psi\phi$ for some $\phi\colon X\looparrowright Y$ and
$\psi\colon Y\looparrowright X$ in $\mathrm{Rel}_{w}(\mathcal{E})$ with
$\phi\psi=I_{Y}$. Since $E$ is reflexive and weakening-closed, we have
$\psi\phi=E\supseteq I_{X}$. Since also trivially $\phi\psi\subseteq I_{Y}$,
we have $\phi\dashv\psi$ in $\mathrm{Rel}_{w}(\mathcal{E})$ and so by 3 we
have that $\phi=f_{*}$ and $\psi=f^{*}$ for some morphism $f\colon X\to
Y\in\mathcal{E}$. Thus, we obtain $E=\psi\phi=f^{*}f_{*}=f/f$. ∎

In the following section we will embark on the goal of constructing the exact
completion $\mathcal{E}_{ex/reg}$ of a regular category $\mathcal{E}$ by a
process of splitting idempotents in a bicategory of relations and then taking
maps in the resulting bicategory. This is essentially an attempt to mimic the
construction of the ordinary exact completion of a regular category, as
initially described by Lawvere in [15] and then with more details for example
in [21], [9],[10], motivated by the combination of the two results contained
in 3 and 3.

However, even if the reader is not familiar with the construction of the
splitting of idempotents, the next proposition can serve as a type of
heuristic for coming up with the definition of morphisms in the completion
$\mathcal{E}_{ex/reg}$. It will also be of practical use a little bit later.
Recall here that in a regular category we say
$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{e_{0}}$$\scriptstyle{e_{1}}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{P}$
is an _exact sequence_ if $(e_{0},e_{1})$ is the kernel congruence of $p$ and
also $p$ is the coinserter of $(e_{0},e_{1})$. In terms of the calculus of
relations, exactness of the sequence is equivalent to the equalities
$p^{*}p_{*}=E$ and $p_{*}p^{*}=I_{P}$.

  * 3.13 Proposition.

Let
$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{P}$
and
$\textstyle{F\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{Y\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{q}$$\textstyle{Q}$
be exact sequences in the regular category $\mathcal{E}$. Then there is an
order-reversing bijection between the following:

    1. (1)

Morphisms $P\to Q$ in $\mathcal{E}$.

    2. (2)

Relations $R_{*}\colon X\looparrowright Y\in\mathrm{Rel}_{w}(\mathcal{E})$ for
which there exists another relation $R^{*}\colon Y\looparrowright
X\in\mathrm{Rel}_{w}(\mathcal{E})$ such that the following are satisfied:

       * –

$FR_{*}E=R_{*}$ and $ER^{*}F=R^{*}$.

       * –

$R^{*}R_{*}\supseteq E$ and $R_{*}R^{*}\subseteq F$.

###### Proof.

Consider first a morphism $r\colon P\to Q\in\mathcal{E}$. Set $R_{*}\coloneqq
q^{*}r_{*}p_{*}$ and $R^{*}\coloneqq p^{*}r^{*}q_{*}$. We have
$FR_{*}E=q^{*}q_{*}q^{*}r_{*}p_{*}p^{*}p_{*}=q^{*}r_{*}p_{*}=R_{*}$ and
similarly $ER^{*}F=p^{*}p_{*}p^{*}r^{*}q_{*}q^{*}q_{*}=p^{*}r^{*}q_{*}=R^{*}$.
In addition,
$R^{*}R_{*}=p^{*}r^{*}q_{*}q^{*}r_{*}p_{*}=p^{*}r^{*}I_{Q}r_{*}p_{*}=p^{*}r^{*}r_{*}p_{*}\supseteq
p^{*}p_{*}=E$ and $R_{*}R^{*}=q^{*}r_{*}p_{*}p^{*}r^{*}q_{*}\subseteq
q^{*}r_{*}r^{*}q_{*}\subseteq q^{*}q_{*}=F$.

Conversely, consider a relation $R_{*}$ as in (2.). Set $\phi\coloneqq
q_{*}R_{*}p^{*}$ and then also $\psi\coloneqq p_{*}R^{*}q^{*}$. Then for these
weakening-closed relations we have

$\psi\phi=p_{*}R^{*}q^{*}q_{*}R_{*}p^{*}\supseteq
p_{*}R^{*}R_{*}p^{*}\supseteq p_{*}Ep^{*}=I_{P}$
$\phi\psi=q_{*}R_{*}p^{*}p_{*}R^{*}q^{*}=q_{*}R_{*}ER^{*}q^{*}=q_{*}R_{*}R^{*}q^{*}\subseteq
q_{*}Fq^{*}=I_{Q}$

Thus, by 3 we have $\phi=r_{*}$ for a (unique) morphism $r\colon P\to Q$.

The fact that these two assignments are inverse to each other is expressed by
the two equalities $q_{*}q^{*}r_{*}p_{*}p^{*}=r_{*}$ and
$q^{*}q_{*}R_{*}p^{*}p_{*}=FR_{*}E=R_{*}$. ∎

Before ending this section, let us make a couple more observations on the
assignment $R_{*}\mapsto r$ from the last proposition. Note that, as the
notation suggests and the above proof exhibits, the relation $R_{*}$
corresponds to the hypergraph $r_{*}$ of a morphism $r\colon P\to Q$.
Specifically, $r$ is uniquely determined from $R_{*}$ by the equality
$r_{*}=q_{*}R_{*}p^{*}$. We would like to also record here a relation $R$ that
in some sense corresponds directly to the (graph of the) morphism $r$.

Given $R_{*}\colon X\looparrowright Y$ as in 3, set $R\coloneqq
R_{*}\cap(R^{*})^{\circ}\colon X\looparrowright Y$. Then we claim that
$r=qRp^{\circ}$. To see this, observe first that $qRp^{\circ}$ is also a map
in $\mathrm{Rel}(\mathcal{E})$ because

$(qRp^{\circ})^{\circ}qRp^{\circ}=pR^{\circ}q^{\circ}qRp^{\circ}\supseteq
pR^{\circ}Rp^{\circ}\supseteq p(E\cap E^{\circ})p^{\circ}=\Delta_{P}$
$(qRp^{\circ})(qRp^{\circ})^{\circ}=qRp^{\circ}pR^{\circ}q^{\circ}=qR(E\cap
E^{\circ})R^{\circ}q^{\circ}=qRR^{\circ}q^{\circ}\subseteq q(F\cap
F^{\circ})q^{\circ}=\Delta_{Q}$

Here we used the fact that in an exact sequence
$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{P}$
we have $E\cap E^{\circ}=p^{*}p_{*}\cap(p^{*}p_{*})^{\circ}=p^{\circ}p$, i.e.
$E\cap E^{\circ}$ is precisely the kernel pair of $p$. In addition, the
inclusions $R^{\circ}R\supseteq E\cap E^{\circ}$ and $RR^{\circ}\subseteq
F\cap F^{\circ}$ were used, the first of which is clear and the second follows
by the modular law (see the next section for details).

Now, finally, we have

$r=r_{*}\cap(r^{*})^{\circ}=q_{*}R_{*}p^{*}\cap(q^{*})^{\circ}(R^{*})^{\circ}(p_{*})^{\circ}\supseteq
q(R_{*}\cap(R^{*})^{\circ})p^{\circ}=qRp^{\circ}.$

But since we have an inclusion between two maps in the allegory
$\mathrm{Rel}(\mathcal{E})$, these maps must be equal. Hence, we conclude that
$r=qRp^{\circ}$.

##  4\. Exact Completion

In this section we come to the heart of this paper, which is the construction
of the exact completion of a regular $\mathsf{Pos}$-category $\mathcal{E}$.

The main idea is to try to perform a construction that mimics one of the ways
in which one can define the exact completion of an ordinary regular category
$\mathcal{C}$. Let us thus quickly recall this construction, as originally
suggested by Lawvere in [15]. We will also very much be drawing inspiration
from the presentation of Succi-Cruciani[21].

Given a regular ordinary category $\mathcal{C}$, one first performs a
_splitting of idempotents_ in the bicategory of relations
$\mathrm{Rel}(\mathcal{C})$. More precisely, one splits the class of
equivalence relations, which are indeed idempotent as morphisms in
$\mathrm{Rel}(\mathcal{C})$. This step yields a bicategory which, a
posteriori, is identified as the bicategory of relations
$\mathrm{Rel}(\mathcal{C}_{ex/reg})$ of the completion. The second step is
then to identify the completion itself, which can be done by taking the
category of maps in the bicategory produced by the first step.

We note that the idea for this construction of the exact completion can be
traced back to the following two observations, valid in any ordinary regular
category $\mathcal{C}$:

  1. (1)

An equivalence relation $E$ on an object $X\in\mathcal{C}$ is effective if and
only if it splits as an idempotent in $\mathrm{Rel}(\mathcal{C})$.

  2. (2)

The morphisms $f\colon X\to Y\in\mathcal{C}$ are precisely the maps in
$\mathrm{Rel}(\mathcal{C})$.

Accordingly, our hope to perform a $\mathsf{Pos}$-enriched version of this
construction hinges on the validity of enriched versions of the two
observations above, as contained respectively in 3 and 3. Hence, in our
context, we should first look at $\mathrm{Rel}_{w}(\mathcal{E})$, split the
idempotents therein which are congruences in $\mathcal{E}$, then finally take
the category of maps in the resulting bicategory.

The fact that we need to work with $\mathrm{Rel}_{w}(\mathcal{E})$ rather than
$\mathrm{Rel}(\mathcal{E})$ already presents some issues. As we have mentioned
earlier, $\mathrm{Rel}(\mathcal{E})$ has the structure of an allegory and it
is this fact that facilitates many computations. Furthermore, the theory of
allegories is well developed and in fact there is a precise correspondence
between ordinary regular and exact categories on the one hand and certain
classes of allegories on the other (see e.g. [10],[9]). On the contrary, the
structure of $\mathrm{Rel}_{w}(\mathcal{E})$ is not as rich. Fundamentally,
the process of taking the opposite of a relation does not restrict to
$\mathrm{Rel}_{w}(\mathcal{E})$. Thus, in our quest to construct the
$\mathsf{Pos}$-enriched exact completion as indicated above, we cannot simply
rely on the general theory of allegories. While this creates a complication,
at the same time it is in some sense to be expected. Indeed, allegories are in
some aspects too simple for our enriched context. For example, the only
inclusions between maps in an allegory are equalities and it is precisely this
fact that does not allow us to recover the order relation on morphisms from
$\mathrm{Rel}(\mathcal{E})$.

Motivated by the above, we embark towards our goal by first defining a
category $Q_{w}(\mathcal{E})$ by splitting the idempotents in
$\mathrm{Rel}_{w}(\mathcal{E})$ which are congruences in $\mathcal{E}$.
Explicitly, $Q_{w}(\mathcal{E})$ is defined as follows:

  * •

Objects of $Q_{w}(\mathcal{E})$ are pairs $(X,E)$, where $X$ is an object of
$\mathcal{E}$ and $E\colon X\looparrowright X$ is a congruence relation in
$\mathcal{E}$.

  * •

Morphisms $\Phi\colon(X,E)\to(Y,F)$ in $Q_{w}(\mathcal{E})$ are (weakening-
closed) relations $\Phi\colon X\looparrowright Y$ in $\mathcal{E}$ such that
$\Phi E=\Phi=F\Phi$ or equivalently $\Phi=F\Phi E$.

Composition in $Q_{w}(\mathcal{E})$ is composition of relations in
$\mathcal{E}$, while the identity morphism on $(X,E)\in Q_{w}(\mathcal{E})$ is
the relation $E$ itself. The morphisms are locally ordered by inclusion and it
is clear that $Q_{w}(\mathcal{E})$ also has binary infima of morphisms given
by intersection of relations in $\mathcal{E}$. Then we define a category
$\mathcal{E}_{ex/reg}$ by taking the maps in $Q_{w}(\mathcal{E})$.

  * 4.1 Definition.

$\mathcal{E}_{ex/reg}\coloneqq\mathrm{Map}(Q_{w}(\mathcal{E}))$.

Explicitly, $\mathcal{E}_{ex/reg}$ has the same objects as
$Q_{w}(\mathcal{E})$, while its morphisms are those
$R_{*}\colon(X,E)\to(Y,F)\in Q_{w}(\mathcal{E})$ for which there exists an
$R^{*}\colon(Y,F)\to(X,E)\in Q_{w}(\mathcal{E})$ such that
$R^{*}R_{*}\supseteq E$ and $R_{*}R^{*}\subseteq F$.

Note that $\mathcal{E}_{ex/reg}$ is not merely an ordinary category, but can
be made into a legitimate Pos-category by defining for any
$R_{*},S_{*}\colon(X,E)\to(Y,F)$ in $\mathcal{E}_{ex/reg}$

$R_{*}\leq S_{*}\vcentcolon\Leftrightarrow R_{*}\supseteq S_{*}$

the inclusion on the right-hand side being that of relations in $\mathcal{E}$.
This is clearly a partial order relation on Homs that is preserved by
composition. Observe furthermore that we can equivalently define the order
$R_{*}\leq S_{*}$ by requiring $R^{*}\subseteq S^{*}$ for the right adjoints.

We also have a canonical functor
$\Gamma\colon\mathcal{E}\to\mathcal{E}_{ex/reg}$ defined by mapping an object
$X\in\mathcal{E}$ to $(X,I_{X})$ and a morphism $f\colon X\to Y\in\mathcal{E}$
to its hypergraph $f_{*}\colon X\looparrowright Y$ considered as a morphism
$(X,I_{X})\to(Y,I_{Y})$. Note that $\Gamma$ is order-preserving and reflecting
by definition of the order on morphisms in $\mathcal{E}_{ex/reg}$.

  * 4.2 Remark.

We will consistently denote morphisms of $\mathcal{E}_{ex/reg}$ by a capital
letter with a lower asterisk and their right adjoint in $Q_{w}(\mathcal{E})$
by the same letter with an upper asterisk. This notation represents our
intuition that $R_{*}$ is the hyper-graph of the morphism $R$ and in some
sense we are working towards making this a precise statement. In particular,
we will denote the identity morphism $(X,E)\to(X,E)$ by $1_{(X,E)*}$, where as
relations in $\mathcal{E}$ we have $1_{(X,E)*}=E$ and $1_{(X,E)}^{*}=E$.

Our goal now in this section is to show that the category
$\mathcal{E}_{ex/reg}$ as defined above is the _exact completion_ of
$\mathcal{E}$ as a regular category. The category $Q_{w}(\mathcal{E})$ will be
seen in the end to be precisely the category of weakening-closed relations in
$\mathcal{E}_{ex/reg}$. Accordingly, the proofs of the various statements
about $\mathcal{E}_{ex/reg}$ later on in this section will be motivated by the
description of the various limit and exactness properties in terms of the
calculus of relations in a regular category. However, we know that such a
description cannot be achieved with only weakening-closed relations. Thus, it
will be convenient to construct also at the same time what will turn out to be
the bicategory of all relations in $\mathcal{E}_{ex/reg}$.

This leads us to define another bicategory $Q(\mathcal{E})$ as follows:

  * •

Objects of $Q(\mathcal{E})$ are again pairs $(X,E)$, where $E\colon
X\looparrowright X$ is a congruence relation in $\mathcal{E}$.

  * •

Morphisms $(X,E)\to(Y,F)$ in $Q(\mathcal{E})$ are relations $\Phi\colon
X\looparrowright Y$ in $\mathcal{E}$ such that $\Phi(E\cap
E^{\circ})=\Phi=(F\cap F^{\circ})\Phi$ or equivalently $(F\cap
F^{\circ})\Phi(E\cap E^{\circ})=\Phi$.

The composition of morphisms is that of relations in $\mathcal{E}$ while the
identity on $(X,E)\in Q(\mathcal{E})$ is $E\cap E^{\circ}$.

In other words, $Q(\mathcal{E})$ is the locally ordered bicategory obtained
from $\mathrm{Rel}(\mathcal{E})$ by splitting those idempotents of the form
$E\cap E^{\circ}$ for a congruence $E$ in $\mathcal{E}$. Notice that
idempotents of this form are equivalence relations in $\mathcal{E}$ and in
particular are symmetric. It then follows (see for example Theorem 3.3.4 in
[10]) that $Q(\mathcal{E})$ is an allegory, where the opposite of a morphism
is given by taking the opposite relation in $\mathcal{E}$.

Now we make some important observations regarding the connection between
morphisms of $Q_{w}(\mathcal{E})$ and $Q(\mathcal{E})$ and between maps in
these two bicategories. If the reader keeps in mind the intuition that these
two categories should respectively be $\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})$
and $\mathrm{Rel}(\mathcal{E}_{ex/reg})$, then these observations are to be
expected.

First, note that every morphism $\Phi\colon(X,E)\to(Y,F)$ in
$Q_{w}(\mathcal{E})$ can also be considered as a morphism in $Q(\mathcal{E})$,
since

$\Phi=\Delta_{Y}\Phi\Delta_{X}\subseteq(F\cap F^{\circ})\Phi(E\cap
E^{\circ})\subseteq F\Phi E=\Phi$

However, it is important to note as well that this assignment is not
functorial as it does not preserve the identity morphisms.

Second, to any map in $Q_{w}(\mathcal{E})$, i.e. to any morphism of
$\mathcal{E}_{ex/reg}$, we can associate in a natural way a map in
$Q(\mathcal{E})$ as follows.

  * 4.3 Lemma.

Consider any $R_{*}\colon(X,E)\to(Y,F)\in\mathcal{E}_{ex/reg}$ and define the
relation $\mathfrak{gr}(R_{*})\coloneqq R_{*}\cap(R^{*})^{\circ}\colon
X\looparrowright Y$ in $\mathcal{E}$. Then $\mathfrak{gr}(R_{*})$ is a map
$(X,E)\to(Y,F)$ in $Q(\mathcal{E})$.

###### Proof.

First, it is easy to see that $(F\cap F^{\circ})\mathfrak{gr}(R_{*})(E\cap
E^{\circ})=\mathfrak{gr}(R_{*})$. Indeed, we have

$\mathfrak{gr}(R_{*})=\Delta_{Y}\mathfrak{gr}(R_{*})\Delta_{X}\subseteq(F\cap
F^{\circ})\mathfrak{gr}(R_{*})(E\cap
E^{\circ})\subseteq(F\mathfrak{gr}(R_{*})E)\cap(F^{\circ}\mathfrak{gr}(R_{*})E^{\circ})$
$\subseteq FR_{*}E\cap
F^{\circ}(R^{*})^{\circ}E^{\circ}=R_{*}\cap(R^{*})^{\circ}=\mathfrak{gr}(R_{*})$

Second, to see that $\mathfrak{gr}(R_{*})$ is indeed a map in $Q(\mathcal{E})$
we argue as follows:

$\mathfrak{gr}(R_{*})\mathfrak{gr}(R_{*})^{\circ}=(R_{*}\cap(R^{*})^{\circ})((R_{*})^{\circ}\cap
R^{*})\subseteq R_{*}R^{*}\cap(R^{*})^{\circ}(R_{*})^{\circ}\subseteq F\cap
F^{\circ}$ $\displaystyle\mathfrak{gr}(R_{*})^{\circ}\mathfrak{gr}(R_{*})$
$\displaystyle=$ $\displaystyle(R_{*}^{\circ}\cap
R^{*})(R_{*}\cap(R^{*})^{\circ})=(R_{*}^{\circ}\cap
R^{*})((R_{*}\cap(R^{*})^{\circ})\cap R_{*})$ $\displaystyle=$
$\displaystyle(R_{*}^{\circ}\cap R^{*})((R_{*}^{\circ}\cap
R^{*})^{\circ}(E\cap E^{\circ})\cap R_{*})$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law}}}{{\supseteq}}$
$\displaystyle(E\cap E^{\circ})\cap(R_{*}^{\circ}\cap R^{*})R_{*}=(E\cap
E^{\circ})\cap(E^{\circ}R_{*}^{\circ}\cap R^{*})R_{*}$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law*}}}{{\supseteq}}$
$\displaystyle(E\cap E^{\circ})\cap E^{\circ}\cap R^{*}R_{*}\supseteq(E\cap
E^{\circ})\cap E^{\circ}\cap E$ $\displaystyle=$ $\displaystyle E\cap
E^{\circ}$

where for establishing the first and second inclusions we used the modular law
in $\mathrm{Rel}(\mathcal{E})$. ∎

Given a morphism $R_{*}\colon(X,E)\to(Y,F)\in\mathcal{E}_{ex/reg}$, we call
the relation $\mathfrak{gr}(R_{*})$ defined above the _graph_ of $R_{*}$.
Observe furthermore that $\mathfrak{gr}(R_{*})$ satisfies the following two
basic equalities:

$F\circ\mathfrak{gr}(R_{*})=R_{*}$ $\mathfrak{gr}(R_{*})^{\circ}\circ F=R^{*}$

Indeed, on one hand clearly $F\circ\mathfrak{gr}(R_{*})\subseteq
FR_{*}=R_{*}$. On the other hand we have

$\displaystyle F\circ\mathfrak{gr}(R_{*})$ $\displaystyle\supseteq
R_{*}R^{*}\mathfrak{gr}(R_{*})=R_{*}R^{*}(R_{*}\cap(R^{*})^{\circ})$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular
Law}}}{{\supseteq}}R_{*}(R^{*}R_{*}\cap E^{\circ})\supseteq R_{*}(E\cap
E^{\circ})\supseteq R_{*}$

The second equality follows in a similar fashion.

In fact, these two equalities characterize $\mathfrak{gr}(R_{*})$ in the
following sense: if the morphism $\Phi\colon(X,E)\to(Y,F)$ is a map in
$Q(\mathcal{E})$ with $F\Phi=R_{*}$ and $\Phi^{\circ}F=R^{*}$, then
$\Phi=\mathfrak{gr}(R_{*})$. Indeed,

$\Phi\subseteq(F\cap F^{\circ})\Phi\subseteq F\Phi\cap
F^{\circ}\Phi=F\Phi\cap(\Phi^{\circ}F)^{\circ}=R_{*}\cap(R^{*})^{\circ}=\mathfrak{gr}(R_{*})$

and so $\Phi=\mathfrak{gr}(R_{*})$ because $Q(\mathcal{E})$ is an allegory and
hence the inclusion of maps is discrete.

Finally, the assignment $R_{*}\mapsto\mathfrak{gr}(R_{*})$ is functorial.
Given $R_{*}\colon(X,E)\to(Y,F)$ and $S_{*}\colon(Y,F)\to(Z,G)$ we have

$G(\mathfrak{gr}(S_{*})\mathfrak{gr}(R_{*}))=(G\mathfrak{gr}(S_{*}))\mathfrak{gr}(R_{*})=S_{*}\mathfrak{gr}(R_{*})=S_{*}F\mathfrak{gr}(R_{*})=S_{*}R_{*}$
$(\mathfrak{gr}(S_{*})\mathfrak{gr}(R_{*}))^{\circ}G=\mathfrak{gr}(R_{*})^{\circ}\mathfrak{gr}(S_{*})^{\circ}G=\mathfrak{gr}(R_{*})^{\circ}S^{*}=\mathfrak{gr}(R_{*})^{\circ}FS^{*}=R^{*}S^{*},$

so we conclude by the above observation that
$\mathfrak{gr}(S_{*})\mathfrak{gr}(R_{*})=\mathfrak{gr}(S_{*}R_{*})$. Also,
$\mathfrak{gr}(1_{(X,E)*})=1_{(X,E)*}\cap(1_{(X,E)}^{*})^{\circ}=E\cap
E^{\circ}$ and the latter is an identity morphism in
$\mathrm{Map}(Q(\mathcal{E}))$.

  * 4.4 Remark.

(on notation) Henceforth, to ease the notation, we shall often denote the
graph $\mathfrak{gr}(R_{*})$ of a morphism
$R_{*}\colon(X,E)\to(Y,E)\in\mathcal{E}_{ex/reg}$ simply by $R$, i.e. we will
just drop the lower asterisk. This shall not present too much risk for
confusion as $R_{*}$ will always have appeared before $R$.

We now begin our work on proving that $\mathcal{E}_{ex/reg}$ is indeed the
desired exact completion of the regular category $\mathcal{E}$. This is broken
down into a sequence of more bite-sized pieces. First, we establish a
fundamental result asserting the existence of certain canonical
representations for morphisms in the bicategories $Q_{w}(\mathcal{E})$ and
$Q(\mathcal{E})$. Following this, we repeatedly employ this representation to
establish step by step that $\mathcal{E}_{ex/reg}$ has the desired finite
limit and exactness properties making it an exact category. The arguments here
are essentially motivated by the description of these properties in terms of
the calculus of relations. Finally, we show that we have indeed constructed
the exact completion by establishing the relevant universal property.

To begin with, we record a small lemma concerning jointly order-monomorphic
pairs of morphisms in $\mathcal{E}_{ex/reg}$.

  * 4.5 Lemma.

If
$\textstyle{(Y,F)}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\scriptstyle{S_{*}}$$\textstyle{(Z,G)}$
is a pair of morphisms in the category $\mathcal{E}_{ex/reg}$ such that
$R^{*}R_{*}\cap S^{*}S_{*}=E$, then this pair is jointly order-monomorphic in
$\mathcal{E}_{ex/reg}$.

###### Proof.

Assume that $R^{*}R_{*}\cap S^{*}S_{*}=E$ and let
$H_{*},K_{*}\colon(A,T)\to(X,E)\in\mathcal{E}_{ex/reg}$ be such that
$R_{*}H_{*}\leq R_{*}K_{*}$ and $S_{*}H_{*}\leq S_{*}K_{*}$ i.e.
$R_{*}H_{*}\supseteq R_{*}K_{*}$ and $S_{*}H_{*}\supseteq S_{*}K_{*}$. Then we
have

$\displaystyle K_{*}H^{*}$ $\displaystyle=$ $\displaystyle
EK_{*}H^{*}=(R^{*}R_{*}\cap S^{*}S_{*})K_{*}H^{*}\subseteq
R^{*}R_{*}K_{*}H^{*}\cap S^{*}S_{*}K_{*}H^{*}$ $\displaystyle\subseteq$
$\displaystyle R^{*}R_{*}H_{*}H^{*}\cap S^{*}S_{*}H_{*}H^{*}\subseteq
R^{*}R_{*}\cap S^{*}S_{*},$

hence $K_{*}H^{*}\subseteq E$. But recall that by definition of morphisms we
have an adjunction $H_{*}\dashv H^{*}$ in $Q_{w}(\mathcal{E})$. Thus,
$K_{*}H^{*}\subseteq E\iff K_{*}\subseteq H_{*}$, so that we obtain $H_{*}\leq
K_{*}$. ∎

The result that follows will be of central importance in establishing all the
desired properties of $\mathcal{E}_{ex/reg}$ throughout the remainder of this
section. It says that any morphism of $Q(\mathcal{E})$ (hence also of
$Q_{w}(\mathcal{E})$) can be expressed in a suitable way via morphisms of
$\mathcal{E}_{ex/reg}$. This should be compared to the fact that in any
regular category $\mathcal{C}$ every relation $R\colon X\looparrowright Y$ can
be written as $R=gf^{\circ}$, where $f\colon Z\to X$ and $g\colon Z\to Y$ are
morphisms in $\mathcal{C}$ with $f^{*}f_{*}\cap g^{*}g_{*}=I_{Z}$. Actually,
our goal is to show in the end that it is _precisely_ this fact, since we will
prove that $Q(\mathcal{E})$ is exactly the bicategory of relations of
$\mathcal{E}_{ex/reg}$, while $Q_{w}(\mathcal{E})$ will be that of weakening-
closed relations.

  * 4.6 Proposition.

Let $\Phi\colon(X,E)\to(Y,F)$ be a morphism of $Q(\mathcal{E})$. Then there
exists a pair of morphisms
$\textstyle{(X,E)}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$ such that

    1. (1)

$\Phi=R_{1}R_{0}^{\circ}$.

    2. (2)

$R_{0}^{*}R_{0*}\cap R_{1}^{*}R_{1*}=T$.

Moreover, any pair $(R_{0*},R_{1*})$ with these two properties has the
following universal property:

Given any morphisms
$\textstyle{(X,E)}$$\textstyle{(C,G)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\scriptstyle{S_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$ such that $S_{1}S_{0}^{\circ}\subseteq\Phi$, there
exists a unique morphism $H_{*}\colon(C,G)\to(Z,T)\in\mathcal{E}_{ex/reg}$
with $R_{0*}H_{*}=S_{0*}$ and $R_{1*}H_{*}=S_{1*}$.

###### Proof.

Suppose that $\Phi$ is represented by the $\mathsf{ff}$-morphism $\langle
r_{0},r_{1}\rangle\colon Z\rightarrowtail X\times Y$ in $\mathcal{E}$. We set
$T\coloneqq r_{0}^{\circ}Er_{0}\cap r_{1}^{\circ}Fr_{1}$ and $R_{0*}\coloneqq
Er_{0}$, $R_{1*}\coloneqq Fr_{1}$. The relations $r_{0}^{\circ}Er_{0}$ and
$r_{1}^{\circ}Fr_{1}$ are inverse images along $r_{0},r_{1}$ respectively of
the congruences $E,F$, hence are themselves congruences. Thus, so is their
intersection $T$.

Also, we claim that that $R_{0*}$ and $R_{1*}$ as defined above are morphisms
$\textstyle{(X,E)}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$. Let’s check this for $R_{0*}$: first, we have
$ER_{0*}=EEr_{0}=Er_{0}=R_{0*}$. Furthermore,

$R_{0*}T=Er_{0}(r_{0}^{\circ}Er_{0}\cap r_{1}^{\circ}Fr_{1})\subseteq
Er_{0}r_{0}^{\circ}Er_{0}\subseteq E\Delta_{X}Er_{0}=EEr_{0}=Er_{0}=R_{0*},$

hence $R_{0*}T=R_{0*}$. So $R_{0*}$ is at least a morphism in
$Q_{w}(\mathcal{E})$. To show that it is actually a map, define
$R_{0}^{*}\coloneqq r_{0}^{\circ}E$. We then similarly have

$TR_{0}^{*}=(r_{0}^{\circ}Er_{0}\cap
r_{1}^{\circ}Fr_{1})r_{0}^{\circ}E\subseteq
r_{0}^{\circ}Er_{0}r_{0}^{\circ}E\subseteq
r_{0}^{\circ}EE=r_{0}^{\circ}E=R_{0}^{*}\implies TR_{0}^{*}=R_{0}^{*}$

and $R_{0}^{*}E=r_{0}^{\circ}EE=r_{0}^{\circ}E=R_{0}^{*}$. And finally,
$R_{0}^{*}R_{0*}=r_{0}^{\circ}EEr_{0}=r_{0}^{\circ}Er_{0}\supseteq T$ and
$R_{0*}R_{0}^{*}=Er_{0}r_{0}^{\circ}E\subseteq EE=E$.

Similarly, it follows that $R_{1*}$ is a morphism
$(Z,T)\to(Y,F)\in\mathcal{E}_{ex/reg}$ whose right adjoint in
$Q_{w}(\mathcal{E})$ is $R_{1}^{*}\coloneqq r_{1}^{\circ}F$.

Just by the definitions, we have

$R_{0}^{*}R_{0*}\cap R_{1}^{*}R_{1*}=r_{0}^{\circ}EEr_{0}\cap
r_{1}^{\circ}FFr_{1}=r_{0}^{\circ}Er_{0}\cap r_{1}^{\circ}Fr_{1}=T.$

In addition,
$R_{0}=R_{0*}\cap(R_{0}^{*})^{\circ}=Er_{0}\cap(r_{0}^{\circ}E)^{\circ}=Er_{0}\cap
E^{\circ}r_{0}\stackrel{{\scriptstyle\ref{Map distributivity}}}{{=}}(E\cap
E^{\circ})r_{0}$ and similarly $R_{1}=(F\cap F^{\circ})r_{1}$, so that

$R_{1}R_{0}^{\circ}=(F\cap F^{\circ})r_{1}r_{0}^{\circ}(E\cap
E^{\circ})=(F\cap F^{\circ})\Phi(E\cap E^{\circ})=\Phi.$

where the last equality holds because $\Phi\in Q(\mathcal{E})$.

Next, we have to prove the stated universality property, so let
$\textstyle{(X,E)}$$\textstyle{(C,G)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\scriptstyle{S_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$ be such that $S_{1}S_{0}^{\circ}\subseteq\Phi$.

Set $H_{*}\coloneqq R_{0}^{*}S_{0*}\cap R_{1}^{*}S_{1*}$ and $H^{*}\coloneqq
S_{0}^{*}R_{0*}\cap S_{1}^{*}R_{1*}$. Since, both $H_{*}$, $H^{*}$ are binary
intersections of compositions of morphisms in $Q_{w}(\mathcal{E})$, it is
immediate that they are both themselves morphisms in that bicategory. We will
show that $H_{*}$ is moreover a map with $H^{*}$ as its right adjoint.

First of all, we have that

$H_{*}H^{*}\subseteq R_{0}^{*}S_{0*}S_{0}^{*}R_{0*}\cap
R_{1}^{*}S_{1*}S_{1}^{*}R_{1*}\subseteq R_{0}^{*}ER_{0*}\cap
R_{1}^{*}FR_{1*}=R_{0}^{*}R_{0*}\cap R_{1}^{*}R_{1*}=T$

For the other inclusion we argue as follows:

$\displaystyle H^{*}H_{*}$ $\displaystyle=$ $\displaystyle(S_{0}^{*}R_{0*}\cap
S_{1}^{*}R_{1*})(R_{0}^{*}S_{0*}\cap
R_{1}^{*}S_{1*})\supseteq(S_{0}^{\circ}R_{0}\cap
S_{1}^{\circ}R_{1})(R_{0}^{\circ}S_{0}\cap R_{1}^{\circ}S_{1})$
$\displaystyle=$ $\displaystyle(S_{0}^{\circ}R_{0}\cap
S_{1}^{\circ}R_{1})((R_{0}^{\circ}S_{0}\cap R_{1}^{\circ}S_{1})(G\cap
G^{\circ})\cap R_{0}^{\circ}S_{0})$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law}}}{{\supseteq}}$
$\displaystyle(G\cap G^{\circ})\cap(S_{0}^{\circ}R_{0}\cap
S_{1}^{\circ}R_{1})R_{0}^{\circ}S_{0}$ $\displaystyle=$ $\displaystyle(G\cap
G^{\circ})\cap((G\cap G^{\circ})S_{0}^{\circ}R_{0}\cap
S_{1}^{\circ}R_{1})R_{0}^{\circ}S_{0}$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law*}}}{{\supseteq}}$
$\displaystyle(G\cap G^{\circ})\cap(G\cap G^{\circ})\cap
S_{1}^{\circ}R_{1}R_{0}^{\circ}S_{0}$

But now, using adjunction properties in $Q(\mathcal{E})$ together with the
assumption that $S_{1}S_{0}^{\circ}\subseteq\Phi$, we observe that

$S_{1}S_{0}^{\circ}\subseteq\Phi=R_{1}R_{0}^{\circ}\implies S_{1}\subseteq
R_{1}R_{0}^{\circ}S_{0}\implies G\cap G^{\circ}\subseteq
S_{1}^{\circ}R_{1}R_{0}^{\circ}S_{0},$

from which we deduce $H^{*}H_{*}\supseteq(G\cap G^{\circ})\cap
S_{1}^{\circ}R_{1}R_{0}^{\circ}S_{0}=G\cap G^{\circ}$. Then, finally,
$H^{*}H_{*}G\supseteq(G\cap G^{\circ})G$, which implies $H^{*}H_{*}\supseteq
G$.

Thus, $H_{*}$ is indeed a morphism in $\mathcal{E}_{ex/reg}$. Furthermore,

$R_{0*}H_{*}=R_{0*}(R_{0}^{*}S_{0*}\cap R_{1}^{*}S_{1*})\subseteq
R_{0*}R_{0}^{*}S_{0*}\subseteq ES_{0*}=S_{0*}$
$R_{0*}H_{*}=R_{0*}(R_{0}^{*}S_{0*}\cap R_{1}^{*}S_{1*})\supseteq
R_{0}(R_{0}^{\circ}S_{0}\cap
R_{1}^{\circ}S_{1})\stackrel{{\scriptstyle\ref{Modular
Law}}}{{\supseteq}}S_{0}\cap R_{0}R_{1}^{\circ}S_{1}=S_{0}$

where for the last inclusion we made use of the fact that
$S_{1}S_{0}^{\circ}\subseteq\Phi=R_{1}R_{0}^{\circ}$ implies $S_{0}\subseteq
R_{0}R_{1}^{\circ}S_{1}$ by the adjunction property in $Q(\mathcal{E})$. Now
we have $ER_{0*}H_{*}\supseteq ES_{0}$, which implies $R_{0*}H_{*}\supseteq
S_{0*}$. Thus, we deduce that $R_{0*}H_{*}=S_{0*}$ and similarly one obtains
$R_{1*}H_{*}=S_{1*}$. Finally, uniqueness is clear because, as we’ve proved in
the previous lemma, the equality $R_{0}^{*}R_{0*}\cap R_{1}^{*}R_{1*}=T$
implies that $R_{0*},R_{1*}$ are jointly order-monomorphic in
$\mathcal{E}_{ex/reg}$. ∎

A pair of morphisms $(R_{0*},R_{1*})$ in $\mathcal{E}_{ex/reg}$ with the
properties in 4 will be called a _tabulation_ of $\Phi\colon(X,E)\to(Y,F)\in
Q(\mathcal{E})$. This terminology is borrowed from the theory of allegories.
Note incidentally that the latter theory could have been directly applied to
$Q(\mathcal{E})$, but this approach would not work for us. The reason for that
is that we can not identify the morphisms of the would be completion
$\mathcal{E}_{ex/reg}$ as maps in this allegory, but rather only in
$Q_{w}(\mathcal{E})$. Thus, we need both of these bicategories at the same
time: $Q_{w}(\mathcal{E})$ to identify the morphisms of $\mathcal{E}_{ex/reg}$
and $Q(\mathcal{E})$ to express the existence of tabulations and perform
calculations more freely.

Furthermore, since as we’ve noted earlier every morphism
$\Phi\colon(X,E)\to(Y,F)\in Q_{w}(\mathcal{E})$ can be considered as a
morphism in $Q(\mathcal{E})$, we also have tabulations for morphisms of
$Q_{w}(\mathcal{E})$. In this case the inclusion
$S_{1}S_{0}^{\circ}\subseteq\Phi$ in the universal property of tabulations is
equivalent to $S_{1*}S_{0}^{*}\subseteq\Phi$. Indeed,
$S_{1}S_{0}^{\circ}\subseteq\Phi$ implies $FS_{1}S_{0}^{\circ}E\subseteq F\Phi
E$, which is to say $S_{1*}S_{0}^{*}\subseteq\Phi$. Similarly, for the
tabulation $(R_{0*},R_{1*})$ we have
$\Phi=R_{1}R_{0}^{\circ}=R_{1*}R_{0}^{*}$.

As we’ve already claimed, the existence of tabulations will be a fundamental
tool for establishing results about $\mathcal{E}_{ex/reg}$. As a first example
of this, we can now completely characterize what it means for a pair of
morphisms to be jointly order-monomorphic in $\mathcal{E}_{ex/reg}$.

  * 4.7 Corollary.

A pair of morphisms
$\textstyle{(Y,F)}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\scriptstyle{S_{*}}$$\textstyle{(Z,G)}$
is jointly order-monomorphic in $\mathcal{E}_{ex/reg}$ if and only if
$R^{*}R_{*}\cap S^{*}S_{*}=E$.

###### Proof.

We’ve already proven sufficiency earlier, so assume conversely that
$R_{*},S_{*}$ are jointly order-monomorphic. By the proposition above, there
exists a tabulation
$\textstyle{(X,E)}$$\textstyle{(A,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{U_{*}}$$\scriptstyle{V_{*}}$$\textstyle{(X,E)}$
for the morphism $R^{*}R_{*}\cap S^{*}S_{*}\in Q_{w}(\mathcal{E})$. Then we
have

$V_{*}U^{*}=R^{*}R_{*}\cap S^{*}S_{*}\subseteq R^{*}R_{*}\implies
R_{*}V_{*}U^{*}\subseteq R_{*}\implies R_{*}V_{*}\subseteq R_{*}U_{*}$

and similarly we obtain $S_{*}V_{*}\subseteq S_{*}U_{*}$. Thus, we have
$R_{*}V_{*}\geq R_{*}U_{*}$ and $S_{*}V_{*}\geq S_{*}U_{*}$ and hence
$V_{*}\geq U_{*}$, which is to say that $V_{*}\subseteq U_{*}$. But now we
have

$R^{*}R_{*}\cap S^{*}S_{*}=V_{*}U^{*}\subseteq U_{*}U^{*}\subseteq E$

Since the reverse inclusion always holds, we conclude that $R^{*}R_{*}\cap
S^{*}S_{*}=E$. ∎

Before beginning to prove the basic finite limit and exactness properties of
$\mathcal{E}_{ex/reg}$ we will need some information on $\mathsf{ff}$ and
$\mathsf{so}$-morphisms therein.

  * 4.8 Lemma.

Let $R_{*}\colon(X,E)\to(Y,F)$ be a morphism in $\mathcal{E}_{ex/reg}$. Then:

    1. (1)

$R_{*}$ is an $\mathsf{ff}$-morphism in $\mathcal{E}_{ex/reg}$ if and only if
$R^{*}R_{*}=E$.

    2. (2)

$R_{*}$ is an iso if and only if $R^{*}R_{*}=E$ and $R_{*}R^{*}=F$.

    3. (3)

If $R_{*}R^{*}=F$, then $R_{*}$ is an $\mathsf{so}$-morphism in
$\mathcal{E}_{ex/reg}$.

###### Proof.

  1. (1)

This follows immediately from the previous corollary.

  2. (2)

Clear.

  3. (3)

Consider a commutative square in $\mathcal{E}_{ex/reg}$ as below, where
$M_{*}$ is an $\mathsf{ff}$-morphism.

$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\scriptstyle{V_{*}}$$\textstyle{(Y,F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{*}}$$\textstyle{(Z,G)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{M_{*}}$$\textstyle{(W,H)}$

By (1.), we know that $M^{*}M_{*}=G$. Set $P_{*}\coloneqq V_{*}R^{*}$. First,
we claim that $P_{*}$ is a morphism $(Y,F)\to(Z,G)$ in $\mathcal{E}_{ex/reg}$
with $P^{*}=R_{*}V^{*}$. Indeed, we have
$P^{*}P_{*}=R_{*}V^{*}V_{*}R^{*}\supseteq R_{*}R^{*}=F$. Observe also that
$P_{*}=M^{*}S_{*}$, because $M_{*}V_{*}=S_{*}R_{*}\implies
M^{*}M_{*}V_{*}=M^{*}S_{*}R_{*}\implies V_{*}=M^{*}S_{*}R_{*}\implies
V_{*}R^{*}=M^{*}S_{*}R_{*}R^{*}=M^{*}S_{*}$. Then we can argue that
$P_{*}P^{*}=M^{*}S_{*}R_{*}V^{*}=M^{*}M_{*}V_{*}V^{*}=V_{*}V^{*}\subseteq G$.

Finally, clearly $P_{*}R_{*}=M^{*}S_{*}R_{*}=M^{*}M_{*}V_{*}=V_{*}$ and also
$M_{*}P_{*}=M_{*}V_{*}R^{*}=S_{*}R_{*}R^{*}=S_{*}$.

∎

  * 4.9 Proposition.

$\mathcal{E}_{ex/reg}$ has finite limits and
$\Gamma\colon\mathcal{E}\to\mathcal{E}_{ex/reg}$ preserves them.

###### Proof.

Let’s first construct the inserter of a pair
$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\scriptstyle{S_{*}}$$\textstyle{(Y,F)}$.
To this end, consider a tabulation
$\textstyle{(X,E)}$$\textstyle{(A,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Phi_{0*}}$$\scriptstyle{\Phi_{1*}}$$\textstyle{(X,E)}$
of $S^{*}R_{*}\cap(E\cap E^{\circ})$ as a morphism $(X,E)\to(X,E)$ in
$Q(\mathcal{E})$. Then we observe that

$\displaystyle\Phi_{1}$ $\displaystyle=$ $\displaystyle\Phi_{1}(T\cap
T^{\circ})=\Phi_{1}(\Phi_{0}^{\circ}\Phi_{0}\cap\Phi_{1}^{\circ}\Phi_{1})\subseteq\Phi_{1}\Phi_{0}^{\circ}\Phi_{0}=(S^{*}R_{*}\cap
E\cap E^{\circ})\Phi_{0}$ $\displaystyle\subseteq$ $\displaystyle(E\cap
E^{\circ})\Phi_{0}=\Phi_{0}$

and hence $\Phi_{1}=\Phi_{0}$ because the inclusion of maps in
$Q(\mathcal{E})$ is discrete. So we have $\Phi_{1*}=\Phi_{0*}$, which we
henceforth denote simply by $\Phi_{*}$. To prove that
$\Phi_{*}\colon(A,T)\to(X,E)$ is the inserter of $(R_{*},S_{*})$ it now
suffices, due to the universal property of tabulations, to show that for every
$H_{*}\colon(Z,G)\to(X,E)$ we have $R_{*}H_{*}\leq S_{*}H_{*}$ if and only if
$HH^{\circ}\subseteq S^{*}R_{*}\cap E\cap E^{\circ}$. Indeed, we have

$\displaystyle R_{*}H_{*}\leq S_{*}H_{*}$ $\displaystyle\iff$ $\displaystyle
S_{*}H_{*}\subseteq R_{*}H_{*}\iff H_{*}\subseteq S^{*}R_{*}H_{*}\iff
H_{*}H^{*}\subseteq S^{*}R_{*}$ $\displaystyle\iff$ $\displaystyle
HH^{\circ}\subseteq S^{*}R_{*}\iff HH^{\circ}\subseteq S^{*}R_{*}\cap E\cap
E^{\circ}$

Next, let us construct the product of a pair of objects $(X,E)$ and $(Y,F)$ in
$\mathcal{E}_{ex/reg}$. Observe that the maximal relation $X\looparrowright Y$
given by the product is clearly a morphism $(X,E)\to(Y,F)$ in
$Q(\mathcal{E})$. Therefore, by 4 it has a tabulation. In fact, looking back
at the proof of the latter proposition we can easily see that the tabulation
thus constructed is given by the pair of morphisms ${(X,E)}$${(X\times
Y,E\times
F)}$${(Y,F)}$$\scriptstyle{\Pi_{(X,E)*}}$$\scriptstyle{\Pi_{(Y,F)*}}$, where
$\Pi_{(X,E)*}=E\pi_{X}$ and $\Pi_{(Y,F)*}=F\pi_{Y}$. In any case, the
universal property of tabulations gives precisely the universal property of a
product diagram in $\mathcal{E}_{ex/reg}$.

Finally, it is easy to check that $\Gamma 1$ is a terminal object for
$\mathcal{E}_{ex/reg}$. ∎

Even though the above proposition tells us that $\mathcal{E}_{ex/reg}$
inherits all finite weighted limits from $\mathcal{E}$, we shall need some
more specific information as well, namely on the construction of comma squares
and pullbacks.

Consider any morphisms $R_{*}\colon(X,E)\to(Z,G)$ and
$S_{*}\colon(Y,F)\to(Z,G)$ in $\mathcal{E}_{ex/reg}$. First, we construct the
comma square below:

$\textstyle{(W,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{0*}}$$\scriptstyle{P_{1*}}$$\scriptstyle{\leq}$$\textstyle{(Y,F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{*}}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\textstyle{(Z,G)}$

For this, we take $(P_{0*},P_{1*})$ to be a tabulation of
$S^{*}R_{*}\colon(X,E)\to(Y,F)\in Q_{w}(\mathcal{E})$. To prove that this
square is indeed a comma, it suffices to prove that, given any
$U_{*}\colon(A,H)\to(X,E)$ and $V_{*}\colon(A,H)\to(Y,F)$, we have
$V_{*}U^{*}\subseteq S^{*}R_{*}$ if and only if $R_{*}U_{*}\leq S_{*}V_{*}$.
But indeed, using properties of adjunctions we have equivalences

$R_{*}U_{*}\leq S_{*}V_{*}\iff S_{*}V_{*}\subseteq R_{*}U_{*}\iff
V_{*}\subseteq S^{*}R_{*}U_{*}\iff V_{*}U^{*}\subseteq S^{*}R_{*}$

For pullbacks let us take now $(P_{0*},P_{1*})$ to be a tabulation of the
relation $S^{\circ}R\in Q(\mathcal{E})$. Then we claim that the following
square is a pullback.

$\textstyle{(W,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{P_{0*}}$$\scriptstyle{P_{1*}}$$\textstyle{(Y,F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{*}}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\textstyle{(Z,G)}$

Indeed, in this case we have for any $U_{*}\colon(A,H)\to(X,E)$ and
$V_{*}\colon(A,H)\to(Y,F)$ that $R_{*}U_{*}=S_{*}V_{*}$ if and only if
$RU=SV$, which in the allegory $Q(\mathcal{E})$ is equivalent to the inclusion
$SV\subseteq RU$. By adjunction conditions, the latter is in turn equivalent
to $SVU^{\circ}\subseteq R$ and then to $VU^{\circ}\subseteq S^{\circ}R$.
Thus, the universal property of the pullback is identified with that of the
tabulation.

Next, we prove that $\mathcal{E}_{ex/reg}$ admits the required factorization
system.

  * 4.10 Proposition.

$\mathcal{E}_{ex/reg}$ has ($\mathsf{so}$,$\mathsf{ff}$)-factorizations.

###### Proof.

Consider a morphism $R_{*}\colon(X,E)\to(Y,F)\in\mathcal{E}_{ex/reg}$. Then
$RR^{\circ}\in Q(\mathcal{E})$ and so it admits a tabulation
$\textstyle{(Y,F)}$$\textstyle{(Z,G)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\scriptstyle{S_{1*}}$$\textstyle{(Y,F)}$.
Since tautologically $R_{*}$ is such that $RR^{\circ}\subseteq
S_{1}S^{\circ}_{0}$, there exists a unique
$Q_{*}\colon(X,E)\to(Z,G)\in\mathcal{E}_{ex/reg}$ such that
$S_{0*}Q_{*}=R_{*}=S_{1*}Q_{*}$.

Now observe that in $Q(\mathcal{E})$ we have $S_{1}\subseteq
S_{1}S_{0}^{\circ}S_{0}=RR^{\circ}S_{0}\subseteq S_{0}$ and so we deduce that
$S_{1}=S_{0}$ and hence $S_{1*}=S_{0*}$. We denote this morphism now simply by
$S_{*}$. Then we have $S^{*}S_{*}=G$ by the tabulation property and this tells
us that $S_{*}$ is an $\mathsf{ff}$-morphism. It suffices now to show that
$Q_{*}Q^{*}=G$, so that $Q_{*}$ will be an $\mathsf{so}$-morphism. For this we
argue as follows:

$\displaystyle SQQ^{\circ}S^{\circ}$ $\displaystyle=$ $\displaystyle
RR^{\circ}=SS^{\circ}\implies$ $\displaystyle S^{\circ}SQQ^{\circ}S^{\circ}S$
$\displaystyle=$ $\displaystyle S^{\circ}SS^{\circ}S\implies$
$\displaystyle(G\cap G^{\circ})QQ^{\circ}(G\cap G^{\circ})$ $\displaystyle=$
$\displaystyle G\cap G^{\circ}\implies$ $\displaystyle QQ^{\circ}$
$\displaystyle=$ $\displaystyle G\cap G^{\circ}$

Then $Q_{*}Q^{*}=GQQ^{\circ}G=G(G\cap G^{\circ})G=G$. ∎

  * 4.11 Remark.

For a morphism $R_{*}\colon(X,E)\to(Y,F)\in\mathcal{E}_{ex/reg}$ we have
$R_{*}R^{*}=F$ if and only if $RR^{\circ}=F\cap F^{\circ}$. We showed the “if”
direction in the course of the above proof. For the converse, assume that
$R_{*}R^{*}=F$ and argue as follows:

$\displaystyle RR^{\circ}$ $\displaystyle=R(R^{\circ}(F\cap F^{\circ})\cap
R^{*})\stackrel{{\scriptstyle\ref{Modular Law}}}{{\supseteq}}(F\cap
F^{\circ})\cap RR^{*}=(F\cap F^{\circ})\cap(R_{*}\cap(R^{*})^{\circ})R^{*}$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law*}}}{{\supseteq}}(F\cap
F^{\circ})\cap R_{*}R^{*}\cap F^{\circ}=(F\cap F^{\circ})\cap F\cap
F^{\circ}=F\cap F^{\circ}$

  * 4.12 Corollary.

A morphism $R_{*}\colon(X,E)\to(Y,F)$ is an $\mathsf{so}$-morphism in
$\mathcal{E}_{ex/reg}$ if and only if $R_{*}R^{*}=F$, if and only if
$RR^{\circ}=F\cap F^{\circ}$.

###### Proof.

If $R_{*}R^{*}=F$, then we know that $R_{*}$ is an $\mathsf{so}$-morphism by
4. In addition, by the above remark we know that $R_{*}R^{*}=F$ is equivalent
to $RR^{\circ}=F\cap F^{\circ}$.

Now assume that $R_{*}$ is an $\mathsf{so}$-morphism. From the proof of 4 we
know that $R_{*}$ can be factored as
${(X,E)}$${(Z,G)}$${(Y,F)}$$\scriptstyle{Q_{*}}$$\scriptstyle{S_{*}}$, where
$S_{*}$ is an $\mathsf{ff}$-morphism and $Q_{*}$ satisfies $Q_{*}Q^{*}=G$.
Then $S_{*}$ is also an $\mathsf{so}$-morphism, since $R_{*}$ is such, and
hence must be an iso. It then follows immediately that $R_{*}$ also satisfies
$R_{*}R^{*}=F$. ∎

With this equational characterization of $\mathsf{so}$-morphisms in hand, we
are now in a position to prove their stability under pullback.

  * 4.13 Proposition.

$\mathsf{so}$-morphisms are stable under pullback in $\mathcal{E}_{ex/reg}$.

###### Proof.

Consider the following pullback square in $\mathcal{E}_{ex/reg}$ where we
assume that $R_{*}$ is an $\mathsf{so}$-morphism, so that we have
$R_{*}R^{*}=G$ or equivalently $RR^{\circ}=G\cap G^{\circ}$.

$\textstyle{(W,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q_{*}}$$\scriptstyle{P_{*}}$$\textstyle{(Y,F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{*}}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{*}}$$\textstyle{(Z,G)}$

By the construction of pullbacks we know that $(P_{*},Q_{*})$ is a tabulation
of $S^{\circ}R$, so that $QP^{\circ}=S^{\circ}R$. Thus, we have

$\displaystyle QQ^{\circ}$ $\displaystyle=$ $\displaystyle Q(T\cap
T^{\circ})Q^{\circ}=Q(P^{\circ}P\cap
Q^{\circ}Q)Q^{\circ}\stackrel{{\scriptstyle\ref{Modular
Law}}}{{\supseteq}}(QP^{\circ}P\cap Q)Q^{\circ}$
$\displaystyle\stackrel{{\scriptstyle\ref{Modular Law*}}}{{\supseteq}}$
$\displaystyle QP^{\circ}PQ^{\circ}\cap(F\cap
F^{\circ})=S^{\circ}RR^{\circ}S\cap(F\cap F^{\circ})$ $\displaystyle=$
$\displaystyle S^{\circ}(G\cap G^{\circ})S\cap(F\cap
F^{\circ})=S^{\circ}S\cap(F\cap F^{\circ})=F\cap F^{\circ}$

Hence, $QQ^{\circ}=F\cap F^{\circ}$ or equivalently $Q_{*}Q^{*}=F$ and hence
$Q_{*}$ is an $\mathsf{so}$-morphism. ∎

Putting together what we have proved so far, we have the following.

  * 4.14 Corollary.

$\mathcal{E}_{ex/reg}$ is a regular category and
$\Gamma\colon\mathcal{E}\to\mathcal{E}_{ex/reg}$ is a fully order-faithful
regular functor.

We next would like to prove that $\mathcal{E}_{ex/reg}$ is exact. To
accomplish this we first make good on promises made much earlier. Namely, we
identify $Q_{w}(\mathcal{E})$ as the bicategory of weakening-closed relations
in $\mathcal{E}_{ex/reg}$ and, before that, $Q(\mathcal{E})$ as the bicategory
of all relations in $\mathcal{E}_{ex/reg}$.

  * 4.15 Proposition.

There is an equivalence $\mathrm{Rel}(\mathcal{E}_{ex/reg})\simeq
Q(\mathcal{E})$.

###### Proof.

We will define a functor
$\mathfrak{F}\colon\mathrm{Rel}$$(\mathcal{E}_{ex/reg})\to$ $Q(\mathcal{E})$
by letting it be the identity on objects and mapping a relation represented by
any jointly order-monomorphic pair
$\textstyle{(X,E)}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$ to the morphism
$R_{1}R_{0}^{\circ}\colon(X,E)\to(Y,F)\in Q(\mathcal{E})$.

To show that this assignment is functorial, consider first the diagonal
relation on the object $(X,E)$ in $\mathrm{Rel}$$(\mathcal{E}_{ex/reg})$, i.e.
the relation represented by the jointly order-monomorphic pair
$\textstyle{(X,E)}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{(X,E)*}}$$\scriptstyle{1_{(X,E)*}}$$\textstyle{(X,E)}$.
Then the image of this relation under $\mathfrak{F}$ is
$1_{(X,E)}1_{(X,E)}^{\circ}=(E\cap E^{\circ})(E\cap E^{\circ})^{\circ}=E\cap
E^{\circ}$ and so $\mathfrak{F}$ preserves identity morphisms.

Next, we consider two relations $\mathscr{R},\mathscr{S}$ in
$\mathcal{E}_{ex/reg}$, say represented respectively by the jointly order-
monomorphic pairs
$\textstyle{(X,E)}$$\textstyle{(A,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$
and
$\textstyle{(Y,F)}$$\textstyle{(B,T^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\scriptstyle{S_{1*}}$$\textstyle{(Z,G)}$.
To calculate the composition of these two relations we form the following
pullback square in $\mathcal{E}_{ex/reg}$

$\textstyle{(C,\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Pi_{1*}}$$\scriptstyle{\Pi_{0*}}$$\textstyle{(B,T^{\prime})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\textstyle{(A,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$

and then the image factorization of $\langle
R_{0*}\Pi_{0*},S_{1*}\Pi_{1*}\rangle$, say

$\textstyle{(C,\Omega)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q_{*}}$$\textstyle{(D,\Theta)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
U_{0*},U_{1*}\rangle}$$\textstyle{(X,E)\times(Z,G)}$

By construction of pullbacks in $\mathcal{E}_{ex/reg}$ we know that
$\Pi_{1}\Pi_{0}^{\circ}=S_{0}^{\circ}R_{1}$. Also, by definition
$\mathfrak{F}$ maps the composition of the two relations to
$\mathfrak{F}(\mathscr{S}\mathscr{R})=U_{1}U_{0}^{\circ}$. But now we have
that

$U_{1}U_{0}^{\circ}=U_{1}QQ^{\circ}U_{0}^{\circ}=S_{1}\Pi_{1}\Pi_{0}^{\circ}R_{0}^{\circ}=S_{1}S_{0}^{\circ}R_{1}R_{0}^{\circ}=\mathfrak{F}(\mathscr{S})\mathfrak{F}(\mathscr{R})$

Finally, the fact that $\mathfrak{F}$ preserves the order of morphisms and is
fully (order-) faithful is precisely the existence of tabulations proved in 4.
Thus, $\mathfrak{F}$ is an equivalence of bicategories. ∎

  * 4.16 Proposition.

There is an equivalence $\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})\simeq
Q_{w}(\mathcal{E})$.

###### Proof.

We define a functor
$\mathfrak{F}\colon\mathrm{Rel}_{w}$$(\mathcal{E}_{ex/reg})\to$
$Q_{w}(\mathcal{E})$ exactly as in the proof of the previous proposition. Then
the main observation to make here is the following: a relation
$\mathscr{R}\colon(X,E)\looparrowright(Y,F)$ represented by the jointly order-
monomorphic pair
$\textstyle{(X,E)}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\textstyle{(Y,F)}$
in $\mathcal{E}_{ex/reg}$ is weakening-closed if and only if
$R_{1*}R_{0}^{*}=R_{1}R_{0}^{\circ}$ as relations in $\mathcal{E}$.

Recall that $\mathscr{R}$ is a weakening-closed relation precisely if
$I_{(Y,F)}\mathscr{R}I_{(X,E)}=\mathscr{R}$ in
$\mathrm{Rel}$$(\mathcal{E}_{ex/reg})$. To compute the composition
$I_{(Y,F)}\mathscr{R}I_{(X,E)}$ one has to form the following diagram in
$\mathcal{E}_{ex/reg}$ where the top square is a pullback and the bottom two
are commas and then take the image factorization of the morphism $\langle
U_{0*}W_{0*},V_{1*}W_{1*}\rangle$.

$\textstyle{(C,X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{W_{0*}}$$\scriptstyle{W_{1*}}$$\textstyle{(A,\Phi)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{U_{0*}}$$\scriptstyle{U_{1*}}$$\textstyle{(B,\Psi)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{V_{0*}}$$\scriptstyle{V_{1*}}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{(X,E)*}}$$\scriptstyle{\leq}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$$\scriptstyle{\leq}$$\textstyle{(Y,F)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{(Y,F)*}}$$\textstyle{(X,E)}$$\textstyle{(Y,F)}$

Note that by the various limit constructions in $\mathcal{E}_{ex/reg}$ we know
that we must have $R_{0}^{*}=U_{1}U_{0}^{\circ}$, $R_{1*}=V_{1}V_{0}^{\circ}$
and $V_{0}^{\circ}U_{1}=W_{1}W_{0}^{\circ}$.

If $I_{(Y,F)}\mathscr{R}I_{(X,E)}=\mathscr{R}$, then there is a factorization
in $\mathcal{E}_{ex/reg}$

$\textstyle{(C,X)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{Q_{*}}$$\textstyle{(Z,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\langle
R_{0*},R_{1*}\rangle}$$\textstyle{(X,E)\times(Y,F)}$

with $Q_{*}$ an $\mathsf{so}$-morphism, so that $QQ^{\circ}=T\cap T^{\circ}$.
Then we have that

$R_{1*}R_{0}^{*}=V_{1}V_{0}^{\circ}U_{1}U_{0}^{\circ}=V_{1}W_{1}W_{0}^{\circ}U_{0}^{\circ}=R_{1}QQ^{\circ}R_{0}^{\circ}=R_{1}R_{0}^{\circ}$

Conversely, assume that $R_{1*}R_{0}^{*}=R_{1}R_{0}^{\circ}$ and let us
consider four morphisms
$\textstyle{(X,E)}$$\textstyle{(C,G)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{S_{0*}}$$\scriptstyle{U_{*}}$$\scriptstyle{S_{1*}}$$\scriptstyle{V_{*}}$$\textstyle{(Y,F)}$
such that $(S_{0*},S_{1*})$ factors through $(R_{0*},R_{1*})$ and $U_{*}\leq
S_{0*}$ and $S_{1*}\leq V_{*}$. Then we respectively have
$S_{1*}S_{0}^{*}\subseteq R_{1*}R_{0}^{*}$ and $U^{*}\subseteq S_{0}^{*}$ and
$V_{*}\subseteq S_{1*}$. Hence, $V_{*}U^{*}\subseteq S_{1*}S_{0}^{*}\subseteq
R_{1*}R_{0}^{*}=R_{1}R_{0}^{\circ}$ and so $(U_{*},V_{*})$ must also factor
through $(R_{0*},R_{1*})$ by the universal property of tabulations.

With this observation in hand, one can run the same proof as in the previous
proposition to show that
$\mathfrak{F}\colon\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})\to
Q_{w}(\mathcal{E})$ thus defined is an equivalence. The only point of minor
difference is in the proof that $\mathfrak{F}$ preserves identity morphisms.
For this, just recall that the identity on an object $(X,E)$ in
$\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})$ is the relation given by the
following comma square

$\textstyle{(A,T)\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{R_{1*}}$$\scriptstyle{R_{0*}}$$\scriptstyle{\leq}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{(X,E)*}}$$\textstyle{(X,E)\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{1_{(X,E)*}}$$\textstyle{(X,E)}$

so that by construction of commas we have that
$R_{1}R_{0}^{\circ}=1_{(X,E)}^{*}1_{(X,E)*}=EE=E$. ∎

Now from this last proposition one can immediately deduce that
$\mathcal{E}_{ex/reg}$ is indeed an exact category.

  * 4.17 Corollary.

The category $\mathcal{E}_{ex/reg}$ is exact.

###### Proof.

Using the equivalence $\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})\simeq
Q_{w}(\mathcal{E})$, we can see that a congruence on an object
$(X,E)\in\mathcal{E}_{ex/reg}$ corresponds precisely to a congruence $R$ on
the object $X\in\mathcal{E}$ with $R\supseteq E$.

Indeed, consider a congruence $\mathscr{R}$ on the object
$(X,E)\in\mathcal{E}_{ex/reg}$, represented by the jointly order-monomorphic
pair ${(X,E)}$${(Y,F)}$${(X,E)}$$\scriptstyle{R_{0*}}$$\scriptstyle{R_{1*}}$.
Consider the functor
$\mathfrak{F}\colon\mathrm{Rel}_{w}(\mathcal{E}_{ex/reg})\to
Q_{w}(\mathcal{E})$ providing the equivalence and let
$R\coloneqq\mathfrak{F}(\mathscr{R})$. Since $\mathfrak{F}$ is an equivalence,
we have that $\mathscr{R}\mathscr{R}\subseteq\mathscr{R}$ if and only if
$RR\subseteq R$ in $Q_{w}(\mathcal{E})$, i.e. that transitivity of
$\mathscr{R}$ is equivalent to the same property for $R$ as a relation in
$\mathcal{E}$. Similarly, the inclusion $\mathscr{R}\supseteq I_{(X,E)}$ is
equivalent to $R\supseteq\mathfrak{F}(I_{(X,E)})=E$. In particular,
$R\supseteq I_{X}$ and so $R$ is a congruence on $X\in\mathcal{E}$.

The idempotent morphism $\mathfrak{F}(\mathscr{R})=R\colon(X,E)\to(X,E)$ in
$Q_{w}(\mathcal{E})$ now splits by construction, namely as
${(X,E)}$${(X,R)}$${(X,E)}$$\scriptstyle{R}$$\scriptstyle{R}$. Thus,
$\mathscr{R}$ splits as an idempotent in
$\mathrm{Rel}_{w}$$(\mathcal{E}_{ex/reg})$ and hence we have shown that
$\mathcal{E}_{ex/reg}$ is exact. ∎

It remains to prove that $\mathcal{E}_{ex/reg}$, or more precisely
$\Gamma\colon\mathcal{E}\to\mathcal{E}_{ex/reg}$ satisfies the required
universal property. Before doing this, we observe in the proposition that
follows that every object of $\mathcal{E}_{ex/reg}$ appears as a quotient of a
congruence coming from $\mathcal{E}$ in a canonical way.

  * 4.18 Proposition.

For every object $(X,E)\in\mathcal{E}_{ex/reg}$ there exists an exact sequence
$\textstyle{\Gamma
E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Gamma
e_{0}}$$\scriptstyle{\Gamma e_{1}}$$\textstyle{\Gamma
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E}$$\textstyle{(X,E)}$,
where $\langle e_{0},e_{1}\rangle\colon E\rightarrowtail X\times X$ is an
$\mathsf{ff}$-morphism representing the congruence $E$ in $\mathcal{E}$.

###### Proof.

Observe that $E$ indeed defines a morphism $E_{*}\colon\Gamma X\to(X,E)$ in
$\mathcal{E}_{ex/reg}$ which is in fact effective because $EI_{X}=E=EE$,
$E^{*}E_{*}=EE=E\supseteq I_{X}$, $E_{*}E^{*}=EE=E$. Now it suffices to show
that the square below is a comma square in $\mathcal{E}_{ex/reg}$.

$\textstyle{\Gamma
E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Gamma
e_{1}}$$\scriptstyle{\Gamma e_{0}}$$\scriptstyle{\leq}$$\textstyle{\Gamma
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E}$$\textstyle{\Gamma
X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{E}$$\textstyle{(X,E)}$

But by the construction of comma squares in $\mathcal{E}_{ex/reg}$ this is
equivalent to having $(\Gamma e_{0})^{*}\Gamma e_{0}\cap(\Gamma
e_{1})^{*}\Gamma e_{1}=I_{E}$ and $\Gamma e_{1}(\Gamma
e_{0})^{\circ}=E^{*}E_{*}$ i.e. $e_{0}^{*}e_{0*}\cap e_{1}^{*}e_{1*}=I_{E}$
and $e_{1}e_{0}^{\circ}=EE$ as relations in $\mathcal{E}$, both of which hold.
∎

Now we at last come to the proof that $\mathcal{E}_{ex/reg}$ satisfies the
universal property that exhibits it as the exact completion of the regular
category $\mathcal{E}$. Before proceeding, let us make a couple of quick
observations that will be used in the course of our calculations in the proof
that follows below.

Consider an exact fork
$\textstyle{E\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\textstyle{P}$
in the regular category $\mathcal{E}$. Recall that in the calculus of
relations this means that $E=p^{*}p_{*}$ and $p_{*}p^{*}=I_{P}$, where the
second equality can equivalently be replaced by $pp^{\circ}=\Delta_{P}$. In
addition, the kernel pair $p^{\circ}p$ of $p$ can be written as
$p^{*}p_{*}\cap(p^{*}p_{*})^{\circ}$ and hence we also have $p^{\circ}p=E\cap
E^{\circ}$ We now observe that the following equalities must hold:

  * •