------------------------------------------------------------------------
-- The Agda standard library
--
-- Core definitions for metrics over ℚ
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

open import Data.Rational.Base
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.Rational.Core
open import Function.Metric.Rational.Definitions
import Function.Metric.Structures as Base

module Function.Metric.Rational.Structures where

private
  variable
    a ℓ : Level
    A   : Set a

------------------------------------------------------------------------
-- Proto-metrics

IsProtoMetric : Rel A ℓ → DistanceFunction A → Set _
IsProtoMetric _≈_ = Base.IsProtoMetric _≈_ _≡_ _≤_ 0ℚ

open Base using (module IsProtoMetric) public

------------------------------------------------------------------------
-- Pre-metrics

IsPreMetric : Rel A ℓ → DistanceFunction A → Set _
IsPreMetric _≈_ = Base.IsPreMetric _≈_ _≡_ _≤_ 0ℚ

open Base using (module IsPreMetric) public

------------------------------------------------------------------------
-- Quasi-semi-metrics

IsQuasiSemiMetric : Rel A ℓ → DistanceFunction A → Set _
IsQuasiSemiMetric _≈_ = Base.IsQuasiSemiMetric _≈_ _≡_ _≤_ 0ℚ

open Base using (module IsQuasiSemiMetric) public

------------------------------------------------------------------------
-- Semi-metrics

IsSemiMetric : Rel A ℓ → DistanceFunction A → Set _
IsSemiMetric _≈_ = Base.IsSemiMetric _≈_ _≡_ _≤_ 0ℚ

open Base using (module IsSemiMetric) public

------------------------------------------------------------------------
-- Metrics

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

------------------------------------------------------------------------
-- Ultra-metrics

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