module Cat.Allegory.Base where

# Allegoriesπ

In the same way that a category abstracts over the commonalities of
sets and functions (and thus allows us to study several other
mathematical constructions which are not βset-and-function-likeβ on the
nose using a common framework), the idea of **allegories**
is to abstract over the commonalities of sets and *relations*.
Remarkably, allegories are defined as category-*like* structures,
as weβll see.

**A note**: In the literature (particularly the nLab),
allegories are defined as a special case of bicategories. For ease of presentation, we
have chosen to introduce allegories as their own concept, *a
priori* disconnected from our theory of bicategories.

record Allegory o β β' : Type (lsuc (o β β β β')) where no-eta-equality field cat : Precategory o β open Precategory cat public

An allegory
$\mathcal{A}$
has an underlying precategory (whose morphisms we call
**relations**), but, more importantly, an ordering relation
$f \le g$
on the relations, which we think of as inclusion in the usual sense^{1}. When considered with this ordering,
$\mathcal{A}$
must be a *locally posetal bicategory*: a bicategory
$\mathcal{A}$,
with all Hom-categories being posets.

field _β€_ : β {x y} β Hom x y β Hom x y β Type β' β€-thin : β {x y} {f g : Hom x y} β is-prop (f β€ g) β€-refl : β {x y} {f : Hom x y} β f β€ f β€-trans : β {x y} {f g h : Hom x y} β f β€ g β g β€ h β f β€ h β€-antisym : β {x y} {f g : Hom x y} β f β€ g β g β€ f β f β‘ g

We want the composition operation to be functorial with respect to the ordering, which means that $f \le f'$ and $g \le g'$ must imply $fg \le f'g'$. We have to include this explicitly since we are unpacking the data of a bicategory.

_β_ : β {w x y} {f f' : Hom x y} {g g' : Hom w x} β f β€ f' β g β€ g' β (f β g) β€ (f' β g')

Moreover,
$\mathcal{A}$
must be equipped with an involution on its Hom-sets: This is the usual
opposite of a relation,
i.e.Β $R^o(x,y) = R(y,x)$,
and, as you have noticed, we will write the opposite of
$f$
as
$f^o$.
The involution must play nice with the ordering, and it must follow the
socks-and-shoes principle^{2} w.r.t. composition:
$(fg)^o = g^of^o$.

field _β : β {x y} β Hom x y β Hom y x dual : β {x y} (f : Hom x y) β f β β β‘ f dual-β : β {w x y} {f : Hom x y} {g : Hom w x} β (f β g) β β‘ g β β f β dual-β€ : β {x y} {f g : Hom x y} β f β€ g β f β β€ g β

The penultimate requirement is that each Hom-poset have binary products, i.e., intersection of relations. Note that we do not mandate nullary products, i.e., we do not require an arbitrary allegory to have βmaximalβ relations.

field _β©_ : β {x y} β Hom x y β Hom x y β Hom x y β©-le-l : β {x y} {f g : Hom x y} β f β© g β€ f β©-le-r : β {x y} {f g : Hom x y} β f β© g β€ g β©-univ : β {x y} {f g h : Hom x y} β h β€ f β h β€ g β h β€ f β© g

Finally, an allegory must satisfy the **modular law**,
which we phrase as the statement below (following Freyd). Allegories
thus generalise modular lattices, in the same way that categories
generalise monoids.^{3}

field modular : β {x y z} (f : Hom x y) (g : Hom y z) (h : Hom x z) β (g β f) β© h β€ g β (f β© (g β β h))

## Quick theoremsπ

The first thing we observe about allegories is a Yoneda-type lemma
for relations: Fixing
$g$
and
$h$,
if
$f \le g$
is equivalent to
$f \le h$
for every
$f$,
then
$g = h$.
Needless to say, this holds in any poset (and really any univalent category),
but we emphasise it *here*, for allegories, since it will be used
to prove important laws.

