Rational neighborhood subtypes

Content created by malarbol.

Created on 2026-10-18.
Last modified on 2026-10-18.

module metric-spaces.rational-neighborhood-subtypes where
Imports 
open import elementary-number-theory.positive-rational-numbers

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

Idea

A rational neighborhood subtype is a type family of subtypes indexed by the positive rational numbers.

They are the underlying type of Cauchy filters on pseudometric spaces.

Definitions

Rational neighborhood subtypes

module _
  {l1 : Level} (l : Level) (A : UU l1)
  where

  Rational-Neighborhood-Subtype : UU (l1 ⊔ lsuc l)
  Rational-Neighborhood-Subtype = ℚ⁺ → subtype l A

module _
  {l1 l : Level} {A : UU l1} (U : Rational-Neighborhood-Subtype l A)
  where

  is-in-Rational-Neighborhood-Subtype : ℚ⁺ → A → UU l
  is-in-Rational-Neighborhood-Subtype d x = type-Prop (U d x)

  is-prop-is-in-Rational-Neighborhood-Subtype :
    (d : ℚ⁺) (x : A) → is-prop (is-in-Rational-Neighborhood-Subtype d x)
  is-prop-is-in-Rational-Neighborhood-Subtype d x =
    is-prop-type-Prop (U d x)

Recent changes