module Cat.Bi.Instances.Relations
  {o β„“} {C : Precategory o β„“} (reg : is-regular C) where

Relations in a regular categoryπŸ”—

This module defines the bicategory of relations in arbitrary regular categories β€” categories with pullback-stable image factorisations. Relations between objects can be defined in arbitrary categories1, but in finite-products categories, the definition takes an especially pleasant form: A relation is a subobject of the Cartesian product

Unlike the more general bicategory of spans which can be defined for an arbitrary category with pullbacks the definition of a bicategory of relations does need an honest regular category. Before we get into the details of the construction, let’s introduce some notation:

Following (Johnstone 2002), relations will be denoted using lowercase Greek letters: we will write a relation as leaving its domain implicit. Any relation can be factored2 into morphisms and β€” we shall say that the pair tabulates

_↬_ : Ob β†’ Ob β†’ Type (o βŠ” β„“)
_↬_ a b = Subobject (a βŠ—β‚€ b)

For intuition, a tabulation of exhibits as the object of witnesses for with the maps and determining the β€œsource” and β€œtarget” of each witness. The condition that be a subobject ensures we have at most one witness in for a pair When speaking informally, we may regard the maps as exhibiting as the total space of a family over From that point of view, it’s natural to write the fibre over some as 3

The identity relation is tabulated by the pair which is easily seen to be a subobject.

id-rel : βˆ€ {a} β†’ a ↬ a
id-rel {a} .domain = a
id-rel {a} .map = Ξ΄
id-rel {a} .monic g h x = by-π₁ $
  ⟨ g , g ⟩       β‰‘Λ˜βŸ¨ ⟨⟩∘ g βˆ™ apβ‚‚ ⟨_,_⟩ (idl g) (idl g) βŸ©β‰‘Λ˜
  ⟨ id , id ⟩ ∘ g β‰‘βŸ¨ x βŸ©β‰‘
  ⟨ id , id ⟩ ∘ h β‰‘βŸ¨ ⟨⟩∘ h βˆ™ apβ‚‚ ⟨_,_⟩ (idl h) (idl h) βŸ©β‰‘
  ⟨ h , h ⟩       ∎

Relational composition is slightly more intricate. Given relations we may compose them at the level of spans by taking the pullback

whose generalised elements are pairs satisfying Thinking of and as bundles over their codomain, the fibre of over is the β€œsum type”

which is not a subobject of since there might be multiple choices of β€œbridge” element As a concrete failure, think in and consider composing the implication order on with its converse: The fibre over has distinct elements corresponding to and

∘-rel : βˆ€ {a b c} β†’ b ↬ c β†’ a ↬ b β†’ a ↬ c
∘-rel {a} {b} {c} Ο† ψ = composite module ∘-rel where
  module Ο† = Relation Ο†
  module ψ = Relation ψ

  inter : Pullback C ψ.tgt Ο†.src
  inter = lex.pullbacks _ _

Can we fix it? Yes! Since is a regular category, our morphism factors as a strong epimorphism onto its image

which is the free subobject generated by Having a nice instrumental property is not a guarantee that this is the correct definition, but it does make it more likely to be correct.4

  it : Hom (inter .apex) (a βŠ—β‚€ c)
  it = ⟨ ψ.src ∘ inter .p₁ , Ο†.tgt ∘ inter .pβ‚‚ ⟩

  composite : a ↬ c
  composite = Im it

Associativity of relational compositionπŸ”—

If we are to make a bicategory out of relations, then we need to get our hands on an associator morphism β€” put more plainly, using that is a preorder, a proof that Suppose our relations are given by and We’ll prove that this composition is associative by exhibiting both and as quotients of a larger, β€œunbiased” composition.

Put all your maps in order and form the huge pullback

whose sheer size might warrant the reader take a moment, out of respect. My claim is that the composite is tabulated by the image of

