open import Cat.Instances.Sets.Complete
open import Cat.Diagram.Coequaliser
open import Cat.Diagram.Pullback
open import Cat.Prelude

import Cat.Diagram.Congruence

module Cat.Instances.Sets.Congruences {β„“} where

Sets has effective quotientsπŸ”—

The hardest part of proving that Sets has effective quotients is the proof that quotients are effective, which we can entirely reuse here. The code here mostly mediates between the notion of β€œcongruence on a Set” and β€œequivalence relation on a Set.” Thus, it is presented without comment.

Sets-effective-congruences : βˆ€ {A} (R : Congruence-on A) β†’ is-effective-congruence R
Sets-effective-congruences {A = A} R = eff where
  module R = Congruence-on R
  open is-effective-congruence

  rel : ∣ A ∣ β†’ ∣ A ∣ β†’ _
  rel x y = fibre R.inclusion (x , y)

  rel-refl : βˆ€ {x} β†’ rel x x
  rel-refl {x} =
    R.has-refl x , Ξ£-pathp (happly R.refl-p₁ _) (happly R.refl-pβ‚‚ _)

  rel-sym : βˆ€ {x y} β†’ rel x y β†’ rel y x
  rel-sym (r , p) = R.has-sym r ,
    Ξ£-pathp (happly R.sym-p₁ _ βˆ™ ap snd p) (happly R.sym-pβ‚‚ _ βˆ™ ap fst p)

  rel-trans : βˆ€ {x y z} β†’ rel x y β†’ rel y z β†’ rel x z
  rel-trans (r , p) (s , q) = R.has-trans (s , r , ap fst q βˆ™ sym (ap snd p)) ,
    Ξ£-pathp (ap fst (happly (sym R.trans-factors) _) βˆ™ ap fst p)
            (ap snd (happly (sym R.trans-factors) _) βˆ™ ap snd q)

  rel-prop : βˆ€ x y β†’ is-prop (rel x y)
  rel-prop _ _ (r , s) (q , p) =
    Ξ£-path
      (happly (R.has-is-monic {c = unit} m1 m2 (funext Ξ» _ β†’ s βˆ™ sym p)) _)
      (Γ—-is-hlevel 2 (A .is-tr) (A .is-tr) _ _ _ _)
    where
      m1 m2 : Precategory.Hom (Sets β„“) unit R.domain
      m1 _ = r
      m2 _ = q

  undo : βˆ€ {x y} β†’ inc x ≑ inc y β†’ rel x y
  undo = equiv→inverse (effective rel-prop rel-refl rel-trans rel-sym)

  open is-coequaliser
  open is-pullback

  eff : is-effective-congruence R
  eff .A/R            = ∣ A ∣ / rel , squash
  eff .quotient       = inc

  eff .has-quotient .coequal = funext Ξ» { x β†’ quot (x , refl) }

  eff .has-quotient .coequalise {F = F} {eβ€² = eβ€²} path =
    Quot-elim (Ξ» _ β†’ F .is-tr) eβ€²
      Ξ» { x y (r , q) β†’ ap eβ€² (ap fst (sym q))
                     Β·Β· happly path r
                     Β·Β· ap eβ€² (ap snd q)
        }

  eff .has-quotient .universal = refl

  eff .has-quotient .unique {F = F} path =
    funext (Coeq-elim-prop (Ξ» x β†’ F .is-tr _ _) (sym βŠ™ happly path))

  eff .is-kernel-pair .square = funext Ξ» { x β†’ quot (x , refl) }

  eff .is-kernel-pair .limiting path x = undo (happly path x) .fst

  eff .is-kernel-pair .pβ‚βˆ˜limiting {p = path} =
    funext (Ξ» x β†’ ap fst (undo (happly path x) .snd))

  eff .is-kernel-pair .pβ‚‚βˆ˜limiting {p = path} =
    funext (Ξ» x β†’ ap snd (undo (happly path x) .snd))

  eff .is-kernel-pair .unique {p = p} q r = funext Ξ» x β†’
    let p = sym ( undo (happly p x) .snd
                βˆ™ Ξ£-pathp (happly (sym q) _) (happly (sym r) _))
     in happly (R.has-is-monic {c = unit} _ _ (funext Ξ» _ β†’ p)) _