open import Cat.Diagram.Coequaliser.RegularEpi
open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Product
open import Cat.Prelude

import Cat.Reasoning

module Cat.Diagram.Congruence {o β} {C : Precategory o β}
(fc : Finitely-complete C) where


Congruencesπ

The idea of congruence is the categorical rephrasing of the idea of equivalence relation. Recall that an equivalence relation on a set is a family of propositions $R : A \times A \to \mathrm{Prop}$ satisfying reflexivity ($R(x,x)$ for all $x$), transitivity ($R(x,y) \land R(y,z) \to R(x,z)$), and symmetry ($R(x,y) \to R(y,x)$). Knowing that $\mathrm{Prop}$ classifies embeddings, we can equivalently talk about an equivalence relation $R$ as being just some set, equipped with a monomorphism $m : R \hookrightarrow A \times A$.

We must now identify what properties of the mono $m$ identify $R$ as being the total space of an equivalence relation. Let us work in the category of sets for the moment. Suppose $R$ is a relation on $A$, and $m : d \hookrightarrow A \times A$ is the monomorphism representing it. Letβs identify the properties of $m$ which correspond to the properties of $R$ weβre interested in:

module _
{β} {A : Set β} {R : β£ A β£ Γ β£ A β£ β Type β}
{rp : β x β is-prop (R x)}
where private
domain : Type β
domain = subtype-classifier.from (Ξ» x β R x , rp x) .fst

m : domain β£ (β£ A β£ Γ β£ A β£)
m = subtype-classifier.from (Ξ» x β R x , rp x) .snd

pβ pβ : domain β β£ A β£
pβ = fst β fst m
pβ = snd β fst m


Reflexivity. $R$ is reflexive if, and only if, the morphisms $p_1, p_2 : d \to A$ have a common left inverse $r : A \to d$.

    R-reflβcommon-inverse
: (β x β R (x , x))
β Ξ£[ rrefl β (β£ A β£ β domain) ]
( (pβ β rrefl β‘ (Ξ» x β x))
Γ (pβ β rrefl β‘ (Ξ» x β x)))
R-reflβcommon-inverse ref = (Ξ» x β (x , x) , ref x) , refl , refl

common-inverseβR-refl
: (rrefl : β£ A β£ β domain)
β (pβ β rrefl β‘ (Ξ» x β x))
β (pβ β rrefl β‘ (Ξ» x β x))
β β x β R (x , x)
common-inverseβR-refl inv p q x = subst R (Ξ» i β p i x , q i x) (inv x .snd)


Symmetry. There is a map $s : d \to d$ which swaps $p_1$ and $p_2$:

    R-symβswap
: (β {x y} β R (x , y) β R (y , x))
β Ξ£[ s β (domain β domain) ] ((pβ β s β‘ pβ) Γ (pβ β s β‘ pβ))
R-symβswap sym .fst ((x , y) , p) = (y , x) , sym p
R-symβswap sym .snd = refl , refl

swapβR-sym
: (s : domain β domain)
β (pβ β s β‘ pβ) β (pβ β s β‘ pβ)
β β {x y} β R (x , y) β R (y , x)
swapβR-sym s p q {x} {y} rel =
subst R (Ξ£-pathp (happly p _) (happly q _)) (s (_ , rel) .snd)


Transitivity. This oneβs a doozy. Since $\mathbf{Sets}$ has finite limits, we have an object of βcomposable pairsβ of $d$, namely the pullback under the cospan $R \xrightarrow{p_1} X \xleftarrow{p_2} R$.

Transitivity, then, means that the two projection maps $p_1q_1, p_2q_2 : (d \times_A d) \rightrightarrows (A \times A)$ β which take a βcomposable pairβ to the βfirst mapβs sourceβ and βsecond mapβs targetβ, respectively β factor through $R$, somehow, i.e.Β we have a $t : (d \times_A d) \to d$ fitting in the diagram below

    s-t-factorβR-transitive
: (t : (Ξ£[ m1 β domain ] Ξ£[ m2 β domain ] (m1 .fst .snd β‘ m2 .fst .fst))
β domain)
β ( Ξ» { (((x , _) , _) , ((_ , y) , _) , _) β x , y } ) β‘ m .fst β t
--  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--      this atrocity is "(pβqβ,pβqβ)" in the diagram
β β {x y z} β R (x , y) β R (y , z) β R (x , z)
s-t-factorβR-transitive compose preserves s t =
subst R (sym (happly preserves _)) (composite .snd)
where composite = compose ((_ , s) , (_ , t) , refl)


