Induced metric space of pseudometric spaces

src/foundation/equivalence-classes.lagda.md

@@ -8,11 +8,15 @@ module foundation.equivalence-classes where
 
 ```agda
 open import foundation.conjunction
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.effective-maps-equivalence-relations
+open import foundation.equivalences
 open import foundation.existential-quantification
+open import foundation.function-types
 open import foundation.functoriality-propositional-truncation
 open import foundation.fundamental-theorem-of-identity-types
+open import foundation.homotopies
 open import foundation.inhabited-subtypes
 open import foundation.locally-small-types
 open import foundation.logical-equivalences
@@ -23,13 +27,13 @@ open import foundation.small-types
 open import foundation.subtype-identity-principle
 open import foundation.subtypes
 open import foundation.surjective-maps
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.universal-property-image
 open import foundation.universe-levels
 
 open import foundation-core.cartesian-product-types
 open import foundation-core.embeddings
 open import foundation-core.equivalence-relations
-open import foundation-core.equivalences
 open import foundation-core.functoriality-dependent-pair-types
 open import foundation-core.identity-types
 open import foundation-core.propositions
@@ -315,12 +319,13 @@ module _
       ( λ D → is-in-equivalence-class-Prop R D a)
       ( eq-class-equivalence-class R C H)
 
-  is-torsorial-is-in-equivalence-class :
-    is-torsorial (λ P → is-in-equivalence-class R P a)
-  pr1 is-torsorial-is-in-equivalence-class =
-    center-total-is-in-equivalence-class
-  pr2 is-torsorial-is-in-equivalence-class =
-    contraction-total-is-in-equivalence-class
+  abstract
+    is-torsorial-is-in-equivalence-class :
+      is-torsorial (λ P → is-in-equivalence-class R P a)
+    pr1 is-torsorial-is-in-equivalence-class =
+      center-total-is-in-equivalence-class
+    pr2 is-torsorial-is-in-equivalence-class =
+      contraction-total-is-in-equivalence-class
 
   is-in-equivalence-class-eq-equivalence-class :
     (q : equivalence-class R) → class R a ＝ q →
@@ -338,6 +343,26 @@ module _
         ( is-in-equivalence-class-eq-equivalence-class)
 ```
 
+### Σ-decompositions of types induced by equivalence classes
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  equiv-total-is-in-equivalence-class :
+    Σ A (λ x → Σ (equivalence-class R) (λ X → is-in-equivalence-class R X x)) ≃
+    ( A)
+  equiv-total-is-in-equivalence-class =
+    right-unit-law-Σ-is-contr
+      ( is-torsorial-is-in-equivalence-class R)
+
+  Σ-decomposition-is-in-equivalence-class :
+    Σ (equivalence-class R) (type-subtype ∘ is-in-equivalence-class-Prop R) ≃ A
+  Σ-decomposition-is-in-equivalence-class =
+    equiv-total-is-in-equivalence-class ∘e equiv-left-swap-Σ
+```
+
 ### The map `class : A → equivalence-class R` is an effective quotient map
 
 ```agda

src/foundation/set-quotients.lagda.md

@@ -8,28 +8,37 @@ module foundation.set-quotients where
 
 ```agda
 open import foundation.action-on-identifications-functions
+open import foundation.contractible-maps
+open import foundation.contractible-types
 open import foundation.dependent-pair-types
 open import foundation.effective-maps-equivalence-relations
 open import foundation.embeddings
+open import foundation.equality-dependent-pair-types
 open import foundation.equivalence-classes
 open import foundation.equivalences
+open import foundation.fibers-of-maps
 open import foundation.function-extensionality
+open import foundation.function-types
+open import foundation.functoriality-dependent-pair-types
+open import foundation.homotopies
 open import foundation.identity-types
 open import foundation.inhabited-subtypes
+open import foundation.logical-equivalences
 open import foundation.reflecting-maps-equivalence-relations
 open import foundation.sets
 open import foundation.slice
 open import foundation.surjective-maps
+open import foundation.torsorial-type-families
+open import foundation.transport-along-identifications
+open import foundation.type-arithmetic-dependent-pair-types
 open import foundation.uniqueness-set-quotients
 open import foundation.universal-property-image
 open import foundation.universal-property-set-quotients
 open import foundation.universe-levels
 open import foundation.whiskering-homotopies-composition
 
 open import foundation-core.equivalence-relations
-open import foundation-core.function-types
 open import foundation-core.functoriality-dependent-function-types
-open import foundation-core.homotopies
 open import foundation-core.propositions
 open import foundation-core.small-types
 open import foundation-core.subtypes
@@ -152,7 +161,38 @@ module _
       ( is-surjective-quotient-map)
 ```
 
-### The map `class : A → equivalence-class R` is an effective quotient map
+### Any element is in the class of its quotient
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  is-in-equivalence-class-quotient-map-set-quotient :
+    (x : A) →
+    is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( x)
+  is-in-equivalence-class-quotient-map-set-quotient x =
+    is-in-equivalence-class-eq-equivalence-class
+      ( R)
+      ( x)
+      ( equivalence-class-set-quotient R (quotient-map R x))
+      ( inv
+        ( is-retraction-equivalence-class-set-quotient R (class R x)))
+
+  inhabitant-equivalence-class-quotient-map-set-quotient :
+    (x : A) →
+    type-subtype
+      ( subtype-set-quotient R (quotient-map R x))
+  inhabitant-equivalence-class-quotient-map-set-quotient x =
+    (x , is-in-equivalence-class-quotient-map-set-quotient x)
+```
+
+## Properties
+
+### The map `class : A → set-quotient R` is an effective quotient map
 
 ```agda
 module _
