Functions between pseudometric spaces

Content created by Louis Wasserman and malarbol.

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

module metric-spaces.functions-pseudometric-spaces where
Imports 
open import foundation.function-types
open import foundation.universe-levels

open import metric-spaces.pseudometric-spaces

Idea

Functions between pseudometric spaces are functions between their carrier types.

Definitions

The type of functions between pseudometric spaces

module _
  {lx lx' ly ly' : Level}
  (X : Pseudometric-Space lx lx') (Y : Pseudometric-Space ly ly')
  where

  type-function-Pseudometric-Space : UU (lx ⊔ ly)
  type-function-Pseudometric-Space =
    type-Pseudometric-Space X → type-Pseudometric-Space Y

The identity function on a pseudometric space

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

  id-Pseudometric-Space : type-function-Pseudometric-Space M M
  id-Pseudometric-Space = id

Recent changes