Functions between metric spaces

Content created by malarbol, Fredrik Bakke and Louis Wasserman.

Created on 2024-09-28.
Last modified on 2025-08-18.

module metric-spaces.functions-metric-spaces where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.sets
open import foundation.universe-levels

open import metric-spaces.metric-spaces

Idea

Functions between metric spaces are functions between their carrier types.

Definitions

The set of functions between metric spaces

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

  set-function-Metric-Space : Set (lx ⊔ ly)
  set-function-Metric-Space =
    hom-set-Set (set-Metric-Space X) (set-Metric-Space Y)

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

The identity function on a metric space

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

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

Recent changes