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 sense¹. When considered with this ordering, $\mathcal{A}$ must be a locally posetal bicategory: a bicategory $\mathcal{A}\text{,}$ 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^{\prime }$ and $g\le g^{\prime }$ must imply $fg\le f^{\prime }{g}^{\prime }\text{.}$ 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  _†
  infixr  _∩_
  infixr  _◆_
  infix  _≤_

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)\text{,}$ and, as you have noticed, we will write the opposite of $f$ as $f^o\text{.}$ The involution must play nice with the ordering, and it must follow the socks-and-shoes principle² w.r.t. composition: $(fg{)}^o=g^o{f}^o\text{.}$

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

  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\text{,}$ if $f\le g$ is equivalent to $f\le h$ for every $f\text{,}$ then $g=h\text{.}$ 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\text{.}$

  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\text{.}$ We ellaborate the correspondence in one direction: Suppose that $f\le (f\cap g{)}^o\text{.}$ Pinging the dual across, we get $h^o\le (f\cap g)\text{,}$ which (by the definition of meet) is equivalent to the conjunction of $h^o\le f$ and $h^o\le g\text{.}$ But ponging the dual on either of those, we get $h\le f^o$ and $h\le g^o\text{,}$ which mean $h\le f^o\cap g^o\text{.}$

  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, $\mathbf{Rel}\text{.}$ As usual, every universe level $\kappa$ gives an allegory ${\mathbf{Rel}}_{\kappa }\text{,}$ whose objects are $\kappa \text{-small}$ sets, and morphisms are $\kappa \text{-small}$ relations. Note that, in the absence of propositional resizing, $\mathbf{Rel}\text{’s}$ underlying category is not locally $\kappa \text{-small:}$ The set of $\kappa \text{-small}$ propositions lives in the successor universe, not in $\kappa \text{.}$

open Allegory
open Precategory

Ordering of relations is as one would expect: $R\le S$ is defined to mean every $R\text{-related}$ pair $(x,y)$ is also $S\text{-related.}$ When seen as subsets of $A\times B\text{,}$ 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)\text{.}$ 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 $\mathrm{Id}\text{,}$ but in either case, what we want to show that $$(x,y)\mapsto \exists (a:A),\mathrm{Id}(x,a)\wedge R(a,y)$$ relates the same pairs as $R\text{.}$ In the interesting direction, we’re given some $a:A$ and a witness that $R(a,y)\text{:}$ but what we wanted was to show $R(x,y)\text{!}$ Fortunately if we we set $\mathrm{Id}(x,a)\text{,}$ then $R(x,y)\simeq R(a,y)\text{,}$ 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\cap S$ is

• The relation given by the intersection of the subsets representing $R$ and $S\text{,}$ 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\text{,}$ 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 (α , β) = case α of λ where
  z x~z z~y → inc (z , (x~z , inc (y , β , z~y)) , z~y)

Rel ℓ .cat .Hom-set x y = hlevel 
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 
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