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
$A$
has an underlying precategory (whose morphisms we call
**relations**), but, more importantly, an ordering relation
$fβ€g$
on the relations, which we think of as inclusion in the usual sense^{1}. When considered with this ordering,
$A$
must be a *locally posetal bicategory*: a bicategory
$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β€f_{β²}$ and $gβ€g_{β²}$ must imply $fgβ€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,
$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_{o}f_{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β€g$
is equivalent to
$fβ€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}β€g$ is exactly the same as $fβ€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β©g)_{o}$ is equivalently given by $f_{o}β©g_{o}.$ We ellaborate the correspondence in one direction: Suppose that $fβ€(fβ©g)_{o}.$ Pinging the dual across, we get $h_{o}β€(fβ©g),$ which (by the definition of meet) is equivalent to the conjunction of $h_{o}β€f$ and $h_{o}β€g.$ But ponging the dual on either of those, we get $hβ€f_{o}$ and $hβ€g_{o},$ which mean $hβ€f_{o}β©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**,
$Rel.$
As usual, every universe level
$ΞΊ$
gives an allegory
$Rel_{ΞΊ},$
whose objects are
$ΞΊ-small$
sets, and morphisms are
$ΞΊ-small$
relations. Note that, in the absence of propositional resizing,
$Relβs$
underlying category is *not* locally
$ΞΊ-small:$
The set of
$ΞΊ-small$
propositions lives in the successor universe, not in
$ΞΊ.$

Ordering of relations is as one would expect: $Rβ€S$ is defined to mean every $R-related$ pair $(x,y)$ is also $S-related.$ When seen as subsets of $AΓ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β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 $Id,$ but in either case, what we want to show that $(x,y)β¦β(a:A),Id(x,a)β§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 $Id(x,a),$ then $R(x,y)β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 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β©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 1) Rel β ._β R x y = R y x Rel β .modular R S T x y (Ξ± , Ξ²) = case Ξ± of Ξ» where z x~z z~y β inc (z , (x~z , inc (y , Ξ² , z~y)) , z~y)

##
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! Ξ» z x~z z=y β subst (Ξ» e β β£ R x e β£) z=y x~z) Ξ» w β inc (y , w , inc refl) Rel β .cat .assoc T S R = ext Ξ» x y β Ξ©-ua (rec! Ξ» a b r s t β inc (b , r , inc (a , s , t))) (rec! Ξ» a r b s t β inc (b , inc (a , r , s) , t)) Rel β .β€-thin = hlevel 1 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 $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β©οΈ