Bounded distance decompositions of metric spaces (UniMath#1482)

Given a metric space `A`, this PR introduces the bounded distance
decomposition of a metric space `A`: the metric space
```agda
  bounded-distance-decompsition-Metric-Space :
    Metric-Space (l1 ⊔ l2) (l1 ⊔ l2)
  bounded-distance-decompsition-Metric-Space =
    indexed-sum-Metric-Space
      ( set-bounded-distance-component-Metric-Space A)
      ( subspace-bounded-distance-component-Metric-Space A)
```
where 
- `set-bounded-distance-component-Metric-Space A` is the quotient set of
`A` by the equivalence relation of being at bounded distance;
- `subspace-bounded-distance-component-Metric-Space A` is the subspace
of elements in a given quotient class.
In each subspace `subspace-bounded-distance-component-Metric-Space A X`,
all elements are at bounded distance.

Any metric space is isometrically equivalent to its bounded distance
decomposition. The underlying equivalence is provided by the following
new results for quotient sets and equivalence classes:

```agda
module _
  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
  where

  equiv-total-equivalence-class :
    Σ (equivalence-class R) (type-subtype ∘ is-in-equivalence-class-Prop R) ≃ A
  equiv-total-equivalence-class = [...]

  equiv-total-set-quotient :
    Σ ( set-quotient R)
       ( type-subtype ∘ is-in-equivalence-class-set-quotient-Prop R) ≃
    ( A)
 equiv-total-set-quotient = [...]
```

Author: malarbol

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,21 @@ 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-equivalence-class :
+    Σ (equivalence-class R) (type-subtype ∘ is-in-equivalence-class-Prop R) ≃ A
+  equiv-total-equivalence-class =
+    ( right-unit-law-Σ-is-contr
+      ( is-torsorial-is-in-equivalence-class R)) ∘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,37 @@ module _
       ( is-surjective-quotient-map)
 ```
 
-### The map `class : A → equivalence-class R` is an effective quotient map
+## Properties
+
+### Any element is in the class of its quotient
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  (x : A)
+  where
+
+  is-in-equivalence-class-quotient-map-set-quotient :
+    is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( x)
+  is-in-equivalence-class-quotient-map-set-quotient =
+    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 :
+    type-subtype
+      ( subtype-set-quotient R (quotient-map R x))
+  inhabitant-equivalence-class-quotient-map-set-quotient =
+    (x , is-in-equivalence-class-quotient-map-set-quotient)
+```
+
+### The map `class : A → set-quotient R` is an effective quotient map
 
 ```agda
 module _
@@ -417,6 +456,135 @@ 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))
+```
+
+### Two elements in the same quotient class are similar
+
+```agda
+module _
+  {l1 l2 : Level} {A : UU l1} (R : equivalence-relation l2 A)
+  where
+
+  sim-is-in-equivalence-class-set-quotient :
+    (X : set-quotient R) {x y : A} →
+    is-in-equivalence-class-set-quotient R X x →
+    is-in-equivalence-class-set-quotient R X y →
+    sim-equivalence-relation R x y
+  sim-is-in-equivalence-class-set-quotient X {x} {y} x∈X y∈X =
+    apply-effectiveness-quotient-map
+      ( R)
+      ( ( eq-set-quotient-equivalence-class-set-quotient R X x∈X) ∙
+        ( inv (eq-set-quotient-equivalence-class-set-quotient R X y∈X)))
+```
+
+### 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-quotient-map-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-quotient-map-set-quotient x y =
+    sim-is-in-equivalence-class-set-quotient
+      ( R)
+      ( quotient-map R x)
+      ( is-in-equivalence-class-quotient-map-set-quotient R 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-set-quotient :
+    Σ ( set-quotient R)
+      ( type-subtype ∘ is-in-equivalence-class-set-quotient-Prop R) ≃
+    ( A)
+  equiv-total-set-quotient =
+    ( right-unit-law-Σ-is-contr
+      ( is-torsorial-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

@@ -47,6 +47,7 @@ module metric-spaces where
 
 open import metric-spaces.approximations-located-metric-spaces public
 open import metric-spaces.approximations-metric-spaces public
+open import metric-spaces.bounded-distance-decompositions-of-metric-spaces public
 open import metric-spaces.cartesian-products-metric-spaces public
 open import metric-spaces.category-of-metric-spaces-and-isometries public
 open import metric-spaces.category-of-metric-spaces-and-short-functions public