Martin Escardo and Tom de Jong, August 2018, April 2022, September 2023. Quotients. Much of this material is moved from or abstracted from the earlier 2018 module Quotient.Large by Martin Escardo. \begin{code} {-# OPTIONS --safe --without-K #-} module Quotient.Type where open import MLTT.Spartan open import UF.Base hiding (_β_) open import UF.Equiv open import UF.FunExt open import UF.PropTrunc open import UF.Sets open import UF.Sets-Properties open import UF.SubtypeClassifier open import UF.SubtypeClassifier-Properties open import UF.Subsingletons open import UF.Subsingletons-FunExt is-prop-valued is-equiv-relation : {X : π€ Μ } β (X β X β π₯ Μ ) β π€ β π₯ Μ is-prop-valued _β_ = β x y β is-prop (x β y) is-equiv-relation _β_ = is-prop-valued _β_ Γ reflexive _β_ Γ symmetric _β_ Γ transitive _β_ EqRel : {π€ π₯ : Universe} β π€ Μ β π€ β (π₯ βΊ) Μ EqRel {π€} {π₯} X = Ξ£ R κ (X β X β π₯ Μ ) , is-equiv-relation R _β[_]_ : {X : π€ Μ } β X β EqRel X β X β π₯ Μ x β[ _β_ , _ ] y = x β y identifies-related-points : {X : π€ Μ } β EqRel {π€} {π₯} X β {Y : π¦ Μ } β (X β Y) β π€ β π₯ β π¦ Μ identifies-related-points (_β_ , _) f = β {x x'} β x β x' β f x οΌ f x' \end{code} To account for the module Quotient.Large, and, at the same time, usual (small) quotients, we introduce a parametric definion of existence of quotients. For small quotients we take β = id, and for large quotients we take β = (_βΊ) (see below). \begin{code} record general-set-quotients-exist (β : Universe β Universe) : π€Ο where field _/_ : {π€ π₯ : Universe} (X : π€ Μ ) β EqRel {π€} {π₯} X β π€ β β π₯ Μ Ξ·/ : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) β X β X / β Ξ·/-identifies-related-points : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) β identifies-related-points β (Ξ·/ β) /-is-set : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) β is-set (X / β) /-universality : {π€ π₯ : Universe} {X : π€ Μ } (β : EqRel {π€} {π₯} X) {π¦ : Universe} {Y : π¦ Μ } β is-set Y β (f : X β Y) β identifies-related-points β f β β! fΜ κ (X / β β Y) , fΜ β Ξ·/ β βΌ f \end{code} Added 22 August 2022. The induction principle follows from the universal property. \begin{code} /-induction : {X : π€ Μ } (β : EqRel {π€} {π₯} X) {P : X / β β π¦ Μ } β ((x' : X / β) β is-prop (P x')) β ((x : X) β P (Ξ·/ β x)) β (y : X / β) β P y /-induction {X = X} β {P} P-is-prop-valued Ο y = transport P (happly fΜ -section-of-prβ y) (prβ (fΜ y)) where f : X β Ξ£ P f x = (Ξ·/ β x , Ο x) f-identifies-related-points : identifies-related-points β f f-identifies-related-points r = to-subtype-οΌ P-is-prop-valued (Ξ·/-identifies-related-points β r) Ξ£P-is-set : is-set (Ξ£ P) Ξ£P-is-set = subsets-of-sets-are-sets (X / β) P (/-is-set β) (Ξ» {x'} β P-is-prop-valued x') u : β! fΜ κ (X / β β Ξ£ P) , fΜ β Ξ·/ β βΌ f u = /-universality β Ξ£P-is-set f f-identifies-related-points fΜ : X / β β Ξ£ P fΜ = β!-witness u fΜ -after-Ξ·-is-f : fΜ β Ξ·/ β βΌ f fΜ -after-Ξ·-is-f = β!-is-witness u fΜ -section-of-prβ : prβ β fΜ οΌ id fΜ -section-of-prβ = ap prβ (singletons-are-props c (prβ β fΜ , h) (id , Ξ» x β refl)) where c : β! g κ (X / β β X / β) , g β Ξ·/ β βΌ Ξ·/ β c = /-universality β (/-is-set β) (Ξ·/ β) (Ξ·/-identifies-related-points β) h : prβ β fΜ β Ξ·/ β βΌ Ξ·/ β h x = ap prβ (fΜ -after-Ξ·-is-f x) \end{code} Paying attention to universe levels, it is important to note that the quotient of X : π€ by a π₯-valued equivalence relation is assumed to live in π€ β π₯. In particular, the quotient of type in π€ by a π€-valued equivalence relation lives in π€ again. The following are facts about quotients, moved from Quotient.Large as they are of general use. \begin{code} module _ {X : π€ Μ } (β@(_β_ , βp , βr , βs , βt) : EqRel {π€} {π₯} X) where module _ (pt : propositional-truncations-exist) where open PropositionalTruncation pt open import UF.ImageAndSurjection pt Ξ·/-is-surjection : is-surjection (Ξ·/ {π€} {π₯} {X} β) Ξ·/-is-surjection = /-induction β (Ξ» x' β being-in-the-image-is-prop x' (Ξ·/ β)) (Ξ» x β β£ x , refl β£) module _ {A : π¦ Μ } (A-is-set : is-set A) where mediating-map/ : (f : X β A) β identifies-related-points β f β X / β β A mediating-map/ f j = β!-witness (/-universality β A-is-set f j) universality-triangle/ : (f : X β A) (j : identifies-related-points β f) β mediating-map/ f j β Ξ·/ β βΌ f universality-triangle/ f j = β!-is-witness (/-universality β A-is-set f j) at-most-one-mediating-map/ : (g h : X / β β A) β g β Ξ·/ β βΌ h β Ξ·/ β β g βΌ h at-most-one-mediating-map/ g h p x = Ξ³ where f : X β A f = g β Ξ·/ β j : identifies-related-points β f j e = ap g (Ξ·/-identifies-related-points β e) q : mediating-map/ f j οΌ g q = witness-uniqueness (Ξ» fΜ β fΜ β Ξ·/ β βΌ f) (/-universality β A-is-set f j) (mediating-map/ f j) g (universality-triangle/ f j) (Ξ» x β refl) r : mediating-map/ f j οΌ h r = witness-uniqueness (Ξ» fΜ β fΜ β Ξ·/ β βΌ f) (/-universality β A-is-set f j) (mediating-map/ f j) h (universality-triangle/ f j) (Ξ» x β (p x)β»ΒΉ) Ξ³ = g x οΌβ¨ happly (q β»ΒΉ) x β© mediating-map/ f j x οΌβ¨ happly r x β© h x β extension/ : (f : X β X / β) β identifies-related-points β f β (X / β β X / β) extension/ = mediating-map/ (/-is-set β) extension-triangle/ : (f : X β X / β) (i : identifies-related-points β f) β extension/ f i β Ξ·/ β βΌ f extension-triangle/ = universality-triangle/ (/-is-set β) module _ (f : X β X) (p : {x y : X} β x β y β f x β f y) where abstract private Ο : identifies-related-points β (Ξ·/ β β f) Ο e = Ξ·/-identifies-related-points β (p e) extensionβ/ : X / β β X / β extensionβ/ = extension/ (Ξ·/ β β f) Ο naturality/ : extensionβ/ β Ξ·/ β βΌ Ξ·/ β β f naturality/ = universality-triangle/ (/-is-set β) (Ξ·/ β β f) Ο module _ (f : X β X β X) (p : {x y x' y' : X} β x β x' β y β y' β f x y β f x' y') where abstract private Ο : (x : X) β identifies-related-points β (Ξ·/ β β f x) Ο x {y} {y'} e = Ξ·/-identifies-related-points β (p {x} {y} {x} {y'} (βr x) e) p' : (x : X) {y y' : X} β y β y' β f x y β f x y' p' x {x'} {y'} = p {x} {x'} {x} {y'} (βr x) fβ : X β X / β β X / β fβ x = extensionβ/ (f x) (p' x) Ξ΄ : {x x' : X} β x β x' β (y : X) β fβ x (Ξ·/ β y) οΌ fβ x' (Ξ·/ β y) Ξ΄ {x} {x'} e y = fβ x (Ξ·/ β y) οΌβ¨ naturality/ (f x) (p' x) y β© Ξ·/ β (f x y) οΌβ¨ Ξ·/-identifies-related-points β (p e (βr y)) β© Ξ·/ β (f x' y) οΌβ¨ (naturality/ (f x') (p' x') y)β»ΒΉ β© fβ x' (Ξ·/ β y) β Ο : (b : X / β) {x x' : X} β x β x' β fβ x b οΌ fβ x' b Ο b {x} {x'} e = /-induction β (Ξ» y β /-is-set β) (Ξ΄ e) b fβ : X / β β X / β β X / β fβ d e = extension/ (Ξ» x β fβ x e) (Ο e) d extensionβ/ : X / β β X / β β X / β extensionβ/ = fβ abstract naturalityβ/ : (x y : X) β fβ (Ξ·/ β x) (Ξ·/ β y) οΌ Ξ·/ β (f x y) naturalityβ/ x y = fβ (Ξ·/ β x) (Ξ·/ β y) οΌβ¨ extension-triangle/ (Ξ» x β fβ x (Ξ·/ β y)) (Ο (Ξ·/ β y)) x β© fβ x (Ξ·/ β y) οΌβ¨ naturality/ (f x) (p (βr x)) y β© Ξ·/ β (f x y) β \end{code} We extend unary and binary prop-valued relations to the quotient. \begin{code} module extending-relations-to-quotient (fe : Fun-Ext) (pe : Prop-Ext) where module _ {X : π€ Μ } (β@(_β_ , βp , βr , βs , βt) : EqRel {π€} {π₯} X) where module _ (r : X β Ξ© π£) (p : {x y : X} β x β y β r x οΌ r y) where extension-relβ : X / β β Ξ© π£ extension-relβ = mediating-map/ β (Ξ©-is-set fe pe) r p extension-rel-triangleβ : extension-relβ β Ξ·/ β βΌ r extension-rel-triangleβ = universality-triangle/ β (Ξ©-is-set fe pe) r p module _ (r : X β X β Ξ© π£) (p : {x y x' y' : X} β x β x' β y β y' β r x y οΌ r x' y') where abstract private p' : (x : X) {y y' : X} β y β y' β r x y οΌ r x y' p' x {y} {y'} = p (βr x) rβ : X β X / β β Ξ© π£ rβ x = extension-relβ (r x) (p' x) Ξ΄ : {x x' : X} β x β x' β (y : X) β rβ x (Ξ·/ β y) οΌ rβ x' (Ξ·/ β y) Ξ΄ {x} {x'} e y = rβ x (Ξ·/ β y) οΌβ¨ extension-rel-triangleβ (r x) (p (βr x)) y β© r x y οΌβ¨ p e (βr y) β© r x' y οΌβ¨ (extension-rel-triangleβ (r x') (p (βr x')) y) β»ΒΉ β© rβ x' (Ξ·/ β y) β Ο : (q : X / β) {x x' : X} β x β x' β rβ x q οΌ rβ x' q Ο q {x} {x'} e = /-induction β (Ξ» q β Ξ©-is-set fe pe) (Ξ΄ e) q rβ : X / β β X / β β Ξ© π£ rβ = mediating-map/ β (Ξ -is-set fe (Ξ» _ β Ξ©-is-set fe pe)) rβ (Ξ» {x} {x'} e β dfunext fe (Ξ» q β Ο q e)) Ο : (x : X) β rβ (Ξ·/ β x) οΌ rβ x Ο = universality-triangle/ β (Ξ -is-set fe (Ξ» _ β Ξ©-is-set fe pe)) rβ (Ξ» {x} {x'} e β dfunext fe (Ξ» q β Ο q e)) Ο : (x y : X) β rβ (Ξ·/ β x) (Ξ·/ β y) οΌ r x y Ο x y = rβ (Ξ·/ β x) (Ξ·/ β y) οΌβ¨ happly (Ο x) (Ξ·/ β y) β© rβ x (Ξ·/ β y) οΌβ¨ extension-rel-triangleβ (r x) (p' x) y β© r x y β extension-relβ : X / β β X / β β Ξ© π£ extension-relβ = rβ extension-rel-triangleβ : (x y : X) β extension-relβ (Ξ·/ β x) (Ξ·/ β y) οΌ r x y extension-rel-triangleβ = Ο \end{code} For proving properties of an extended binary relation, it is useful to have a binary and ternary versions of quotient induction. \begin{code} module _ (fe : Fun-Ext) {X : π€ Μ } (β : EqRel {π€ } {π₯} X) where /-inductionβ : β {π¦} {P : X / β β X / β β π¦ Μ } β ((x' y' : X / β) β is-prop (P x' y')) β ((x y : X) β P (Ξ·/ β x) (Ξ·/ β y)) β (x' y' : X / β) β P x' y' /-inductionβ p h = /-induction β (Ξ» x' β Ξ -is-prop fe (p x')) (Ξ» x β /-induction β (p (Ξ·/ β x)) (h x)) /-inductionβ : β {π¦} β {P : X / β β X / β β X / β β π¦ Μ } β ((x' y' z' : X / β) β is-prop (P x' y' z')) β ((x y z : X) β P (Ξ·/ β x) (Ξ·/ β y) (Ξ·/ β z)) β (x' y' z' : X / β) β P x' y' z' /-inductionβ p h = /-inductionβ (Ξ» x' y' β Ξ -is-prop fe (p x' y')) (Ξ» x y β /-induction β (p (Ξ·/ β x) (Ξ·/ β y)) (h x y)) quotients-equivalent : (X : π€ Μ ) (R : EqRel {π€} {π₯} X) (R' : EqRel {π€} {π¦} X) β ({x y : X} β x β[ R ] y β x β[ R' ] y) β (X / R) β (X / R') quotients-equivalent X (_β_ , βp , βr , βs , βt ) (_β'_ , βp' , βr' , βs' , βt') Ξ΅ = Ξ³ where β = (_β_ , βp , βr , βs , βt ) β' = (_β'_ , βp' , βr' , βs' , βt') i : {x y : X} β x β y β Ξ·/ β' x οΌ Ξ·/ β' y i e = Ξ·/-identifies-related-points β' (lr-implication Ξ΅ e) iβ»ΒΉ : {x y : X} β x β' y β Ξ·/ β x οΌ Ξ·/ β y iβ»ΒΉ e = Ξ·/-identifies-related-points β (rl-implication Ξ΅ e) f : X / β β X / β' f = mediating-map/ β (/-is-set β') (Ξ·/ β') i fβ»ΒΉ : X / β' β X / β fβ»ΒΉ = mediating-map/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ a : (x : X) β f (fβ»ΒΉ (Ξ·/ β' x)) οΌ Ξ·/ β' x a x = f (fβ»ΒΉ (Ξ·/ β' x)) οΌβ¨ I β© f (Ξ·/ β x) οΌβ¨ II β© Ξ·/ β' x β where I = ap f (universality-triangle/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ x) II = universality-triangle/ β (/-is-set β') (Ξ·/ β') i x Ξ± : f β fβ»ΒΉ βΌ id Ξ± = /-induction β' (Ξ» _ β /-is-set β') a b : (x : X) β fβ»ΒΉ (f (Ξ·/ β x)) οΌ Ξ·/ β x b x = fβ»ΒΉ (f (Ξ·/ β x)) οΌβ¨ I β© fβ»ΒΉ (Ξ·/ β' x) οΌβ¨ II β© Ξ·/ β x β where I = ap fβ»ΒΉ (universality-triangle/ β (/-is-set β') (Ξ·/ β') i x) II = universality-triangle/ β' (/-is-set β) (Ξ·/ β) iβ»ΒΉ x Ξ² : fβ»ΒΉ β f βΌ id Ξ² = /-induction β (Ξ» _ β /-is-set β) b Ξ³ : (X / β) β (X / β') Ξ³ = qinveq f (fβ»ΒΉ , Ξ² , Ξ±) \end{code} We now define the existence of small and large quotients: \begin{code} set-quotients-exist large-set-quotients-exist : π€Ο set-quotients-exist = general-set-quotients-exist (Ξ» π€ β π€) large-set-quotients-exist = general-set-quotients-exist (_βΊ) \end{code} It turns out that quotients, if they exist, are necessarily effective. This is proved the module Quotient.Effective. But we need to include the definition here. \begin{code} are-effective : {β : Universe β Universe} β general-set-quotients-exist β β π€Ο are-effective sq = {π€ π₯ : Universe} {X : π€ Μ } (R : EqRel {π€} {π₯} X) {x y : X} β Ξ·/ R x οΌ Ξ·/ R y β x β[ R ] y where open general-set-quotients-exist sq \end{code}