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π

open Cat.Diagram.Congruence (Sets-finitely-complete {β = β})
private
unit : Set β
unit = el (Lift β β€) Ξ» x y p q i j β lift tt


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) = Ξ£-prop-path!
(happly (R.has-is-monic {c = unit} (Ξ» _ β r) (Ξ» _ β q) (funext Ξ» _ β s β sym p)) _)

open Congruence hiding (quotient)
undo : β {x y} β inc x β‘ inc y β rel x y
undo = 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 .universal {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 .factors = refl

epi .has-quotient .unique {F = F} path =
funext (Coeq-elim-prop (Ξ» x β F .is-tr _ _) (happly path))

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

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

epi .is-kernel-pair .pββuniversal {p = path} =
funext (Ξ» x β ap fst (undo (happly path x) .snd))

epi .is-kernel-pair .pββuniversal {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)) _