module _ {o β β'} (A : Allegory o β β') where open Allegory A β€-yoneda : β {x y} {g h : Hom x y} β (β f β f β€ g β f β€ h) β (β f β f β€ h β f β€ g) β g β‘ h β€-yoneda to fro = β€-antisym (to _ β€-refl) (fro _ β€-refl)

Since the duality respects ordering, we can ping-pong $(-)^o$ to get it out of the way: $f^o \le g$ is exactly the same as $f \le g^o$.

dual-β€β : β {x y} {f : Hom x y} {g} β f β€ g β β f β β€ g dual-β€β {f = f} w = subst (f β β€_) (dual _) (dual-β€ w) dual-β€α΅£ : β {x y} {f : Hom x y} {g} β f β β€ g β f β€ g β dual-β€α΅£ {f = f} {g} w = subst (_β€ g β ) (dual _) (dual-β€ w)

As an application of these two quick lemmas and the laws for meets, we prove that the dual $(f \cap g)^o$ is equivalently given by $f^o \cap g^o$. We ellaborate the correspondence in one direction: Suppose that $f \le (f \cap g)^o$. Pinging the dual across, we get $h^o \le (f \cap g)$, which (by the definition of meet) is equivalent to the conjunction of $h^o \le f$ and $h^o \le g$. But ponging the dual on either of those, we get $h \le f^o$ and $h \le g^o$, which mean $h \le f^o \cap g^o$.

dual-β© : β {x y} {f g : Hom x y} β (f β© g) β β‘ f β β© g β dual-β© {f = f} {g = g} = β€-yoneda (Ξ» h hβ€fβ©gα΅ β let hα΅β€fβ©g = dual-β€β hβ€fβ©gα΅ hα΅β€f = β€-trans hα΅β€fβ©g β©-le-l hα΅β€g = β€-trans hα΅β€fβ©g β©-le-r in β©-univ (dual-β€α΅£ hα΅β€f) (dual-β€α΅£ hα΅β€g)) (Ξ» h hβ€gα΅β©fα΅ β let hβ€gα΅ = β€-trans hβ€gα΅β©fα΅ β©-le-r hβ€fα΅ = β€-trans hβ€gα΅β©fα΅ β©-le-l in dual-β€α΅£ (β©-univ (dual-β€β hβ€fα΅) (dual-β€β hβ€gα΅))) dual-id : β {x} β id {x = x} β β‘ id dual-id = sym (sym (dual id) β ap _β (sym (idl _)) β dual-β β ap (_β id β ) (dual _) β idl _)

# The allegory of relationsπ

The allegorical analogue of the category of sets is the
**allegory of relations**,
$\mathbf{Rel}$.
As usual, every universe level
$\kappa$
gives an allegory
$\mathbf{Rel}_\kappa$,
whose objects are
$\kappa$-small
sets, and morphisms are
$\kappa$-small
relations. Note that, in the absence of propositional resizing,
$\mathbf{Rel}$βs
underlying category is *not* locally
$\kappa$-small:
The set of
$\kappa$-small
propositions lives in the successor universe, not in
$\kappa$.

Ordering of relations is as one would expect: $R \le S$ is defined to mean every $R$-related pair $(x, y)$ is also $S$-related. When seen as subsets of $A \times B$, this is exactly the inclusion ordering.

Rel : β β β Allegory (lsuc β) β β Rel β .cat .Ob = Set β Rel β .cat .Hom A B = β£ A β£ β β£ B β£ β Ξ© Rel β ._β€_ R S = β x y β β£ R x y β£ β β£ S x y β£

Relational composition is again given by the familiar formula: The composite of $R$ and $S$ is given by the relation which βbridges the gapβ, i.e.Β $(R \circ S)(x, z)$ iff. there exists some $y$ such that $R(x, y)$ and $S(y, z)$. Iβm not sure how surprising this will be to some of you β embarassingly, it was fairly surprising to me β but the identity relation is.. the identity relation:

Rel β .cat ._β_ S R x z = elΞ© (Ξ£ _ Ξ» y β β£ R x y β£ Γ β£ S y z β£) Rel β .cat .id x y = elΞ© (x β‘ y)