Generallyπ

Above, we have calculated the properties of a monomorphism $m : R \hookrightarrow A \times A$ which identify $R$ as an equivalence relation on the object $A$. Note that, since the definition relies on both products and pullbacks, we go ahead and assume the category is finitely complete.

open Cat.Reasoning C
open Pullback
open Product
private module fc = Finitely-complete fc

private
_β_ : Ob β Ob β Ob
A β B = fc.products A B .apex

record is-congruence {A R} (m : Hom R (A β A)) : Type (o β β) where
no-eta-equality


Hereβs the data of a congruence. Get ready, because thereβs a lot of it:

  private module AΓA = Product (fc.products A A)
relβ : Hom R A
relβ = AΓA.Οβ β m
relβ : Hom R A
relβ = AΓA.Οβ β m
private module RΓR = Pullback (fc.pullbacks relβ relβ)
private module AΓAΓA = Pullback (fc.pullbacks relβ relβ)

  field
has-is-monic : is-monic m
-- Reflexivity:

has-refl : Hom A R
refl-pβ : relβ β has-refl β‘ id
refl-pβ : relβ β has-refl β‘ id

-- Symmetry:
has-sym : Hom R R
sym-pβ : relβ β has-sym β‘ relβ
sym-pβ : relβ β has-sym β‘ relβ

-- Transitivity
has-trans : Hom RΓR.apex R

source-target : Hom RΓR.apex AΓA.apex
source-target = AΓA.β¨ relβ β RΓR.pβ , relβ β RΓR.pβ β©AΓA.

field
trans-factors : source-target β‘ m β has-trans

  trans-pβ : relβ β has-trans β‘ relβ β AΓAΓA.pβ
trans-pβ =
pullr (sym trans-factors)
β AΓA.Οββfactor

trans-pβ : relβ β has-trans β‘ relβ β AΓAΓA.pβ
trans-pβ =
pullr (sym trans-factors)
β AΓA.Οββfactor

unpair-trans
: β {X} {pβ' pβ' : Hom X R}
β (sq : relβ β pβ' β‘ relβ β pβ')
β m β has-trans β RΓR.universal sq β‘ AΓA.β¨ relβ β pβ' , relβ β pβ' β©AΓA.
unpair-trans sq =
pulll (sym trans-factors)
Β·Β· apβ AΓA.β¨_,_β© (pullr RΓR.pββuniversal) (pullr RΓR.pββuniversal)

record Congruence-on A : Type (o β β) where
no-eta-equality
field
{domain}    : Ob
inclusion   : Hom domain (A β A)
has-is-cong : is-congruence inclusion
open is-congruence has-is-cong public


The diagonalπ

The first example of a congruence we will see is the βdiagonalβ morphism $\Delta : A \to (A \times A)$, corresponding to the βtrivial relationβ.

diagonal : β {A} β Hom A (A β A)
diagonal {A} = fc.products A A .β¨_,_β© id id


That the diagonal morphism is monic follows from the following calculation, where we use that $\operatorname{id}_{} = \pi_1 \circ \Delta$.

diagonal-is-monic : β {A} β is-monic (diagonal {A})
diagonal-is-monic {A} g h p =
(AΓA.Οβ β diagonal) β g β‘β¨ extendr p β©β‘
(AΓA.Οβ β diagonal) β h β‘β¨ eliml AΓA.Οββfactor β©β‘
h                       β
where module AΓA = Product (fc.products A A)


We now calculate that it is a congruence, using the properties of products and pullbacks. The reflexivity map is given by the identity, and so is the symmetry map; For the transitivity map, we arbitrarily pick the first projection from the pullback of βcomposable pairsβ; The second projection wouldβve worked just as well.

diagonal-congruence : β {A} β is-congruence diagonal
diagonal-congruence {A} = cong where
module AΓA = Product (fc.products A A)
module Pb = Pullback (fc.pullbacks (AΓA.Οβ β diagonal) (AΓA.Οβ β diagonal))
open is-congruence

