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 \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 $\prop$ classifies embeddings, we can equivalently talk about an equivalence relation $R$ as being just some set, equipped with a mono $m : R \mono 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 \mono 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 = equiv→inverse (subtype-classifier .snd) (λ x → R x , rp x) .fst

m : domain ↣ (∣ A ∣ × ∣ A ∣)
m = equiv→inverse (subtype-classifier .snd) (λ 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 $\sets$ has finite limits, we have an object of “composable pairs” of $d$, namely the pullback under the cospan $R \xto{p_1} X \xot{p_2} R$. Transitivity, then, means that the two projection maps $p_1q_1, p_2q_2 : (d \times_A d) \tto (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 \mono 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.

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:

  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

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 $\id{id} = \pi_1 \circ \Delta$.

diagonal-is-monic : ∀ {A} → is-monic (diagonal {A})
diagonal-is-monic {A} g h p =
g                       ≡⟨ introl A×A.π₁∘factor ⟩≡
(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 \xto{f} b \xot{f} a$. Calculating in $\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.limiting {p₁' = id} {p₂' = id} refl
cg .refl-p₁ = ap (_∘ Kp.limiting refl) a×a.π₁∘factor ∙ Kp.p₁∘limiting
cg .refl-p₂ = ap (_∘ Kp.limiting refl) a×a.π₂∘factor ∙ Kp.p₂∘limiting


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.limiting {p₁' = Kp.p₂} {p₂' = Kp.p₁} (sym Kp.square)
cg .sym-p₁ = ap (_∘ Kp.limiting (sym Kp.square)) a×a.π₁∘factor
∙ sym (a×a.π₂∘factor ∙ sym Kp.p₁∘limiting)
cg .sym-p₂ = ap (_∘ Kp.limiting (sym Kp.square)) a×a.π₂∘factor
∙ sym (a×a.π₁∘factor ∙ sym Kp.p₂∘limiting)

Understanding the transitivity map is left as an exercise to the reader.
    cg .has-trans =
Kp.limiting {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.limiting _
≡⟨ a×a.⟨⟩∘ _ ⟩≡
a×a.⟨ Kp.p₁ ∘ Kp.limiting _ , Kp.p₂ ∘ Kp.limiting _ ⟩a×a.
≡⟨ ap₂ a×a.⟨_,_⟩ (Kp.p₁∘limiting ∙ ap₂ _∘_ (sym a×a.π₁∘factor) refl)
(Kp.p₂∘limiting ∙ 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 \mono A \times A$ be a congruence on $A$. If $\ca{C}$ has a coequaliser $q : A \epi A/R$ for the composites $R \mono 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 = eff 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
eff : is-effective-congruence _
eff .is-effective-congruence.A/R = b
eff .quotient = f
eff .has-quotient = quot
eff .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