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