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 A\mathcal{A} has an underlying precategory (whose morphisms we call relations), but, more importantly, an ordering relation f≀gf \le g on the relations, which we think of as inclusion in the usual sense1. When considered with this ordering, A\mathcal{A} must be a locally posetal bicategory: a bicategory A\mathcal{A}, 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 f≀fβ€²f \le f' and g≀gβ€²g \le g' must imply fg≀fβ€²gβ€²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, A\mathcal{A} must be equipped with an involution on its Hom-sets: This is the usual opposite of a relation, i.e.Β Ro(x,y)=R(y,x)R^o(x,y) = R(y,x), and, as you have noticed, we will write the opposite of ff as fof^o. The involution must play nice with the ordering, and it must follow the socks-and-shoes principle2 w.r.t. composition: (fg)o=gofo(fg)^o = g^of^o.

    _†     : βˆ€ {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 gg and hh, if f≀gf \le g is equivalent to f≀hf \le h for every ff, then g=hg = 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
    : βˆ€ {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(-)^o to get it out of the way: fo≀gf^o \le g is exactly the same as f≀gof \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∩g)o(f \cap g)^o is equivalently given by fo∩gof^o \cap g^o. We ellaborate the correspondence in one direction: Suppose that f≀(f∩g)of \le (f \cap g)^o. Pinging the dual across, we get ho≀(f∩g)h^o \le (f \cap g), which (by the definition of meet) is equivalent to the conjunction of ho≀fh^o \le f and ho≀gh^o \le g. But ponging the dual on either of those, we get h≀foh \le f^o and h≀goh \le g^o, which mean h≀fo∩goh \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α΅’ β†’
        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, Rel\mathbf{Rel}. As usual, every universe level ΞΊ\kappa gives an allegory RelΞΊ\mathbf{Rel}_\kappa, whose objects are ΞΊ\kappa-small sets, and morphisms are ΞΊ\kappa-small relations. Note that, in the absence of propositional resizing, Rel\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≀SR \le S is defined to mean every RR-related pair (x,y)(x, y) is also SS-related. When seen as subsets of AΓ—BA \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 RR and SS is given by the relation which β€œbridges the gap”, i.e.Β (R∘S)(x,z)(R \circ S)(x, z) iff. there exists some yy such that R(x,y)R(x, y) and S(y,z)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⁑\operatorname{Id}_{}, but in either case, what we want to show that (x,y)β†¦βˆƒ(a:A),Id⁑(x,a)∧R(a,y)(x, y) \mapsto \exists (a : A), \operatorname{Id}_{}(x, a) \land R(a, y) relates the same pairs as RR. In the interesting direction, we’re given some a:Aa : A and a witness that R(a,y)R(a, y): but what we wanted was to show R(x,y)R(x, y)! Fortunately if we we set Id⁑(x,a)\operatorname{Id}_{}(x, a), then R(x,y)≃R(a,y)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∩SR \cap S is

  • The relation given by the intersection of the subsets representing RR and SS, or
  • The relation which relates xx and yy iff. both RR and SS relate them.

The dual is given by inverting the order of arguments to RR, 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 Rel\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.β†©οΈŽ

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

  4. rather precariousβ†©οΈŽ