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.

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 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 =
  g                       β‰‘βŸ¨ introl AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
  (AΓ—A.π₁ ∘ diagonal) ∘ g β‰‘βŸ¨ extendr p βŸ©β‰‘
  (AΓ—A.π₁ ∘ diagonal) ∘ h β‰‘βŸ¨ eliml AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ© βŸ©β‰‘
  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.Ο€β‚βˆ˜βŸ¨βŸ©
  cong .refl-pβ‚‚ = eliml AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ©
  cong .has-sym = id
  cong .sym-p₁ = eliml AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ sym AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ©
  cong .sym-pβ‚‚ = eliml AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ sym AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ©
  cong .has-trans = Pb.p₁
  cong .trans-factors = AΓ—A.uniqueβ‚‚
    (AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ eliml AΓ—A.Ο€β‚βˆ˜βŸ¨βŸ©) (AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ eliml AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ©)
    (assoc _ _ _ βˆ™ Pb.square βˆ™ eliml AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ©)
    (cancell AΓ—A.Ο€β‚‚βˆ˜βŸ¨βŸ©)

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.Ο€β‚βˆ˜βŸ¨βŸ©) βˆ™ apβ‚‚ _∘_ refl (sym p) βˆ™ pulll aΓ—a.Ο€β‚βˆ˜βŸ¨βŸ©)
    (sym (pulll aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ©) βˆ™ apβ‚‚ _∘_ refl (sym p) βˆ™ pulll aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ©)

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.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ Kp.pβ‚βˆ˜universal
    cg .refl-pβ‚‚ = ap (_∘ Kp.universal refl) aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ 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.Ο€β‚βˆ˜βŸ¨βŸ©
               βˆ™ sym (aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ© βˆ™ sym Kp.pβ‚βˆ˜universal)
    cg .sym-pβ‚‚ = ap (_∘ Kp.universal (sym Kp.square)) aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ©
               βˆ™ sym (aΓ—a.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ 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.Ο€β‚‚βˆ˜βŸ¨βŸ©)) βŸ©β‰‘
          f ∘ (aΓ—a.Ο€β‚‚ ∘ kernel-pair) ∘ rel.pβ‚‚ β‰‘βŸ¨ ap (f ∘_) (sym rel.square) βŸ©β‰‘
          f ∘ (aΓ—a.π₁ ∘ kernel-pair) ∘ rel.p₁ β‰‘βŸ¨ extendl (ap (f ∘_) aΓ—a.Ο€β‚βˆ˜βŸ¨βŸ© βˆ™ Kp.square) βŸ©β‰‘
          f ∘ Kp.pβ‚‚ ∘ rel.p₁                  ∎

    cg .trans-factors =
      sym (
        kernel-pair ∘ Kp.universal _
      β‰‘βŸ¨ aΓ—a.⟨⟩∘ _ βŸ©β‰‘
        aΓ—a.⟨ Kp.p₁ ∘ Kp.universal _ , Kp.pβ‚‚ ∘ Kp.universal _ ⟩aΓ—a.
      β‰‘βŸ¨ apβ‚‚ aΓ—a.⟨_,_⟩ (Kp.pβ‚βˆ˜universal βˆ™ apβ‚‚ _∘_ (sym aΓ—a.Ο€β‚βˆ˜βŸ¨βŸ©) refl)
                       (Kp.pβ‚‚βˆ˜universal βˆ™ apβ‚‚ _∘_ (sym aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ©) 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
    has-kernel-pair : is-kernel-pair C R.rel₁ 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 .has-kernel-pair =
    transport
      (Ξ» i β†’ is-pullback C (aΓ—a.Ο€β‚βˆ˜βŸ¨βŸ© {p1 = pb.p₁} {p2 = pb.pβ‚‚} (~ i)) f
                           (aΓ—a.Ο€β‚‚βˆ˜βŸ¨βŸ© {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 .has-kernel-pair = cong.has-kernel-pair
  epi .has-is-coeq = cong.has-quotient