Let’s see how to get there.

  j : Hom (X .apex) (a βŠ—β‚€ d)
  j = ⟨ t₁ ∘ u₁ ∘ x₁ , rβ‚‚ ∘ vβ‚‚ ∘ xβ‚‚ ⟩

Factor as

That’s the composite To then add on the first step is to take the pullback

but note that we have so we can construct a map satisfying and

  Ξ± : Hom (X .apex) ([rs]t.inter .apex)
  Ξ± = [rs]t.inter .universal {p₁' = u₁ ∘ x₁} {pβ‚‚' = q ∘ xβ‚‚} comm where abstract

Now, both squares in the diagram below are pullbacks, so the large rectangle is a pullback, too.

  remβ‚€ : is-pullback C (u₁ ∘ x₁) tβ‚‚ xβ‚‚ (s₁ ∘ v₁)
  rem₀ = pasting-left→outer-is-pullback
    (st.inter .has-is-pb)
    (rotate-pullback (X .has-is-pb))
    (pulll (st.inter .square) βˆ™ extendr (sym (X .square)))

Now, by definition, we have and is also the source map in the composite so we may rewrite the pullback rectangle as

which, since the right square is a pullback, means the left one is, too; Since is a strong epi, is, too.

  abstract
    rem₁ : is-pullback C (ξ₁ ∘ Ξ±) tβ‚‚ xβ‚‚ ((π₁ ∘ i {f = rs.it}) ∘ q)
    rem₁ = transport
      (apβ‚‚ (Ξ» x y β†’ is-pullback C x (Relation.tgt t) (X .p₁) y)
        (sym ([rs]t.inter .pβ‚βˆ˜universal))
        (sym (pullr (sym (factor rs.it .factors)) βˆ™ Ο€β‚βˆ˜βŸ¨βŸ©))) remβ‚€


    Ξ±-is-pb : is-pullback C Ξ± ΞΎβ‚‚ xβ‚‚ q
    Ξ±-is-pb = pasting-outerβ†’left-is-pullback ([rs]t.inter .has-is-pb) rem₁ ([rs]t.inter .pβ‚‚βˆ˜universal)

  Ξ±-cover : is-strong-epi C Ξ±
  α-cover = stable _ _ (out! {pa = is-strong-epi-is-prop C _} (factor rs.it .mediate∈E)) α-is-pb

The purpose of all this calculation is the following: Postcomposing with a strong epimorphism preserves images, so the image of which tabulates will be the same as that of

which we can calculate is exactly β€” just like we wanted!

  [rs]tβ‰…i : Im ⟨ t₁ ∘ [rs]t.inter .p₁ , (Ο€β‚‚ ∘ i) ∘ [rs]t.inter .pβ‚‚ ⟩
      Sub.β‰… Im ⟨ t₁ ∘ u₁ ∘ x₁ , rβ‚‚ ∘ vβ‚‚ ∘ xβ‚‚ ⟩
  [rs]t≅i = subst (λ e → Im [rs]t.it Sub.≅ Im e)
    (⟨⟩∘ _ βˆ™ apβ‚‚ ⟨_,_⟩
      (pullr ([rs]t.inter .pβ‚βˆ˜universal))
      ( pullr ([rs]t.inter .pβ‚‚βˆ˜universal)
      βˆ™ extendl (pullr (sym (factor _ .factors)) βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©)))
    (image-pre-cover [rs]t.it _ Ξ±-cover)

