{-# OPTIONS --cubical-compatible --safe #-}
module Function.Metric.Nat.Structures where
open import Data.Nat.Base hiding (suc)
open import Function.Base using (const)
open import Level using (Level; suc)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
open import Function.Metric.Nat.Core
open import Function.Metric.Nat.Definitions
import Function.Metric.Structures as Base
private
variable
a ℓ : Level
A : Set a
IsProtoMetric : Rel A ℓ → DistanceFunction A → Set _
IsProtoMetric _≈_ = Base.IsProtoMetric _≈_ _≡_ _≤_ 0
open Base using (module IsProtoMetric) public
IsPreMetric : Rel A ℓ → DistanceFunction A → Set _
IsPreMetric _≈_ = Base.IsPreMetric _≈_ _≡_ _≤_ 0
open Base using (module IsPreMetric) public
IsQuasiSemiMetric : Rel A ℓ → DistanceFunction A → Set _
IsQuasiSemiMetric _≈_ = Base.IsQuasiSemiMetric _≈_ _≡_ _≤_ 0
open Base using (module IsQuasiSemiMetric) public
IsSemiMetric : Rel A ℓ → DistanceFunction A → Set _
IsSemiMetric _≈_ = Base.IsSemiMetric _≈_ _≡_ _≤_ 0
open Base using (module IsSemiMetric) public
IsMetric : Rel A ℓ → DistanceFunction A → Set _
IsMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0 _+_
module IsMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
(M : IsMetric _≈_ d) where
open Base.IsGeneralMetric M public
IsUltraMetric : Rel A ℓ → DistanceFunction A → Set _
IsUltraMetric _≈_ = Base.IsGeneralMetric _≈_ _≡_ _≤_ 0 _⊔_
module IsUltraMetric {_≈_ : Rel A ℓ} {d : DistanceFunction A}
(UM : IsUltraMetric _≈_ d) where
open Base.IsGeneralMetric UM public