module Cat.Allegory.Base where


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
  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.

    _≀_       : βˆ€ {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')

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:

    _†     : βˆ€ {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.

    _∩_    : βˆ€ {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

      : βˆ€ {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
    : βˆ€ {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
    (Ξ» h h≀f∩gα΅’ β†’
        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α΅’ β†’
        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, 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

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.β†©οΈŽ

  3. as a hint: joins in your lattice become compositionβ†©οΈŽ

  4. rather precariousβ†©οΈŽ