{-# OPTIONS --lossy-unification #-}
open import Cat.Diagram.Pullback.Properties
open import Cat.Morphism.Factorisation
open import Cat.Morphism.StrongEpi
open import Cat.Instances.Functor
open import Cat.Instances.Product
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Bi.Base
open import Cat.Prelude
open import Cat.Regular

import Cat.Displayed.Instances.Subobjects as Sub
import Cat.Functor.Bifunctor as Bifunctor
import Cat.Regular.Image as Img
import Cat.Reasoning as Cr

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

open Pullback
open is-regular reg
open Binary-products C lex.products
open Factorisation
open Cr C
open Sub C
open Img reg

Relations in a regular category🔗

This module defines the bicategory of relations in arbitrary regular categories — categories with pullback-stable image factorisations. Relations $\phi :a\looparrowright b$ between objects $a,b:\mathcal{C}$ can be defined in arbitrary categories¹, but in finite-products categories, the definition takes an especially pleasant form: A relation $\phi :a\looparrowright b$ is a subobject of the Cartesian product $a\times b\text{.}$

Unlike the more general bicategory of spans ${\mathrm{Spans}}_{\mathcal{C}}\text{,}$ which can be defined for an arbitrary category with pullbacks $\mathcal{C}\text{,}$ 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 $\phi :R\hookrightarrow A\times B$ as $\phi :A\looparrowright B\text{,}$ leaving its domain $R$ implicit. Any relation $\phi$ can be factored² into morphisms $s:R\to A$ and $t:R\to B$ — we shall say that the pair $(s,t)$ tabulates $\phi \text{.}$

_↬_ : Ob → Ob → Type (o ⊔ ℓ)
_↬_ a b = Subobject (a ⊗₀ b)

For intuition, a tabulation $(f,g):R\hookrightarrow A\times B$ of $\phi :A\looparrowright B$ exhibits $R$ as the object of witnesses for $\phi \text{,}$ with the maps $f$ and $g$ determining the “source” and “target” of each witness. The condition that $(f,g)$ be a subobject ensures we have at most one witness in $r$ for a $\phi \text{-related}$ pair $a,b\text{.}$ When speaking informally, we may regard the maps $(f,g)$ as exhibiting $R$ as the total space of a family over $A\times B\text{;}$ From that point of view, it’s natural to write the fibre over some $(x,y)$ as $R(x,y).$³

module Relation {a b} (r : _↬_ a b) where
  rel : Ob
  rel = r .domain

  src : Hom rel a
  src = π₁ ∘ r .map

  tgt : Hom rel b
  tgt = π₂ ∘ r .map

The identity relation $\iota :a\looparrowright a$ is tabulated by the pair $(\mathrm{id},\mathrm{id}):A\hookrightarrow A\times A\text{,}$ 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 $(s,t):R\hookrightarrow B\times C\text{,}$ $(s^{\prime },t^{\prime }):S\hookrightarrow A\times B\text{,}$ we may compose them at the level of spans by taking the pullback

whose generalised elements are pairs $(a,b):\Gamma \to R\times S$ satisfying $t^{\prime }(b)=s(a)\text{.}$ Thinking of $(s,t)$ and $(s^{\prime },t^{\prime })$ as bundles over their codomain, the fibre of $R{\times }_{B}S$ over $x,y$ is the “sum type”

which is not a subobject of $A\times C\text{,}$ since there might be multiple choices of “bridge” element $b\text{!}$ As a concrete failure, think in $\mathbf{Sets}\text{,}$ and consider composing the implication order on $\{0,1\}$ with its converse: The fibre over $(0,0)$ has distinct elements corresponding to $0\le 0\ge 0$ and $0\le 1\ge 0\text{.}$

∘-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 $\mathcal{C}$ is a regular category, our morphism $(s^{\prime },t):R{\times }_{B}S\to A\times C$ factors as a strong epimorphism onto its image

which is the free subobject generated by $(s^{\prime },t)\text{.}$ 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.⁴

  it : Hom (inter .apex) (a ⊗₀ c)
  it = ⟨ ψ.src ∘ inter .p₁ , φ.tgt ∘ inter .p₂ ⟩

  composite : a ↬ c
  composite = Im it

∘-rel-assoc
  : ∀ {a b c d}
  → (φ : c ↬ d)
  → (ψ : b ↬ c)
  → (χ : a ↬ b)
  → (∘-rel φ (∘-rel ψ χ)) Sub.≅ (∘-rel (∘-rel φ ψ) χ)
∘-rel-assoc {a} {b} {c} {d} r s t = done where
  private
    module rs = ∘-rel r s
    module st = ∘-rel s t
    module [rs]t = ∘-rel (∘-rel r s) t
    module r[st] = ∘-rel r (∘-rel s t)
    v₂ = rs.inter .p₂
    v₁ = rs.inter .p₁

    u₂ = st.inter .p₂
    u₁ = st.inter .p₁
    open Relation r renaming (src to r₁ ; tgt to r₂) hiding (rel)
    open Relation s renaming (src to s₁ ; tgt to s₂) hiding (rel)
    open Relation t renaming (src to t₁ ; tgt to t₂) hiding (rel)

    i : ∀ {x y} {f : Hom x y} → Hom im[ f ] y
    i = factor _ .forget

    q : ∀ {x y} {f : Hom x y} → Hom x im[ f ]
    q = factor _ .mediate

    ξ₁ = [rs]t.inter .p₁
    ξ₂ = [rs]t.inter .p₂

    ζ₁ = r[st].inter .p₁
    ζ₂ = r[st].inter .p₂

  X : Pullback C (rs.inter .p₁) (st.inter .p₂)
  X = lex.pullbacks (rs.inter .p₁) (st.inter .p₂)
  private module X = Pullback X renaming (p₂ to x₁ ; p₁ to x₂)
  open X using (x₂ ; x₁)

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 $\mathrm{Sub}(A\times B)$ is a preorder, a proof that $(\phi \psi )\chi \cong \phi (\psi \chi )\text{.}$ Suppose our relations are given by $\chi =(t_1,t_2):T\hookrightarrow A\times B\text{,}$ $\psi =(s_1,s_2):S\hookrightarrow B\times C\text{,}$ and $\phi =(r_1,r_2):R\hookrightarrow C\times D\text{.}$ We’ll prove that this composition is associative by exhibiting both $(\phi \psi )\chi$ and $\phi (\psi \chi )$ 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 $(\phi \psi )\chi$ 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 $⟨t_1{u}_1,s_2{u}_2⟩$ as

That’s the composite $\phi \psi \text{.}$ To then add on $\chi \text{,}$ the first step is to take the pullback

but note that we have $t_2{u}_1{x}_1={\pi }_{1}iq{x}_2\text{,}$ so we can construct a map $\alpha :X\to I{\times }_{B}T$ satisfying ${\xi }_1\alpha =u_1{x}_1$ and ${\xi }_2\beta =q{x}_2\text{.}$

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

    comm : t₂ ∘ u₁ ∘ x₁ ≡ (π₁ ∘ i {f = rs.it}) ∘ q ∘ x₂
    comm = pulll (st.inter .square)
         ∙ pullr (sym (X .square))
         ∙ sym ( pulll (pullr (sym (factor _ .factors)))
               ∙ ap₂ _∘_ π₁∘⟨⟩ refl ∙ sym (assoc _ _ _))

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 ${\xi }_1\alpha =u_1{x}_1\text{,}$ and $s_1{v}_1$ is also the source map ${\pi }_{1}iq:I\to B$ in the composite $\phi \psi \text{,}$ so we may rewrite the pullback rectangle as

which, since the right square is a pullback, means the left one is, too; Since $q$ is a strong epi, $\alpha$ 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! (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 $⟨t_1{\xi }_1,{\pi }_{2}i{\xi }_2⟩\text{,}$ which tabulates $(\phi \psi )\chi \text{,}$ will be the same as that of

which we can calculate is exactly $⟨t_1{u}_1{x}_1,r_2{v}_2{x}_2⟩$ — 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 $R{\times }_{B}J$ that defines $\phi (\psi \chi )\text{,}$ define a map $\beta$ from $X$ into it, show that $\beta$ is a cover, so $\phi (\psi \chi )$ is tabulated by the same map out of $X$ that we just showed tabulates $(\phi \psi )\chi \text{.}$ 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! (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 = [rs]t≅i Sub.Iso⁻¹ Sub.∘Iso r[st]≅i

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 $\mathcal{C}\text{:}$ Monotonicity of the composition operation is all we need for functoriality, and our coherence isomorphisms automatically satisfy naturality and their identities (triangle/pentagon) since $\mathrm{Sub}(-\times -)$ 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  _ _
  ∘-rel-fun .F-∘ _ _ = hlevel  _ _

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 $\mathcal{C}\text{;}$ The maps $a\looparrowright b$ are all the subobjects $\mathrm{Sub}(a\times b)\text{;}$ 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  _ _
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  _ _
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  _ _
Rel[_] .pentagon f g h i = hlevel  _ _