------------------------------------------------------------------------
-- The Agda standard library
--
-- Some metric structures (not packed up with sets, operations, etc.)
------------------------------------------------------------------------
 
-- The contents of this module should usually be accessed via
-- `Function.Metric`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Structures using (IsPartialOrder; IsEquivalence)
 
module Function.Metric.Structures
  {a i ℓ₁ ℓ₂ ℓ₃} {A : Set a} {I : Set i}
  (_≈ₐ_ : Rel A ℓ₁) (_≈ᵢ_ : Rel I ℓ₂) (_≤_ : Rel I ℓ₃) (0# : I) where
 
open import Algebra.Core using (Op₂)
open import Function.Metric.Core
open import Function.Metric.Definitions
open import Level using (_⊔_)
 
------------------------------------------------------------------------
-- Proto-metrics
 
-- We do not insist that the ordering relation is total as otherwise
-- we would exclude the real numbers.
 
record IsProtoMetric (d : DistanceFunction A I)
                   : Set (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isPartialOrder   : IsPartialOrder _≈ᵢ_ _≤_
    ≈-isEquivalence  : IsEquivalence _≈ₐ_
    cong             : Congruent _≈ₐ_ _≈ᵢ_ d
    nonNegative      : NonNegative _≤_ d 0#
 
  open IsPartialOrder isPartialOrder public
    renaming (module Eq to EqI)
 
  module EqC = IsEquivalence ≈-isEquivalence
 
------------------------------------------------------------------------
-- Pre-metrics
 
record IsPreMetric (d : DistanceFunction A I)
                 : Set (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isProtoMetric : IsProtoMetric d
    ≈⇒0           : Definite _≈ₐ_ _≈ᵢ_ d 0#
 
  open IsProtoMetric isProtoMetric public
 
------------------------------------------------------------------------
-- Quasi-semi-metrics
 
record IsQuasiSemiMetric (d : DistanceFunction A I)
                       : Set (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isPreMetric : IsPreMetric d
    0⇒≈         : Indiscernable _≈ₐ_ _≈ᵢ_ d 0#
 
  open IsPreMetric isPreMetric public
 
------------------------------------------------------------------------
-- Semi-metrics
 
record IsSemiMetric (d : DistanceFunction A I)
                  : Set (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isQuasiSemiMetric : IsQuasiSemiMetric d
    sym               : Symmetric _≈ᵢ_ d
 
  open IsQuasiSemiMetric isQuasiSemiMetric public
 
------------------------------------------------------------------------
-- General metrics
 
-- A general metric obeys a generalised form of the triangle inequality.
-- It can be specialised to a standard metric/ultrametric/inframetric
-- etc. by providing the correct operator.
--
-- Furthermore we do not assume that _∙_ & 0# form a monoid as
-- associativity does not hold for p-relaxed metrics/p-inframetrics and
-- the identity laws do not hold for ultrametrics over negative
-- codomains.
--
-- See "Properties of distance spaces with power triangle inequalities"
-- by Daniel J. Greenhoe, 2016 (arXiv)
 
record IsGeneralMetric (_∙_ : Op₂ I) (d : DistanceFunction A I)
                     : Set (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃) where
  field
    isSemiMetric : IsSemiMetric d
    triangle     : TriangleInequality _≤_ _∙_ d
 
  open IsSemiMetric isSemiMetric public