cong : is-congruence _
cong .has-is-monic = diagonal-is-monic
cong .has-refl = id
cong .refl-pβ = eliml AΓA.Οββfactor
cong .refl-pβ = eliml AΓA.Οββfactor
cong .has-sym = id
cong .sym-pβ = eliml AΓA.Οββfactor β sym AΓA.Οββfactor
cong .sym-pβ = eliml AΓA.Οββfactor β sym AΓA.Οββfactor
cong .has-trans = Pb.pβ
cong .trans-factors = AΓA.uniqueβ
(AΓA.Οββfactor β eliml AΓA.Οββfactor) (AΓA.Οββfactor β eliml AΓA.Οββfactor)
(assoc _ _ _ β Pb.square β eliml AΓA.Οββfactor)
(cancell AΓA.Οββfactor)


Effective congruencesπ

A second example in the same vein as the diagonal is, for any morphism $f : a \to b$, its kernel pair, i.e.Β the pullback of $a \xrightarrow{f} b \xleftarrow{f} a$. Calculating in $\mathbf{Sets}$, this is the equivalence relation generated by $f(x) = f(y)$ β it is the subobject of $a \times a$ consisting of those βvalues which $f$ maps to the same thingβ.

module _ {a b} (f : Hom a b) where
private
module Kp = Pullback (fc.pullbacks f f)
module aΓa = Product (fc.products a a)

kernel-pair : Hom Kp.apex aΓa.apex
kernel-pair = aΓa.β¨ Kp.pβ , Kp.pβ β©aΓa.

private
module rel = Pullback
(fc.pullbacks (aΓa.Οβ β kernel-pair) (aΓa.Οβ β kernel-pair))

kernel-pair-is-monic : is-monic kernel-pair
kernel-pair-is-monic g h p = Kp.uniqueβ {p = extendl Kp.square}
refl refl
(sym (pulll aΓa.Οββfactor) β apβ _β_ refl (sym p) β pulll aΓa.Οββfactor)
(sym (pulll aΓa.Οββfactor) β apβ _β_ refl (sym p) β pulll aΓa.Οββfactor)


We build the congruence in parts.

  open is-congruence
kernel-pair-is-congruence : is-congruence kernel-pair
kernel-pair-is-congruence = cg where
cg : is-congruence _
cg .has-is-monic = kernel-pair-is-monic


For the reflexivity map, we take the unique map $f : A \to A \times_B A$ which is characterised by $p_1 f = p_2 f = \mathrm{id}$; This expresses, diagramatically, that $f(x) = f(x)$.

    cg .has-refl = Kp.universal {pβ' = id} {pβ' = id} refl
cg .refl-pβ = ap (_β Kp.universal refl) aΓa.Οββfactor β Kp.pββuniversal
cg .refl-pβ = ap (_β Kp.universal refl) aΓa.Οββfactor β Kp.pββuniversal


Symmetry is witnessed by the map $(A \times_B A) \to (A \times_B A)$ which swaps the components. This oneβs pretty simple.

    cg .has-sym = Kp.universal {pβ' = Kp.pβ} {pβ' = Kp.pβ} (sym Kp.square)
cg .sym-pβ = ap (_β Kp.universal (sym Kp.square)) aΓa.Οββfactor
β sym (aΓa.Οββfactor β sym Kp.pββuniversal)
cg .sym-pβ = ap (_β Kp.universal (sym Kp.square)) aΓa.Οββfactor
β sym (aΓa.Οββfactor β sym Kp.pββuniversal)

Understanding the transitivity map is left as an exercise to the reader.
    cg .has-trans =
Kp.universal {pβ' = Kp.pβ β rel.pβ} {pβ' = Kp.pβ β rel.pβ} path
where abstract
path : f β Kp.pβ β rel.pβ β‘ f β Kp.pβ β rel.pβ
path =
f β Kp.pβ β rel.pβ                  β‘β¨ extendl (Kp.square β ap (f β_) (sym aΓa.Οββfactor)) β©β‘
f β (aΓa.Οβ β kernel-pair) β rel.pβ β‘β¨ ap (f β_) (sym rel.square) β©β‘
f β (aΓa.Οβ β kernel-pair) β rel.pβ β‘β¨ extendl (ap (f β_) aΓa.Οββfactor β Kp.square) β©β‘
f β Kp.pβ β rel.pβ                  β