Now do that whole thing over again. I’m not joking: start by forming the pullback that defines define a map from into it, show that is a cover, so is tabulated by the same map out of that we just showed tabulates It’s such blatant repetition that I’ve omitted it from the page: you can choose to show hidden code if you want to look at the formalisation.

  Ξ² : Hom (X .apex) (r[st].inter .apex)
  Ξ² = r[st].inter .universal {p₁' = q ∘ x₁} {pβ‚‚' = vβ‚‚ ∘ xβ‚‚} comm where abstract
    comm : (Ο€β‚‚ ∘ i) ∘ q {f = st.it} ∘ x₁ ≑ r₁ ∘ vβ‚‚ ∘ xβ‚‚
    comm = pulll (pullr (sym (factor st.it .factors)) βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©)
         βˆ™ pullr (sym (X .square)) βˆ™ extendl (rs.inter .square)

  abstract
    remβ‚‚ : is-pullback C (ΞΆβ‚‚ ∘ Ξ²) r₁ x₁ ((Ο€β‚‚ ∘ i) ∘ q {f = st.it})
    remβ‚‚ = transport
      (apβ‚‚ (Ξ» x y β†’ is-pullback C x (Relation.src r) x₁ y)
        (sym (r[st].inter .pβ‚‚βˆ˜universal))
        (sym (pullr (sym (factor st.it .factors)) βˆ™ Ο€β‚‚βˆ˜βŸ¨βŸ©)))
      (pasting-left→outer-is-pullback
        (rotate-pullback (rs.inter .has-is-pb)) (X .has-is-pb)
        (extendl (sym (rs.inter .square)) βˆ™ pushr (X .square)))

    Ξ²-is-pb : is-pullback C Ξ² ΢₁ x₁ q
    β-is-pb = pasting-outer→left-is-pullback
      (rotate-pullback (r[st].inter .has-is-pb))
      remβ‚‚
      (r[st].inter .pβ‚βˆ˜universal)

  Ξ²-cover : is-strong-epi C Ξ²
  β-cover = stable _ _ (out! {pa = is-strong-epi-is-prop C _} (factor st.it .mediate∈E)) β-is-pb

  r[st]β‰…i : Im r[st].it Sub.β‰… Im j
  r[st]β‰…i = subst (Ξ» e β†’ Im r[st].it Sub.β‰… Im e)
    (⟨⟩∘ _ βˆ™ apβ‚‚ ⟨_,_⟩ (pullr (r[st].inter .pβ‚βˆ˜universal) βˆ™ extendl (pullr (sym (factor _ .factors)) βˆ™ Ο€β‚βˆ˜βŸ¨βŸ©))
                       (pullr (r[st].inter .pβ‚‚βˆ˜universal)))
    (image-pre-cover r[st].it _ Ξ²-cover)

  done : Im r[st].it Sub.β‰… Im [rs]t.it
  done = r[st]β‰…i Sub.∘Iso ([rs]tβ‰…i Sub.Iso⁻¹)

The bicategory of relationsπŸ”—

That is, fortunately, the hardest part of the proof. It remains to construct these three maps:

∘-rel-monotone
  : βˆ€ {b c d} {r r' : c ↬ d} {s s' : b ↬ c}
  β†’ r β‰€β‚˜ r' β†’ s β‰€β‚˜ s' β†’ ∘-rel r s β‰€β‚˜ ∘-rel r' s'

∘-rel-idr : βˆ€ {a b} (f : a ↬ b) β†’ ∘-rel f id-rel Sub.β‰… f
∘-rel-idl : βˆ€ {a b} (f : a ↬ b) β†’ ∘-rel id-rel f Sub.β‰… f

Witnessing, respectively, that relational composition respects inclusion of subobjects in both its arguments, and that it has the identity relation as right and left identities. These proofs are less interesting, since they are routine applications of the universal property of images, and a lot of annoying calculations with products and pullbacks.

The curious reader can choose to show hidden code to display the proofs, but keep in mind that they are not commented.

