Extensionality of pseudometric spaces

Content created by Louis Wasserman and malarbol.

Created on 2025-08-18.
Last modified on 2025-08-18.

module metric-spaces.extensionality-pseudometric-spaces where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.fundamental-theorem-of-identity-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.torsorial-type-families
open import foundation.transport-along-identifications
open import foundation.universe-levels

open import metric-spaces.pseudometric-spaces
open import metric-spaces.similarity-of-elements-pseudometric-spaces

Idea

A pseudometric space is called extensional if the similarity relation has propositional fibers. This is equivalent to the following conditions:

The carrier type of an extensional pseudometric space is a set.

Definitions

The property of being an extensional pseudometric space

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  where

  is-extensional-prop-Pseudometric-Space : Prop (l1 ⊔ l2)
  is-extensional-prop-Pseudometric-Space =
    Π-Prop
      ( type-Pseudometric-Space A)
      ( is-prop-Prop ∘
        Σ (type-Pseudometric-Space A) ∘
        sim-Pseudometric-Space A)

  is-extensional-Pseudometric-Space : UU (l1 ⊔ l2)
  is-extensional-Pseudometric-Space =
    type-Prop is-extensional-prop-Pseudometric-Space

  is-prop-is-extensional-Pseudometric-Space :
    is-prop is-extensional-Pseudometric-Space
  is-prop-is-extensional-Pseudometric-Space =
    is-prop-type-Prop is-extensional-prop-Pseudometric-Space

Tightness of a pseudometric space

A pseudometric space is tight if any two similar elements are equal.

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  where

  is-tight-Pseudometric-Space : UU (l1 ⊔ l2)
  is-tight-Pseudometric-Space =
    (x y : type-Pseudometric-Space A) →
    sim-Pseudometric-Space A x y →
    x ＝ y

Properties

Tight pseudometric spaces are extensional

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (T : is-tight-Pseudometric-Space A)
  where

  is-extensional-is-tight-Pseudometric-Space :
    is-extensional-Pseudometric-Space A
  is-extensional-is-tight-Pseudometric-Space x =
    is-prop-all-elements-equal
      ( λ (u , I) (v , J) →
        eq-type-subtype
          ( sim-prop-Pseudometric-Space A x)
          ( inv (T x u I) ∙ T x v J))

Characterization of equality in an extensional pseudometric space

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (E : is-extensional-Pseudometric-Space A)
  where

  is-torsorial-sim-is-extensional-Pseudometric-Space :
    (x : type-Pseudometric-Space A) →
    is-torsorial (sim-Pseudometric-Space A x)
  is-torsorial-sim-is-extensional-Pseudometric-Space x =
    is-proof-irrelevant-is-prop
      ( E x)
      ( x , refl-sim-Pseudometric-Space A x)

  is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space :
    (x y : type-Pseudometric-Space A) →
    is-equiv (sim-eq-Pseudometric-Space A x y)
  is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space x =
    fundamental-theorem-id
      ( is-torsorial-sim-is-extensional-Pseudometric-Space x)
      ( sim-eq-Pseudometric-Space A x)

  equiv-sim-eq-is-extensional-Pseudometric-Space :
    (x y : type-Pseudometric-Space A) →
    (x ＝ y) ≃ (sim-Pseudometric-Space A x y)
  equiv-sim-eq-is-extensional-Pseudometric-Space x y =
    ( sim-eq-Pseudometric-Space A x y) ,
    ( is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space x y)

  eq-sim-is-extensional-Pseudometric-Space :
    (x y : type-Pseudometric-Space A) →
    sim-Pseudometric-Space A x y →
    x ＝ y
  eq-sim-is-extensional-Pseudometric-Space x y =
    map-inv-equiv (equiv-sim-eq-is-extensional-Pseudometric-Space x y)

Extensional pseudometric spaces are tight

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (E : is-extensional-Pseudometric-Space A)
  where

  is-tight-is-extensional-Pseudometric-Space :
    is-tight-Pseudometric-Space A
  is-tight-is-extensional-Pseudometric-Space =
    eq-sim-is-extensional-Pseudometric-Space A E

The carrier type of an extensional pseudometric space is a set

module _
  {l1 l2 : Level} (A : Pseudometric-Space l1 l2)
  (E : is-extensional-Pseudometric-Space A)
  where

  is-set-type-is-extensional-Pseudometric-Space :
    is-set (type-Pseudometric-Space A)
  is-set-type-is-extensional-Pseudometric-Space x y =
    is-prop-is-equiv
      ( is-fiberwise-equiv-sim-eq-is-extensional-Pseudometric-Space
        ( A)
        ( E)
        ( x)
        ( y))
      ( is-prop-sim-Pseudometric-Space A x y)

See also

Recent changes