open import Cat.Prelude

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 sense1. 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')

  infixl 50 _β
infixr 40 _β_
infix 30 _β€_


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 principle2 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
let
in β©-univ (dual-β€α΅£ hα΅β€f) (dual-β€α΅£ hα΅β€g))
let
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$.

open Allegory
open Precategory


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βs4 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


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

2. 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.β©οΈ