------------------------------------------------------------------------
-- 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 --without-K --safe #-}

open import Relation.Binary hiding (Symmetric)

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