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) \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 \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