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 hiding (Kernel-pair)

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 satisfying reflexivity ( for all transitivity ( and symmetry ( Knowing that classifies embeddings, we can equivalently talk about an equivalence relation as being just some set, equipped with a monomorphism

We must now identify what properties of the mono identify as being the total space of an equivalence relation. Let us work in the category of sets for the moment. Suppose is a relation on and is the monomorphism representing it. Letβs identify the properties of which correspond to the properties of 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. is reflexive if, and only if, the morphisms have a common left inverse

    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 which swaps and

    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 has finite limits, we have an object of βcomposable pairsβ of namely the pullback under the cospan

Transitivity, then, means that the two projection maps β which take a βcomposable pairβ to the βfirst mapβs sourceβ and βsecond mapβs targetβ, respectively β factor through somehow, i.e.Β we have a 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 which identify as an equivalence relation on the object 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 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

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 its kernel pair, i.e.Β the pullback of Calculating in this is the equivalence relation generated by β it is the subobject of consisting of those βvalues which 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 which is characterised by This expresses, diagrammatically, that

    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 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 be a congruence on If has a coequaliser for the composites then we call the quotient map, and we call the quotient of

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 coequalises the two projections, by definition, we have Calculating in the category of sets where equality of morphisms is computed pointwise, we can say that βthe images of elements under the quotient map 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 has a quotient and is additionally the pullback of along itself, then is called an effective congruence, and 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 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 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