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 = epi 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

  open Congruence hiding (quotient)
  undo : βˆ€ {x y} β†’ inc x ≑ inc y β†’ rel x y
  undo = equiv→inverse $ effective λ where
    ._∼_ β†’ rel
    .has-is-prop x y β†’ rel-prop x y
    .reflᢜ β†’ rel-refl
    ._βˆ™αΆœ_ β†’ rel-trans
    .symᢜ β†’ rel-sym

  open is-coequaliser
  open is-pullback

  epi : is-effective-congruence R
  epi .A/R            = el (∣ A ∣ / rel) squash
  epi .quotient       = inc

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

  epi .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)
        }

  epi .has-quotient .universal = refl

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

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

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

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

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

  epi .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)) _