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.π₁∘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 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.π₁∘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 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.π₁∘factor ∙ Kp.p₁∘universal
    cg .refl-p₂ = ap (_∘ Kp.universal refl) a×a.π₂∘factor ∙ 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.π₁∘factor
               ∙ sym (a×a.π₂∘factor ∙ sym Kp.p₁∘universal)
    cg .sym-p₂ = ap (_∘ Kp.universal (sym Kp.square)) a×a.π₂∘factor
               ∙ sym (a×a.π₁∘factor ∙ 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.π₂∘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.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.π₁∘factor) refl)
                       (Kp.p₂∘universal ∙ 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 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
    is-kernel-pair : is-pullback C R.rel₁ quotient 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 .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