cg .trans-factors =
sym (
kernel-pair β Kp.universal _
aΓa.β¨ Kp.pβ β Kp.universal _ , Kp.pβ β Kp.universal _ β©aΓa.
β‘β¨ apβ aΓa.β¨_,_β© (Kp.pββuniversal β apβ _β_ (sym aΓa.Οββfactor) refl)
(Kp.pββuniversal β apβ _β_ (sym aΓa.Οββfactor) refl) β©β‘
aΓa.β¨ (aΓa.Οβ β kernel-pair) β rel.pβ , (aΓa.Οβ β kernel-pair) β rel.pβ β©aΓa.
β)

Kernel-pair : Congruence-on a
Kernel-pair .Congruence-on.domain = _
Kernel-pair .Congruence-on.inclusion = kernel-pair
Kernel-pair .Congruence-on.has-is-cong = kernel-pair-is-congruence


Quotient objectsπ

Let $m : R \hookrightarrow A \times A$ be a congruence on $A$. If $\mathcal{C}$ has a coequaliser $q : A \twoheadrightarrow A/R$ for the composites $R \hookrightarrow A \times A \to A$, then we call $q$ the quotient map, and we call $A/R$ the quotient of $R$.

is-quotient-of : β {A A/R} (R : Congruence-on A) β Hom A A/R β Type _
is-quotient-of R = is-coequaliser C R.relβ R.relβ
where module R = Congruence-on R


Since $q$ coequalises the two projections, by definition, we have $q\pi_1m = q\pi_2m$; Calculating in the category of sets where equality of morphisms is computed pointwise, we can say that βthe images of $R$-related elements under the quotient map $q$ are equalβ. By definition, the quotient for a congruence is a regular epimorphism.

open is-regular-epi

quotient-regular-epi
: β {A A/R} {R : Congruence-on A} {f : Hom A A/R}
β is-quotient-of R f β is-regular-epi C f
quotient-regular-epi quot .r = _
quotient-regular-epi quot .arrβ = _
quotient-regular-epi quot .arrβ = _
quotient-regular-epi quot .has-is-coeq = quot


If $R \hookrightarrow A \times A$ has a quotient $q : A \to A/R$, and $R$ is additionally the pullback of $q$ along itself, then $R$ is called an effective congruence, and $q$ is an effective coequaliser. Since, as mentioned above, the kernel pair of a morphism is βthe congruence of equal imagesβ, this says that an effective quotient identifies exactly those objects related by $R$, and no more.

record is-effective-congruence {A} (R : Congruence-on A) : Type (o β β) where
private module R = Congruence-on R
field
{A/R}          : Ob
quotient       : Hom A A/R
has-quotient   : is-quotient-of R quotient
is-kernel-pair : is-pullback C R.relβ quotient R.relβ quotient


If $f$ is the coequaliser of its kernel pair β that is, it is an effective epimorphism β then it is an effective congruence, and vice-versa.

kernel-pair-is-effective
: β {a b} {f : Hom a b}
β is-quotient-of (Kernel-pair f) f
β is-effective-congruence (Kernel-pair f)
kernel-pair-is-effective {a = a} {b} {f} quot = epi where
open is-effective-congruence hiding (A/R)
module aΓa = Product (fc.products a a)
module pb = Pullback (fc.pullbacks f f)

open is-coequaliser
epi : is-effective-congruence _
epi .is-effective-congruence.A/R = b
epi .quotient = f
epi .has-quotient = quot
epi .is-kernel-pair =
transport
(Ξ» i β is-pullback C (aΓa.Οββfactor {p1 = pb.pβ} {p2 = pb.pβ} (~ i)) f
(aΓa.Οββfactor {p1 = pb.pβ} {p2 = pb.pβ} (~ i)) f)
pb.has-is-pb

kp-effective-congruenceβeffective-epi
: β {a b} {f : Hom a b}
β (eff : is-effective-congruence (Kernel-pair f))
β is-effective-epi C (eff .is-effective-congruence.quotient)
kp-effective-congruenceβeffective-epi {f = f} cong = epi where
module cong = is-effective-congruence cong
open is-effective-epi
epi : is-effective-epi C _
epi .kernel = Kernel-pair _ .Congruence-on.domain
epi .pβ = _
epi .pβ = _
epi .is-kernel-pair = cong.is-kernel-pair
epi .has-is-coeq = cong.has-quotient