{-# OPTIONS --lossy-unification -vtc.def:20 #-}
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 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 , 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

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 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  β-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 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   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 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.