We can investigate the reason for this by working through e.g.Β the proof that relational composition is right-unital. Weβll leave the identity relation written as just $\operatorname{Id}_{}$, but in either case, what we want to show that $(x, y) \mapsto \exists (a : A), \operatorname{Id}_{}(x, a) \land R(a, y)$ relates the same pairs as $R$. In the interesting direction, weβre given some $a : A$ and a witness that $R(a, y)$: but what we wanted was to show $R(x, y)$! Fortunately if we we set $\operatorname{Id}_{}(x, a)$, then $R(x, y) \simeq R(a, y)$, and weβre done.

Rel β .cat .idr {A} {B} R = ext Ξ» x y β Ξ©-ua (β‘-rec! (Ξ» { (a , b , w) β subst (Ξ» e β β£ R e y β£) (sym (out! b)) w })) Ξ» w β inc (x , inc refl , w)

The other interesting bits of the construction are meets, the dual, and the implication witnessing the modular law: Meets are given by the pointwise conjunction, i.e., $R \cap S$ is

- The relation given by the intersection of the subsets representing $R$ and $S$, or
- The relation which relates $x$ and $y$ iff. both $R$ and $S$ relate them.

The dual is given by inverting the order of arguments to $R$, and the modular law is given by some pair-shuffling.

Rel β ._β©_ R S x y = el (β£ R x y β£ Γ β£ S x y β£) hlevel! Rel β ._β R x y = R y x Rel β .modular R S T x y (Ξ± , Ξ²) = β‘-rec! (Ξ» { (z , r , s) β inc (z , (r , inc (y , Ξ² , s)) , s) }) Ξ±

##
The rest of the construction is either automated, or very boring
applications of propositional extensionality. Most of the proof below
was not written by me, but rather by Agdaβs^{4}
automatic proof search: that speaks to how contentful it is.

Rel β .cat .Hom-set x y = hlevel 2 Rel β .cat .idl R = ext Ξ» x y β Ξ©-ua (β‘-rec! (Ξ» { (a , b , w) β subst (Ξ» e β β£ R x e β£) (out! w) b })) Ξ» w β inc (y , w , inc refl) Rel β .cat .assoc T S R = ext Ξ» x y β Ξ©-ua (β‘-rec! Ξ» { (a , b , w) β β‘-rec! (Ξ» { (c , d , x) β inc (c , d , inc (a , x , w)) }) b }) (β‘-rec! Ξ» { (a , b , w) β β‘-rec! (Ξ» { (c , d , x) β inc (c , inc (a , b , d) , x) }) w }) Rel β .β€-thin = hlevel! Rel β .β€-refl x y w = w Rel β .β€-trans x y p q z = y p q (x p q z) Rel β .β€-antisym p q = ext Ξ» x y β Ξ©-ua (p x y) (q x y) Rel β ._β_ f g a b = β‘-map (Ξ» { (x , y , w) β x , g a x y , f x b w }) -- This is nice: Rel β .dual R = refl Rel β .dual-β = ext Ξ» x y β Ξ©-ua (β‘-map Ξ» { (a , b , c) β a , c , b }) (β‘-map Ξ» { (a , b , c) β a , c , b }) Rel β .dual-β€ fβ€g x y w = fβ€g y x w Rel β .β©-le-l x y (a , _) = a Rel β .β©-le-r x y (_ , b) = b Rel β .β©-univ hβ€f hβ€g x y h = hβ€f x y h , hβ€g x y h

This will make more sense when we see the construction of $\mathbf{Rel}$ belowβ©οΈ

This is an allegorical (ha) name to emphasize the reason why applying the inverse changes the order of multiplication: To put on socks and shoes, you must first put on your socks, and only then your shoes; but taking them off, the first thing to come off are the shoes, and only then can you remove your socks.β©οΈ

as a hint:

*joins*in your lattice become compositionβ©οΈrather precariousβ©οΈ