Maps between pseudometric spaces

Content created by Fredrik Bakke and Louis Wasserman.

Created on 2026-01-01.
Last modified on 2026-01-01.

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

open import metric-spaces.pseudometric-spaces

Idea

Maps between pseudometric spaces are functions between their carrier types.

Definitions

The type of maps between pseudometric spaces

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

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

The identity map on a pseudometric space

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

  id-map-Pseudometric-Space : map-Pseudometric-Space M M
  id-map-Pseudometric-Space = id

Constant maps between pseudometric spaces

module _
  {l1 l2 l1' l2' : Level}
  (A : Pseudometric-Space l1 l2) (B : Pseudometric-Space l1' l2')
  (b : type-Pseudometric-Space B)
  where

  const-map-Pseudometric-Space : map-Pseudometric-Space A B
  const-map-Pseudometric-Space = const (type-Pseudometric-Space A) b

Recent changes