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 has an underlying precategory (whose morphisms we call relations), but, more importantly, an ordering relation on the relations, which we think of as inclusion in the usual sense1. When considered with this ordering, must be a locally posetal bicategory: a bicategory 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 and must imply 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, must be equipped with an involution on its Hom-sets: This is the usual opposite of a relation, i.e.Β  and, as you have noticed, we will write the opposite of as The involution must play nice with the ordering, and it must follow the socks-and-shoes principle2 w.r.t. composition:

  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 and if is equivalent to for every then 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 to get it out of the way: is exactly the same as

  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 is equivalently given by We ellaborate the correspondence in one direction: Suppose that Pinging the dual across, we get which (by the definition of meet) is equivalent to the conjunction of and But ponging the dual on either of those, we get and which mean

  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, As usual, every universe level gives an allegory whose objects are sets, and morphisms are relations. Note that, in the absence of propositional resizing, underlying category is not locally The set of propositions lives in the successor universe, not in

open Allegory
open Precategory


Ordering of relations is as one would expect: is defined to mean every pair is also When seen as subsets of 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 and is given by the relation which βbridges the gapβ, i.e.Β  iff. there exists some such that and 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 but in either case, what we want to show that relates the same pairs as In the interesting direction, weβre given some and a witness that but what we wanted was to show Fortunately if we we set then 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., is

• The relation given by the intersection of the subsets representing and or
• The relation which relates and iff. both and relate them.

The dual is given by inverting the order of arguments to 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β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! Ξ» 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


1. This will make more sense when we see the construction of 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.β©οΈ