∘-rel-monotone {r = r} {r'} {s} {s'} α β =
  Im-universal (∘-rel.it r s) _
    {e = factor _ .mediate ∘ ∘-rel.inter r' s' .universal
      {p₁' = Ξ² .map ∘ ∘-rel.inter _ _ .p₁}
      {pβ‚‚' = Ξ± .map ∘ ∘-rel.inter _ _ .pβ‚‚}
      ( pullr (pulll (sym (Ξ² .sq) βˆ™ idl _))
      βˆ™ sym (pullr (pulll (sym (Ξ± .sq) βˆ™ idl _))
      βˆ™ (assoc _ _ _ Β·Β· sym (∘-rel.inter r s .square) Β·Β· sym (assoc _ _ _))))}
    (Product.uniqueβ‚‚ (lex.products _ _)
      (Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr refl)
      (Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ pullr refl)
      (  apβ‚‚ _∘_ refl (pulll (sym (factor _ .factors)))
      Β·Β· pulll Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ pullr (∘-rel.inter r' s' .pβ‚βˆ˜universal)
      Β·Β· pullr (pulll (sym (Ξ² .sq) βˆ™ idl _)))
      (  apβ‚‚ _∘_ refl (pulll (sym (factor _ .factors)))
      Β·Β· pulll Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ pullr (∘-rel.inter r' s' .pβ‚‚βˆ˜universal)
      Β·Β· pullr (pulll (sym (Ξ± .sq) βˆ™ idl _))))

∘-rel-idr f = Sub-antisym fid≀f f≀fid where
  fid≀f : ∘-rel f id-rel β‰€β‚˜ f
  fid≀f = Im-universal _ _ {e = ∘-rel.inter f id-rel .pβ‚‚} $ sym $ ⟨⟩-unique _
    (sym (∘-rel.inter f id-rel .square βˆ™ sym (assoc _ _ _)) βˆ™ eliml Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ introl Ο€β‚βˆ˜βŸ¨βŸ©)
    (assoc _ _ _)

  f≀fid : f β‰€β‚˜ ∘-rel f id-rel
  f≀fid .map = factor _ .mediate ∘
    ∘-rel.inter f id-rel .universal {p₁' = Relation.src f} {pβ‚‚' = id}
      (eliml Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ intror refl)
  f≀fid .sq = idl _ βˆ™ sym (pulll (sym (factor _ .factors)) βˆ™ ⟨⟩∘ _ βˆ™ sym (⟨⟩-unique _
    (sym (apβ‚‚ _∘_ (eliml Ο€β‚βˆ˜βŸ¨βŸ©) refl βˆ™ ∘-rel.inter _ _ .pβ‚βˆ˜universal))
    (sym (pullr (∘-rel.inter _ _ .pβ‚‚βˆ˜universal) βˆ™ idr _))))

∘-rel-idl f = Sub-antisym idf≀f f≀idf where
  idf≀f : ∘-rel id-rel f β‰€β‚˜ f
  idf≀f = Im-universal _ _ {e = ∘-rel.inter id-rel f .p₁} $ sym $ ⟨⟩-unique _
    (assoc _ _ _)
    (assoc _ _ _ βˆ™ ∘-rel.inter id-rel f .square βˆ™ eliml Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ introl Ο€β‚‚βˆ˜βŸ¨βŸ©)

  f≀idf : f β‰€β‚˜ ∘-rel id-rel f
  f≀idf .map = factor _ .mediate ∘
    ∘-rel.inter id-rel f .universal {p₁' = id} {pβ‚‚' = Relation.tgt f}
      (idr _ βˆ™ sym (eliml Ο€β‚βˆ˜βŸ¨βŸ©))
  f≀idf .sq = idl _ βˆ™ sym (pulll (sym (factor _ .factors)) βˆ™ ⟨⟩∘ _ βˆ™ sym (⟨⟩-unique _
    (sym (pullr (∘-rel.inter id-rel f .pβ‚βˆ˜universal) βˆ™ idr _))
    (sym (pullr (∘-rel.inter id-rel f .pβ‚‚βˆ˜universal) βˆ™ eliml Ο€β‚‚βˆ˜βŸ¨βŸ©))))

open Prebicategory hiding (Ob ; Hom)
open make-natural-iso
open Functor

That aside over with, we can set up the bicategory of relations in Monotonicity of the composition operation is all we need for functoriality, and our coherence isomorphisms automatically satisfy naturality and their identities (triangle/pentagon) since is always a preorder.

private
  ∘-rel-fun : βˆ€ {a b c} β†’ Functor (Sub (b βŠ—β‚€ c) Γ—αΆœ Sub (a βŠ—β‚€ b)) (Sub (a βŠ—β‚€ c))
  ∘-rel-fun .Fβ‚€ (a , b) = ∘-rel a b
  ∘-rel-fun .F₁ (f , g) = ∘-rel-monotone  f g

  ∘-rel-fun .F-id    = hlevel 1 _ _
  ∘-rel-fun .F-∘ _ _ = hlevel 1 _ _

Rel[_] : Prebicategory o (o βŠ” β„“) β„“
Rel[_] .Prebicategory.Ob = Ob
Rel[_] .Prebicategory.Hom a b = Sub (a βŠ—β‚€ b)
Rel[_] .id      = id-rel
Rel[_] .compose = ∘-rel-fun

The objects are those of The maps are all the subobjects The identity relation is the graph of the identity function, and relational composition is a mess.

Rel[_] .unitor-l = to-natural-iso mk where
  mk : make-natural-iso Id (Bifunctor.Right ∘-rel-fun id-rel)
  mk .eta x = ∘-rel-idl x .Sub.from
  mk .inv x = ∘-rel-idl x .Sub.to
  mk .eta∘inv x = Sub.invr (∘-rel-idl x)
  mk .inv∘eta x = Sub.invl (∘-rel-idl x)
  mk .natural x y f = hlevel 1 _ _
Rel[_] .unitor-r = to-natural-iso mk where
  mk : make-natural-iso Id (Bifunctor.Left ∘-rel-fun id-rel)
  mk .eta x = ∘-rel-idr x .Sub.from
  mk .inv x = ∘-rel-idr x .Sub.to
  mk .eta∘inv x = Sub.invr (∘-rel-idr x)
  mk .inv∘eta x = Sub.invl (∘-rel-idr x)
  mk .natural x y f = hlevel 1 _ _
Rel[_] .associator {a} {b} {c} {d} = to-natural-iso mk where
  mk : make-natural-iso (compose-assocˑ ∘-rel-fun) (compose-assocʳ ∘-rel-fun {A = a} {b} {c} {d})
  mk .eta (x , y , z) = ∘-rel-assoc x y z .Sub.from
  mk .inv (x , y , z) = ∘-rel-assoc x y z .Sub.to
  mk .eta∘inv (x , y , z) = Sub.invr (∘-rel-assoc x y z)
  mk .inv∘eta (x , y , z) = Sub.invl (∘-rel-assoc x y z)
  mk .natural (x , y , z) (Ξ± , Ξ² , Ξ³) f =
    ≀-over-is-prop
      (compose-assocΚ³ {H = Ξ» x y β†’ Sub (x βŠ—β‚€ y)} ∘-rel-fun .F₁ f Sub.∘ ∘-rel-assoc x y z .Sub.from)
      (∘-rel-assoc Ξ± Ξ² Ξ³ .Sub.from Sub.∘ compose-assocΛ‘ {H = Ξ» x y β†’ Sub (x βŠ—β‚€ y)} ∘-rel-fun .F₁ f)
Rel[_] .triangle f g = hlevel 1 _ _
Rel[_] .pentagon f g h i = hlevel 1 _ _

  1. A relation is a span such that are jointly monic.β†©οΈŽ

  2. Recall that, for we have a tautological decomposition β†©οΈŽ

  3. Points in this fibre is a morphism satisfying and β†©οΈŽ

  4. From a point of view informed by parametricity, one might argue that this is not only the correct move, but the only possible way of turning a map into a subobject.β†©οΈŽ


References

  • Johnstone, Peter T. 2002. Sketches of an Elephant: a Topos Theory Compendium. Oxford Logic Guides. New York, NY: Oxford Univ. Press. https://cds.cern.ch/record/592033.