    ------------------------------------------------------------------------
    -- 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