Exponents of set quotients
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Julian KG, fernabnor and louismntnu.
Created on 2023-02-05.
Last modified on 2023-09-12.
{-# OPTIONS --lossy-unification #-} module foundation.exponents-set-quotients where
Imports
open import foundation.binary-relations open import foundation.dependent-pair-types open import foundation.function-extensionality open import foundation.functoriality-set-quotients open import foundation.reflecting-maps-equivalence-relations open import foundation.set-quotients open import foundation.sets open import foundation.universal-property-set-quotients open import foundation.universe-levels open import foundation-core.contractible-types open import foundation-core.embeddings open import foundation-core.equivalence-relations open import foundation-core.function-types open import foundation-core.homotopies open import foundation-core.identity-types open import foundation-core.propositions open import foundation-core.whiskering-homotopies
Idea
Given a type A
equipped with an equivalence relation R
and a type X
, the
set quotient
(X → A) / ~
where f ~ g := (x : A) → R (f x) (g x)
, embeds into the type X → A/R
. This
embedding for every X
, A
, and R
if and only if the axiom of choice holds.
Consequently, we get embeddings
((hom-Equivalence-Relation R S) / ~) ↪ ((A/R) → (B/S))
for any two equivalence relations R
on A
and S
on B
.
Definitions
The canonical equivalence relation on X → A
module _ {l1 l2 l3 : Level} (X : UU l1) {A : UU l2} (R : Equivalence-Relation l3 A) where rel-function-type : Relation-Prop (l1 ⊔ l3) (X → A) rel-function-type f g = Π-Prop X (λ x → prop-Equivalence-Relation R (f x) (g x)) sim-function-type : (f g : X → A) → UU (l1 ⊔ l3) sim-function-type = type-Relation-Prop rel-function-type refl-sim-function-type : is-reflexive sim-function-type refl-sim-function-type f x = refl-Equivalence-Relation R (f x) symmetric-sim-function-type : is-symmetric sim-function-type symmetric-sim-function-type f g r x = symmetric-Equivalence-Relation R (f x) (g x) (r x) transitive-sim-function-type : is-transitive sim-function-type transitive-sim-function-type f g h r s x = transitive-Equivalence-Relation R (f x) (g x) (h x) (r x) (s x) eq-rel-function-type : Equivalence-Relation (l1 ⊔ l3) (X → A) pr1 eq-rel-function-type = rel-function-type pr1 (pr2 eq-rel-function-type) = refl-sim-function-type pr1 (pr2 (pr2 eq-rel-function-type)) = symmetric-sim-function-type pr2 (pr2 (pr2 eq-rel-function-type)) = transitive-sim-function-type map-exponent-reflecting-map-Equivalence-Relation : {l4 : Level} {B : UU l4} → reflecting-map-Equivalence-Relation R B → (X → A) → (X → B) map-exponent-reflecting-map-Equivalence-Relation q = postcomp X (map-reflecting-map-Equivalence-Relation R q) reflects-exponent-reflecting-map-Equivalence-Relation : {l4 : Level} {B : UU l4} (q : reflecting-map-Equivalence-Relation R B) → reflects-Equivalence-Relation eq-rel-function-type ( map-exponent-reflecting-map-Equivalence-Relation q) reflects-exponent-reflecting-map-Equivalence-Relation q {f} {g} H = eq-htpy (λ x → reflects-map-reflecting-map-Equivalence-Relation R q (H x)) exponent-reflecting-map-Equivalence-Relation : {l4 : Level} {B : UU l4} → reflecting-map-Equivalence-Relation R B → reflecting-map-Equivalence-Relation eq-rel-function-type (X → B) pr1 (exponent-reflecting-map-Equivalence-Relation q) = map-exponent-reflecting-map-Equivalence-Relation q pr2 (exponent-reflecting-map-Equivalence-Relation q) = reflects-exponent-reflecting-map-Equivalence-Relation q module _ {l4 l5 : Level} (Q : Set l4) (q : reflecting-map-Equivalence-Relation eq-rel-function-type (type-Set Q)) (Uq : {l : Level} → is-set-quotient l eq-rel-function-type Q q) (QR : Set l5) (qR : reflecting-map-Equivalence-Relation R (type-Set QR)) (UqR : {l : Level} → is-set-quotient l R QR qR) where unique-inclusion-is-set-quotient-eq-rel-function-type : is-contr ( Σ ( type-Set Q → (X → type-Set QR)) ( λ h → ( h ∘ map-reflecting-map-Equivalence-Relation eq-rel-function-type q) ~ ( map-exponent-reflecting-map-Equivalence-Relation qR))) unique-inclusion-is-set-quotient-eq-rel-function-type = universal-property-set-quotient-is-set-quotient ( eq-rel-function-type) ( Q) ( q) ( Uq) ( function-Set X QR) ( exponent-reflecting-map-Equivalence-Relation qR) map-inclusion-is-set-quotient-eq-rel-function-type : type-Set Q → (X → type-Set QR) map-inclusion-is-set-quotient-eq-rel-function-type = map-universal-property-set-quotient-is-set-quotient ( eq-rel-function-type) ( Q) ( q) ( Uq) ( function-Set X QR) ( exponent-reflecting-map-Equivalence-Relation qR) triangle-inclusion-is-set-quotient-eq-rel-function-type : ( ( map-inclusion-is-set-quotient-eq-rel-function-type) ∘ ( map-reflecting-map-Equivalence-Relation eq-rel-function-type q)) ~ ( map-exponent-reflecting-map-Equivalence-Relation qR) triangle-inclusion-is-set-quotient-eq-rel-function-type = triangle-universal-property-set-quotient-is-set-quotient ( eq-rel-function-type) ( Q) ( q) ( Uq) ( function-Set X QR) ( exponent-reflecting-map-Equivalence-Relation qR)
An equivalence relation on relation preserving maps
module _ {l1 l2 l3 l4 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {B : UU l3} (S : Equivalence-Relation l4 B) where rel-hom-Equivalence-Relation : Relation-Prop (l1 ⊔ l4) (hom-Equivalence-Relation R S) rel-hom-Equivalence-Relation f g = rel-function-type A S ( map-hom-Equivalence-Relation R S f) ( map-hom-Equivalence-Relation R S g) sim-hom-Equivalence-Relation : (f g : hom-Equivalence-Relation R S) → UU (l1 ⊔ l4) sim-hom-Equivalence-Relation f g = sim-function-type A S ( map-hom-Equivalence-Relation R S f) ( map-hom-Equivalence-Relation R S g) refl-sim-hom-Equivalence-Relation : is-reflexive sim-hom-Equivalence-Relation refl-sim-hom-Equivalence-Relation f = refl-sim-function-type A S (map-hom-Equivalence-Relation R S f) symmetric-sim-hom-Equivalence-Relation : is-symmetric sim-hom-Equivalence-Relation symmetric-sim-hom-Equivalence-Relation f g = symmetric-sim-function-type A S ( map-hom-Equivalence-Relation R S f) ( map-hom-Equivalence-Relation R S g) transitive-sim-hom-Equivalence-Relation : is-transitive sim-hom-Equivalence-Relation transitive-sim-hom-Equivalence-Relation f g h = transitive-sim-function-type A S ( map-hom-Equivalence-Relation R S f) ( map-hom-Equivalence-Relation R S g) ( map-hom-Equivalence-Relation R S h) eq-rel-hom-Equivalence-Relation : Equivalence-Relation (l1 ⊔ l4) (hom-Equivalence-Relation R S) pr1 eq-rel-hom-Equivalence-Relation = rel-hom-Equivalence-Relation pr1 (pr2 eq-rel-hom-Equivalence-Relation) = refl-sim-hom-Equivalence-Relation pr1 (pr2 (pr2 eq-rel-hom-Equivalence-Relation)) = symmetric-sim-hom-Equivalence-Relation pr2 (pr2 (pr2 eq-rel-hom-Equivalence-Relation)) = transitive-sim-hom-Equivalence-Relation
The universal reflecting map from hom-Equivalence-Relation R S
to A/R → B/S
First variant using only the universal property of set quotients
module _ {l1 l2 l3 l4 l5 l6 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) (QR : Set l3) (qR : reflecting-map-Equivalence-Relation R (type-Set QR)) (UqR : {l : Level} → is-set-quotient l R QR qR) {B : UU l4} (S : Equivalence-Relation l5 B) (QS : Set l6) (qS : reflecting-map-Equivalence-Relation S (type-Set QS)) (UqS : {l : Level} → is-set-quotient l S QS qS) where universal-map-is-set-quotient-hom-Equivalence-Relation : hom-Equivalence-Relation R S → type-hom-Set QR QS universal-map-is-set-quotient-hom-Equivalence-Relation = map-is-set-quotient R QR qR S QS qS UqR UqS reflects-universal-map-is-set-quotient-hom-Equivalence-Relation : reflects-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( universal-map-is-set-quotient-hom-Equivalence-Relation) reflects-universal-map-is-set-quotient-hom-Equivalence-Relation {f} {g} s = eq-htpy ( ind-is-set-quotient R QR qR UqR ( λ x → Id-Prop QS ( map-is-set-quotient R QR qR S QS qS UqR UqS f x) ( map-is-set-quotient R QR qR S QS qS UqR UqS g x)) ( λ a → coherence-square-map-is-set-quotient R QR qR S QS qS UqR UqS f a ∙ ( ( apply-effectiveness-is-set-quotient' S QS qS UqS (s a)) ∙ ( inv ( coherence-square-map-is-set-quotient R QR qR S QS qS UqR UqS g a))))) universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation : reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( type-hom-Set QR QS) pr1 universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation = universal-map-is-set-quotient-hom-Equivalence-Relation pr2 universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation = reflects-universal-map-is-set-quotient-hom-Equivalence-Relation
Second variant using the designated set quotients
module _ {l1 l2 l3 l4 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {B : UU l3} (S : Equivalence-Relation l4 B) where universal-reflecting-map-set-quotient-hom-Equivalence-Relation : reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( set-quotient R → set-quotient S) universal-reflecting-map-set-quotient-hom-Equivalence-Relation = universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation ( R) ( quotient-Set R) ( reflecting-map-quotient-map R) ( λ {l} → is-set-quotient-set-quotient R {l}) ( S) ( quotient-Set S) ( reflecting-map-quotient-map S) ( λ {l} → is-set-quotient-set-quotient S {l}) universal-map-set-quotient-hom-Equivalence-Relation : hom-Equivalence-Relation R S → set-quotient R → set-quotient S universal-map-set-quotient-hom-Equivalence-Relation = map-reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( universal-reflecting-map-set-quotient-hom-Equivalence-Relation) reflects-universal-map-set-quotient-hom-Equivalence-Relation : reflects-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( universal-map-set-quotient-hom-Equivalence-Relation) reflects-universal-map-set-quotient-hom-Equivalence-Relation = reflects-map-reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( universal-reflecting-map-set-quotient-hom-Equivalence-Relation)
Properties
The inclusion of the quotient (X → A)/~
into X → A/R
is an embedding
module _ {l1 l2 l3 l4 l5 : Level} (X : UU l1) {A : UU l2} (R : Equivalence-Relation l3 A) (Q : Set l4) (q : reflecting-map-Equivalence-Relation ( eq-rel-function-type X R) ( type-Set Q)) (Uq : {l : Level} → is-set-quotient l (eq-rel-function-type X R) Q q) (QR : Set l5) (qR : reflecting-map-Equivalence-Relation R (type-Set QR)) (UqR : {l : Level} → is-set-quotient l R QR qR) where is-emb-inclusion-is-set-quotient-eq-rel-function-type : is-emb ( map-inclusion-is-set-quotient-eq-rel-function-type X R Q q Uq QR qR UqR) is-emb-inclusion-is-set-quotient-eq-rel-function-type = is-emb-map-universal-property-set-quotient-is-set-quotient ( eq-rel-function-type X R) ( Q) ( q) ( Uq) ( function-Set X QR) ( exponent-reflecting-map-Equivalence-Relation X R qR) ( λ g h p x → apply-effectiveness-is-set-quotient R QR qR UqR (htpy-eq p x))
The extension of the universal map from hom-Equivalence-Relation R S
to A/R → B/S
to the quotient is an embedding
First variant using only the universal property of the set quotient
module _ {l1 l2 l3 l4 l5 l6 l7 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) (QR : Set l3) (qR : reflecting-map-Equivalence-Relation R (type-Set QR)) (UR : {l : Level} → is-set-quotient l R QR qR) {B : UU l4} (S : Equivalence-Relation l5 B) (QS : Set l6) (qS : reflecting-map-Equivalence-Relation S (type-Set QS)) (US : {l : Level} → is-set-quotient l S QS qS) (QH : Set l7) (qH : reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( type-Set QH)) (UH : {l : Level} → is-set-quotient l (eq-rel-hom-Equivalence-Relation R S) QH qH) where unique-inclusion-is-set-quotient-hom-Equivalence-Relation : is-contr ( Σ ( type-hom-Set QH (hom-Set QR QS)) ( λ μ → ( μ ∘ map-reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( qH)) ~ ( universal-map-is-set-quotient-hom-Equivalence-Relation R QR qR UR S QS qS US))) unique-inclusion-is-set-quotient-hom-Equivalence-Relation = universal-property-set-quotient-is-set-quotient ( eq-rel-hom-Equivalence-Relation R S) ( QH) ( qH) ( UH) ( hom-Set QR QS) ( universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation R QR qR UR S QS qS US) inclusion-is-set-quotient-hom-Equivalence-Relation : type-hom-Set QH (hom-Set QR QS) inclusion-is-set-quotient-hom-Equivalence-Relation = pr1 (center (unique-inclusion-is-set-quotient-hom-Equivalence-Relation)) triangle-inclusion-is-set-quotient-hom-Equivalence-Relation : ( inclusion-is-set-quotient-hom-Equivalence-Relation ∘ map-reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( qH)) ~ ( universal-map-is-set-quotient-hom-Equivalence-Relation R QR qR UR S QS qS US) triangle-inclusion-is-set-quotient-hom-Equivalence-Relation = pr2 (center (unique-inclusion-is-set-quotient-hom-Equivalence-Relation)) is-emb-inclusion-is-set-quotient-hom-Equivalence-Relation : is-emb inclusion-is-set-quotient-hom-Equivalence-Relation is-emb-inclusion-is-set-quotient-hom-Equivalence-Relation = is-emb-map-universal-property-set-quotient-is-set-quotient ( eq-rel-hom-Equivalence-Relation R S) ( QH) ( qH) ( UH) ( hom-Set QR QS) ( universal-reflecting-map-is-set-quotient-hom-Equivalence-Relation R QR qR UR S QS qS US) ( λ g h p a → apply-effectiveness-is-set-quotient S QS qS US ( ( inv-htpy ( coherence-square-map-is-set-quotient R QR qR S QS qS UR US g) ∙h ( ( htpy-eq p ·r map-reflecting-map-Equivalence-Relation R qR) ∙h ( coherence-square-map-is-set-quotient R QR qR S QS qS UR US h))) ( a))) emb-inclusion-is-set-quotient-hom-Equivalence-Relation : type-Set QH ↪ type-hom-Set QR QS pr1 emb-inclusion-is-set-quotient-hom-Equivalence-Relation = inclusion-is-set-quotient-hom-Equivalence-Relation pr2 emb-inclusion-is-set-quotient-hom-Equivalence-Relation = is-emb-inclusion-is-set-quotient-hom-Equivalence-Relation
Second variant using the official set quotients
module _ {l1 l2 l3 l4 : Level} {A : UU l1} (R : Equivalence-Relation l2 A) {B : UU l3} (S : Equivalence-Relation l4 B) where quotient-hom-Equivalence-Relation-Set : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4) quotient-hom-Equivalence-Relation-Set = quotient-Set (eq-rel-hom-Equivalence-Relation R S) set-quotient-hom-Equivalence-Relation : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) set-quotient-hom-Equivalence-Relation = type-Set quotient-hom-Equivalence-Relation-Set is-set-set-quotient-hom-Equivalence-Relation : is-set set-quotient-hom-Equivalence-Relation is-set-set-quotient-hom-Equivalence-Relation = is-set-type-Set quotient-hom-Equivalence-Relation-Set reflecting-map-quotient-map-hom-Equivalence-Relation : reflecting-map-Equivalence-Relation ( eq-rel-hom-Equivalence-Relation R S) ( set-quotient-hom-Equivalence-Relation) reflecting-map-quotient-map-hom-Equivalence-Relation = reflecting-map-quotient-map (eq-rel-hom-Equivalence-Relation R S) quotient-map-hom-Equivalence-Relation : hom-Equivalence-Relation R S → set-quotient-hom-Equivalence-Relation quotient-map-hom-Equivalence-Relation = quotient-map (eq-rel-hom-Equivalence-Relation R S) is-set-quotient-set-quotient-hom-Equivalence-Relation : {l : Level} → is-set-quotient l ( eq-rel-hom-Equivalence-Relation R S) ( quotient-hom-Equivalence-Relation-Set) ( reflecting-map-quotient-map-hom-Equivalence-Relation) is-set-quotient-set-quotient-hom-Equivalence-Relation = is-set-quotient-set-quotient (eq-rel-hom-Equivalence-Relation R S) unique-inclusion-set-quotient-hom-Equivalence-Relation : is-contr ( Σ ( set-quotient-hom-Equivalence-Relation → set-quotient R → set-quotient S) ( λ μ → ( μ ∘ quotient-map (eq-rel-hom-Equivalence-Relation R S)) ~ ( universal-map-set-quotient-hom-Equivalence-Relation R S))) unique-inclusion-set-quotient-hom-Equivalence-Relation = universal-property-set-quotient-is-set-quotient ( eq-rel-hom-Equivalence-Relation R S) ( quotient-hom-Equivalence-Relation-Set) ( reflecting-map-quotient-map-hom-Equivalence-Relation) ( is-set-quotient-set-quotient-hom-Equivalence-Relation) ( hom-Set (quotient-Set R) (quotient-Set S)) ( universal-reflecting-map-set-quotient-hom-Equivalence-Relation R S) inclusion-set-quotient-hom-Equivalence-Relation : set-quotient (eq-rel-hom-Equivalence-Relation R S) → set-quotient R → set-quotient S inclusion-set-quotient-hom-Equivalence-Relation = pr1 (center (unique-inclusion-set-quotient-hom-Equivalence-Relation)) triangle-inclusion-set-quotient-hom-Equivalence-Relation : ( inclusion-set-quotient-hom-Equivalence-Relation ∘ quotient-map (eq-rel-hom-Equivalence-Relation R S)) ~ ( universal-map-set-quotient-hom-Equivalence-Relation R S) triangle-inclusion-set-quotient-hom-Equivalence-Relation = pr2 (center (unique-inclusion-set-quotient-hom-Equivalence-Relation)) is-emb-inclusion-set-quotient-hom-Equivalence-Relation : is-emb inclusion-set-quotient-hom-Equivalence-Relation is-emb-inclusion-set-quotient-hom-Equivalence-Relation = is-emb-map-universal-property-set-quotient-is-set-quotient ( eq-rel-hom-Equivalence-Relation R S) ( quotient-hom-Equivalence-Relation-Set) ( reflecting-map-quotient-map-hom-Equivalence-Relation) ( is-set-quotient-set-quotient-hom-Equivalence-Relation) ( hom-Set (quotient-Set R) (quotient-Set S)) ( universal-reflecting-map-set-quotient-hom-Equivalence-Relation R S) ( λ g h p a → apply-effectiveness-quotient-map S ( ( inv-htpy ( coherence-square-map-set-quotient R S g) ∙h ( ( htpy-eq p ·r quotient-map R) ∙h ( coherence-square-map-set-quotient R S h))) ( a))) emb-inclusion-set-quotient-hom-Equivalence-Relation : set-quotient (eq-rel-hom-Equivalence-Relation R S) ↪ ( set-quotient R → set-quotient S) pr1 emb-inclusion-set-quotient-hom-Equivalence-Relation = inclusion-set-quotient-hom-Equivalence-Relation pr2 emb-inclusion-set-quotient-hom-Equivalence-Relation = is-emb-inclusion-set-quotient-hom-Equivalence-Relation
Recent changes
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-06-25. Fredrik Bakke, louismntnu, fernabnor, Egbert Rijke and Julian KG. Posets are categories, and refactor binary relations (#665).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).