The precategory of metric spaces and maps

Content created by Fredrik Bakke and Louis Wasserman.

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

module metric-spaces.precategory-of-metric-spaces-and-maps where
Imports 
open import category-theory.precategories

open import foundation.function-types
open import foundation.identity-types
open import foundation.universe-levels

open import metric-spaces.maps-metric-spaces
open import metric-spaces.metric-spaces

Idea

Since the carrier type of any metric space is a set, they are the objects of a precategory where morphisms are maps between them.

Definition

module _
  {l1 l2 : Level}
  where

  precategory-map-Metric-Space :
    Precategory (lsuc l1 ⊔ lsuc l2) l1
  precategory-map-Metric-Space =
    make-Precategory
      ( Metric-Space l1 l2)
      ( map-set-Metric-Space)
      ( λ {A B C} g f → g ∘ f)
      ( λ A → id)
      ( λ {A B C D} h g f → refl)
      ( λ {A B} f → refl)
      ( λ {A B} f → refl)

Recent changes