In this article we establish a connection between pretabular unitary allegories and bicategories of relations, and also between tabular unitary allegories and regular categories. The material is entirely adapted from Categories, Allegories; we have merely changed some details of arrangement, notation, and terminology.
We write the composite of morphisms $r \colon a \to b$, $s \colon b \to c$ as $s r \colon a \to c$.
An allegory is a $Pos$-enriched $\dagger$-category $A$ where each hom-poset has binary meets, and the modular law is satisfied. The modular law takes two forms, whenever the left sides of the inequalities make sense:
$r s \wedge t \leq r(s \wedge r^\dagger t)$
$r s \wedge t \leq (r \wedge t s^\dagger)s$
(and of course there are variations, using commutativity of $\wedge$). Each of these forms can be derived from the other, using the $\dagger$-structure.
The $\dagger$-operation, which we henceforth denote by $(-)^o$, preserves meets since it preserves order and is an involution.)
For any $r \colon a \to b$, we have $r \leq r r^o r$.
We have $r \leq r 1_b \wedge r \leq r(1 \wedge r^o r) \leq r r^o r$ where the middle inequality uses the modular law.
Recall that a map in an allegory is a morphism $f \colon a \to b$ such that $f \dashv f^o$. A relation $r \colon a \to b$ is well-defined if we merely have a counit inclusion $r r^o \leq 1_b$, and is total if we merely have a unit inclusion $1_a \leq r^o r$. Clearly maps are closed under composition, as are total relations and well-defined relations.
If $f \colon a \to b$ is a map, then for any $r, s \in \hom(b, c)$ we have $(r \wedge s)f = r f \wedge s f$.
The non-trivial inclusion follows from
where the first inequality is an instance of the modular law, and the second holds for any well-defined relation $f$.
If $f, g \colon a \to b$ are maps and $f \leq g$, then $f = g$.
Since the dagger operation $(-)^o \colon \hom(a, b) \to \hom(b, a)$ preserves order, we have $f^o \leq g^o$. But also the inclusion $f \leq g$ between left adjoints is mated to an inclusion $g^o \leq f^o$ between right adjoints. Hence $f^o = g^o$, and therefore $f = g$.
Let $r \colon a \to b$ be a morphism. We define the domain $\dom(r)$ to be $1_a \wedge r^o r$. A morphism $e \colon a \to a$ is coreflexive if $e \leq 1_a$; in particular, domains are coreflexive. $Cor(a)$ denotes the poset of coreflexives in $\hom(a, a)$.
Coreflexives $r \colon a \to a$ are symmetric and transitive. (Symmetric and transitive imply idempotent.)
We have $r \leq r r^o r \leq 1_a r^o 1_a \leq r^o$ where the first inequality is lemma 1. Of course also $r r \leq 1_a r = r$. (If $r$ is symmetric and transitive, then $r \leq r r^o r = r r r \leq r r$ as well.)
For $r, s \in \hom(a, b)$, we have $\dom(r \wedge s) = 1_a \wedge r^o s$.
One inclusion is trivial:
The other inclusion follows from fairly tricky applications of the modular law:
For $r \colon a \to b$ and coreflexives $c \in \hom(a, a)$, we have $\dom(r) \leq c$ if and only if $r \leq r c$. In particular, $r \leq r \circ \dom(r)$.
If $1_a \wedge r^o r \leq c$, then
If $r \leq r c$, then
where the antepenultimate inequality uses the modular law, and the last uses lemma 4.
For $r \colon a \to b$ and $s \colon b \to c$, we have $\dom(s r) \leq \dom(r)$.
By lemma 6, it suffices that $s r \leq s r \circ \dom(r)$. But this follows from the last sentence of lemma 6.
An object $t$ is a unit in an allegory if $1_t$ is maximal in $\hom(t, t)$ and if for every object $a$ there is $f \colon a \to t$ such that $1_a \leq f^o f$ (i.e., $f$ is total).
Of course by maximality we also have $f f^o \leq 1_t$, so such $f$ must also be a map.
We say $A$ is unital (Freyd-Scedrov say unitary) if $A$ has a unit.
Let $t$ be a unit. Then $\dom \colon \hom(a, t) \to Cor(a)$ is an injective order-preserving function.
Order-preservation is clear. If $r, s \colon a \to t$ and $\dom(r) \leq \dom(s)$, then $r \leq s$:
where the first inequality uses lemma 6, and the last inequality follows from $r s^o \leq 1_t$ (since $1_t$ is maximal in $\hom(t, t)$). Therefore $\dom(r) = \dom(s)$ implies $r = s$.
For a unit $t$ and any $a$, there is at most one total relation = map $r \colon a \to t$ (because in that case $\dom(r) = 1_a$, and we apply the previous proposition), and this is maximal in $\hom(a, t)$. Thus $t$ is terminal in $Map(A)$.
Let $\varepsilon_a \colon a \to t$ denote the maximal element of $\hom(a, t)$. For any $r \colon a \to b$, we then have $r \leq \varepsilon_b^o \varepsilon_a$ since this is mated to the inequality $\varepsilon_b r \leq \varepsilon_a$. Therefore $\varepsilon_b^o \varepsilon_a$ is the maximal element of $\hom(a, b)$.
Recall from Categories, Allegories that a tabulation of $r \colon a \to b$ is a pair of maps $f \colon x \to a$, $g \colon x \to b$ such that $r = g f^o$ and $f^o f \wedge g^o g = 1_x$.
For maps $f \colon x \to a$, $g \colon x \to b$, the condition $f^o f \wedge g^o g = 1_x$ implies $(f, g)$ is a jointly monic pair in $Map(A)$.
Let $h, h' \colon y \to x$ be maps, and suppose $f h = f h'$ and $g h = g h'$. If $f^o f \wedge g^o g = 1_x$, then
where the second and fourth equations use lemma 2.
Suppose $r: a \to b$ is tabulated by $(f \colon x \to a, g \colon x \to b)$, and suppose $h \colon y \to a$, $k \colon y \to b$ are maps. We have $k h^o \leq g f^o$ if and only if there exists a map $j \colon y \to x$ such that $h = f j$ and $k = g j$ (this $j$ is unique by lemma 7).
One direction is easy: if $h = f j$ and $k = g j$ for some map $j$, then
In the other direction: suppose $k h^o \leq g f^o$. Put $j = f^o h \wedge g^o k$. First we check that $j$ is a map. We have $1_y \leq j^o j$ from
using lemma 5. We have $j j^o \leq 1_x$ from
where the last step uses one of the tabulation conditions. So $j$ is a map.
Finally, we have $f j \leq f(f^o h) \leq h$, which implies $f j = h$ (lemma 3). Similarly $g j = k$.
Tabulations are unique up to unique isomorphism.
A diagram in $Map(A)$
commutes if and only if $k h^o \leq g^o f$.
An identity inclusion $g k = f h$ is certainly mated to an inclusion $k h^o \leq g^o f$. Conversely, an inclusion $k h^o \leq g^o f$ is mated to $g k \leq f h$, and we can use lemma 3.
Given $f \colon a \to c$ and $g \colon b \to c$ in $Map(A)$, a tabulation $(h \colon p \to a, k \colon p \to b)$ of $r = g^o f$ provides a pullback of $(f, g)$.
Indeed, by definition of tabulation we then have $k h^o = g^o f$, so $g k = f h$. For the universality of $(h, k)$: if $g k' = f h'$, then $k (h')^o \leq g^o f$, and we can apply proposition 2 to finish.
If $i \colon a \to b$ is a monomorphism in $Map(A)$ and $i^o i$ has a tabulation, then $i^o i = 1_a$.
The tabulation of $i^o i$ gives a pullback of the pair $(i, i)$, but since this pullback is already $(1_a, 1_a)$, the conclusion is clear.
If $r \colon a \to a$ is coreflexive, then for any tabulation $(f, g)$ of $r$, we have $f = g$ and $f$ is monic.
The inclusion $g f^o = r \leq 1_a$ is mated to $g \leq f$ which must be an identity $g = f$. If $(f, g) = (f, f)$ is jointly monic, then $f$ is monic.
An allegory is tabular if every morphism $r \colon a \to b$ admits a tabulation. A unital allegory is pretabular if for all $a, b$, the maximal morphism $\varepsilon_b^o \varepsilon_a \in \hom(a, b)$ (see the last sentence of the Units section) admits a tabulation.
It is immediate from corollary 4 that if $A$ is tabular, then $Map(A)$ has pullbacks.
Likewise, it is immediate from the preceding corollary that if $A$ is unital and pretabular, then $Map(A)$ has products, because we can form the pullback of the maps $\varepsilon_a \colon a \to t$, $\varepsilon_b \colon b \to t$ to the terminal object $t$.
In a tabular allegory $A$, a map $q \colon a \to e$ is a strong epi in $Map(A)$ if $q q^o = 1_e$.
If $q q^o = 1_e$, then it is first of all clear that $q$ is an epi in $Map(A)$ because it retracts $q^o$ in $A$. We show $q$ is orthogonal to monomorphisms in $Map(A)$. That is, consider a commutative diagram
where $i$ is monic. We wish to show there exists a filler map $g \colon e \to b$ such that $g q = f$ and $i g = j$. The uniqueness of a filler map is clear since $i$ is monic.
Put $g = f q^o$. We first check that $g$ is a map. Notice that the identity inclusion $i f = j q$ is mated to an inclusion $f q^o \leq i^o j$, so we have $g \leq i^o j$. In that case we have
where the last inclusion holds because $i$ is monic (corollary 5). This gives the counit for $g \dash v g^o$. For the unit, use
So $g = f q^o$ is a map. We also have
and finally we have
so that $f = g q$ by lemma 3. This completes the proof.
If $A$ is tabular, then $Map(A)$ has equalizers. Moreover, every map has a (strong epi)-mono factorization, and strong epis are preserved by pullbacks. In short, $Map(A)$ is a locally regular category. If $A$ is moreover unital, then $Map(A)$ is regular.
The equalizer of a pair of maps $f, g \colon a \to b$ may be constructed as a tabulation of the coreflexive arrow $\dom(f \wedge g)$. By lemma 8, the tabulation is of the form $(h, h)$ where $h$ is monic, and by an application of proposition 2, one sees it is the universal map that equalizes $f$ and $g$.
For any map $f \colon a \to b$, consider a tabulation of the coreflexive $\dom(f^o) = f f^o \colon b \to b$ by a pair of maps $(i, i)$. Notice that $i \colon e \to b$ is monic in $Map(A)$, and $i i^o = f f^o$. By proposition 2, there exists a unique $q \colon a \to e$ such that $f = i q$. Following the proof of proposition 2, the map $q$ is constructed as $i^o f$. We have
i.e., $\dom(q^o) = 1_e$ ($q^o$ is total). By lemma 9, this means $q$ is a strong epi in $Map(A)$. Thus we have factored $f$ into a strong epi followed by a mono.
Now suppose $q \colon a \to e$ is any strong epi and $g \colon d \to e$ is a map, and that $(g' \colon p \to a, q' \colon p \to d)$ is a pullback of $(g, q)$. Then $(g', q')$ is a tabulation of $q^o g$, so $q^o g = g' (q')^o$. Now the left side of this equation is total, and therefore so is the right: $1_e \leq \dom(g' (q')^o)$. But then
where the second inequality uses corollary 1. This means $q'$ is strong epi, and we are done.