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×APropR : 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:RA×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:dA×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 = 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. RR is reflexive if, and only if, the morphisms p1,p2:dAp_1, p_2 : d \to A have a common left inverse r:Adr : 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:dds : 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 Rp1Xp2RR \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) \rightrightarrows (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:RA×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:abf : a \to b, its kernel pair, i.e. the pullback of afbfaa \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:AA×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:RA×Am : R \mono A \times A be a congruence on AA. If C\ca{C} has a coequaliser q:AA/Rq : A \epi A/R for the composites RA×AAR \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 RA×AR \hookrightarrow A \times A has a quotient q:AA/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