@@ -417,6 +457,127 @@ module _
       B f Uf
 ```
 
+### Any quotient class containing a given element `x` is equal to `quotient-map x`
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  eq-set-quotient-equivalence-class-set-quotient :
+    (X : set-quotient R) {x : A} →
+    is-in-equivalence-class-set-quotient R X x →
+    quotient-map R x ＝ X
+  eq-set-quotient-equivalence-class-set-quotient X {x} H =
+    ( ap
+      ( set-quotient-equivalence-class R)
+      ( eq-class-equivalence-class
+        ( R)
+        ( equivalence-class-set-quotient R X)
+        ( H))) ∙
+    ( is-section-equivalence-class-set-quotient R X)
+```
+
+### Two quotient classes that contain similar elements are equal
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  eq-set-quotient-sim-element-set-quotient :
+    (X : set-quotient R) {x : A} →
+    (Y : set-quotient R) {y : A} →
+    is-in-equivalence-class-set-quotient R X x →
+    is-in-equivalence-class-set-quotient R Y y →
+    sim-equivalence-relation R x y →
+    X ＝ Y
+  eq-set-quotient-sim-element-set-quotient X {x} Y {y} x∈X y∈Y x~y =
+    ( ( inv (eq-set-quotient-equivalence-class-set-quotient R X x∈X)) ∙
+      ( apply-effectiveness-quotient-map' R x~y) ∙
+      ( eq-set-quotient-equivalence-class-set-quotient R Y y∈Y))
+```
+
+### Any element in the quotient class of another is similar to it
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  sim-is-in-equivalence-class-set-quotient :
+    (x y : A) →
+    is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( y) →
+    sim-equivalence-relation R x y
+  sim-is-in-equivalence-class-set-quotient x y y∈X =
+    apply-effectiveness-quotient-map
+      ( R)
+      ( inv
+        ( eq-set-quotient-equivalence-class-set-quotient
+          ( R)
+          ( quotient-map R x)
+          ( y∈X)))
+```
+
+### Σ-decompositions of types induced by set quotients
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  abstract
+    is-torsorial-is-in-equivalence-class-set-quotient :
+      (x : A) →
+      is-contr
+        ( Σ ( set-quotient R)
+            ( λ X → is-in-equivalence-class-set-quotient R X x))
+    is-torsorial-is-in-equivalence-class-set-quotient x =
+      is-contr-equiv'
+        ( Σ (equivalence-class R) (λ X → is-in-equivalence-class R X x))
+        ( equiv-Σ
+          ( λ X → is-in-equivalence-class-set-quotient R X x)
+          ( compute-set-quotient R)
+          ( λ X →
+            equiv-iff-is-prop
+              ( is-prop-is-in-equivalence-class R X x)
+              ( is-prop-is-in-equivalence-class-set-quotient
+                ( R)
+                ( set-quotient-equivalence-class R X)
+                ( x))
+              ( λ x∈X →
+                inv-tr
+                  ( λ Y → is-in-equivalence-class R Y x)
+                  ( is-retraction-equivalence-class-set-quotient R X)
+                  ( x∈X))
+              ( λ x∈X →
+                tr
+                  ( λ Y → is-in-equivalence-class R Y x)
+                  ( is-retraction-equivalence-class-set-quotient R X)
+                  ( x∈X))))
+        ( is-torsorial-is-in-equivalence-class R x)
+
+  equiv-total-is-in-equivalence-class-set-quotient :
+    Σ ( A)
+      ( λ x →
+        Σ ( set-quotient R)
+          ( λ X → is-in-equivalence-class-set-quotient R X x)) ≃
+    ( A)
+  equiv-total-is-in-equivalence-class-set-quotient =
+    right-unit-law-Σ-is-contr
+      ( is-torsorial-is-in-equivalence-class-set-quotient)
+
+  Σ-decomposition-is-in-equivalence-class-set-quotient :
+    Σ ( set-quotient R)
+      ( type-subtype ∘ is-in-equivalence-class-set-quotient-Prop R) ≃
+    ( A)
+  Σ-decomposition-is-in-equivalence-class-set-quotient =
+    equiv-total-is-in-equivalence-class-set-quotient ∘e equiv-left-swap-Σ
+```
+
 ## See also
 
 - [Set coequalizers](foundation.set-coequalizers.md) for an equivalent notion

src/metric-spaces.lagda.md

@@ -55,6 +55,7 @@ open import metric-spaces.complete-metric-spaces public
 open import metric-spaces.continuous-functions-metric-spaces public
 open import metric-spaces.convergent-cauchy-approximations-metric-spaces public
 open import metric-spaces.convergent-sequences-metric-spaces public
+open import metric-spaces.decomposition-metric-spaces-elements-at-bounded-distance-metric-spaces public
 open import metric-spaces.dependent-products-metric-spaces public
 open import metric-spaces.discrete-metric-spaces public
 open import metric-spaces.elements-at-bounded-distance-metric-spaces public
@@ -74,6 +75,7 @@ open import metric-spaces.limits-of-functions-metric-spaces public
 open import metric-spaces.limits-of-sequences-metric-spaces public
 open import metric-spaces.lipschitz-functions-metric-spaces public
 open import metric-spaces.locally-constant-functions-metric-spaces public
+open import metric-spaces.metric-quotients-of-pseudometric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-complete-metric-spaces public
 open import metric-spaces.metric-space-of-cauchy-approximations-metric-spaces public
 open import metric-spaces.metric-space-of-convergent-cauchy-approximations-metric-spaces public