The precategory of metric spaces and functions

Content created by Fredrik Bakke and malarbol.

Created on 2024-09-28.
Last modified on 2024-09-28.

module metric-spaces.precategory-of-metric-spaces-and-functions 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.functions-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 functions between them.

Definition

module _
  {l1 l2 : Level}
  where

  precategory-function-Metric-Space :
    Precategory (lsuc l1 ⊔ lsuc l2) l1
  precategory-function-Metric-Space =
    make-Precategory
      ( Metric-Space l1 l2)
      ( set-map-type-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