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Γ—Aβ†’PropR : A \times A \to \prop satisfying reflexivity (R(x,x)R(x,x) for all xx), transitivity (R(x,y)∧R(y,z)β†’R(x,z)R(x,y) \land R(y,z) \to R(x,z)), and symmetry (R(x,y)β†’R(y,x)R(x,y) \to R(y,x)). Knowing that Prop\prop classifies embeddings, we can equivalently talk about an equivalence relation RR as being just some set, equipped with a mono m:Rβ†ͺAΓ—Am : R \mono A \times A.

We must now identify what properties of the mono mm identify RR as being the total space of an equivalence relation. Let us work in the category of sets for the moment. Suppose RR is a relation on AA, and m:dβ†ͺAΓ—Am : d \mono A \times A is the monomorphism representing it. Let’s identify the properties of mm which correspond to the properties of RR 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. RR is reflexive if, and only if, the morphisms p1,p2:d→Ap_1, p_2 : d \to A have a common left inverse r:A→dr : 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→ds : d \to d which swaps p1p_1 and p2p_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\sets has finite limits, we have an object of β€œcomposable pairs” of dd, namely the pullback under the cospan Rβ†’p1X←p2RR \xto{p_1} X \xot{p_2} R.

Transitivity, then, means that the two projection maps p1q1,p2q2:(dΓ—Ad)⇉(AΓ—A)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 RR, somehow, i.e.Β we have a t:(dΓ—Ad)β†’dt : (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β†ͺAΓ—Am : R \mono A \times A which identify RR as an equivalence relation on the object AA. 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 Ξ”:Aβ†’(AΓ—A)\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=Ο€1βˆ˜Ξ”\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β†’bf : a \to b, its kernel pair, i.e.Β the pullback of aβ†’fb←faa \xto{f} b \xot{f} a. Calculating in Sets\sets, this is the equivalence relation generated by f(x)=f(y)f(x) = f(y) β€” it is the subobject of aΓ—aa \times a consisting of those β€œvalues which ff 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→A×BAf : A \to A \times_B A which is characterised by p1f=p2f=idp_1 f = p_2 f = \mathrm{id}; This expresses, diagramatically, that f(x)=f(x)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Γ—BA)β†’(AΓ—BA)(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β†ͺAΓ—Am : R \mono A \times A be a congruence on AA. If C\ca{C} has a coequaliser q:Aβ† A/Rq : A \epi A/R for the composites Rβ†ͺAΓ—Aβ†’AR \mono A \times A \to A, then we call qq the quotient map, and we call A/RA/R the quotient of RR.

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 qq coequalises the two projections, by definition, we have qΟ€1m=qΟ€2mq\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 RR-related elements under the quotient map qq 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β†ͺAΓ—AR \hookrightarrow A \times A has a quotient q:Aβ†’A/Rq : A \to A/R, and RR is additionally the pullback of qq along itself, then RR is called an effective congruence, and qq 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 RR, 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 ff 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