Monotonic premetric structures on types

Content created by Fredrik Bakke and malarbol.

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

module metric-spaces.monotonic-premetric-structures where
Imports 
open import elementary-number-theory.positive-rational-numbers

open import foundation.propositions
open import foundation.universe-levels

open import metric-spaces.premetric-structures

Idea

A premetric is monotonic if any d₁-neighborhoods are d₂-neighborhoods for d₁ < d₂, i.e., if the subsets of upper bounds on the distance between any two points are upper stable.

Definitions

The property of being a monotonic premetric structure

module _
  {l1 l2 : Level} {A : UU l1} (B : Premetric l2 A)
  where

  is-monotonic-prop-Premetric : Prop (l1 ⊔ l2)
  is-monotonic-prop-Premetric =
    Π-Prop
      ( A)
      ( λ x →
        ( Π-Prop
          ( A)
          ( λ y →
            ( Π-Prop
              ( ℚ⁺)
              ( λ d₁ →
                ( Π-Prop
                  ( ℚ⁺)
                  ( λ d₂ →
                    ( Π-Prop
                      ( le-ℚ⁺ d₁ d₂)
                      ( λ H →
                        hom-Prop (B d₁ x y) (B d₂ x y))))))))))

  is-monotonic-Premetric : UU (l1 ⊔ l2)
  is-monotonic-Premetric = type-Prop is-monotonic-prop-Premetric

  is-prop-is-monotonic-Premetric : is-prop is-monotonic-Premetric
  is-prop-is-monotonic-Premetric = is-prop-type-Prop is-monotonic-prop-Premetric

Recent changes