------------------------------------------------------------------------
-- The Agda standard library
--
-- Bundles for metrics
------------------------------------------------------------------------
 
-- The contents of this module should be accessed via `Function.Metric`.
 
{-# OPTIONS --cubical-compatible --safe #-}
 
module Function.Metric.Bundles  where
 
open import Algebra.Core using (Op₂)
open import Level using (Level; suc; _⊔_)
open import Relation.Binary.Core using (Rel)
 
open import Function.Metric.Structures
open import Function.Metric.Core
 
------------------------------------------------------------------------
-- ProtoMetric
 
record ProtoMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                 : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  infix  _≈_ _≈ᵢ_ _≤_
  field
    Carrier       : Set a
    Image         : Set i
    _≈_           : Rel Carrier ℓ₁
    _≈ᵢ_          : Rel Image ℓ₂
    _≤_           : Rel Image ℓ₃
    0#            : Image
    d             : DistanceFunction Carrier Image
    isProtoMetric : IsProtoMetric _≈_ _≈ᵢ_ _≤_ 0# d
 
  open IsProtoMetric isProtoMetric public
 
------------------------------------------------------------------------
-- PreMetric
 
record PreMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
               : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  infix  _≈_ _≈ᵢ_ _≤_
  field
    Carrier     : Set a
    Image       : Set i
    _≈_         : Rel Carrier ℓ₁
    _≈ᵢ_        : Rel Image ℓ₂
    _≤_         : Rel Image ℓ₃
    0#          : Image
    d           : DistanceFunction Carrier Image
    isPreMetric : IsPreMetric _≈_ _≈ᵢ_ _≤_ 0# d
 
  open IsPreMetric isPreMetric public
 
  protoMetric : ProtoMetric a i ℓ₁ ℓ₂ ℓ₃
  protoMetric = record
    { isProtoMetric = isProtoMetric
    }
 
------------------------------------------------------------------------
-- QuasiSemiMetric
 
record QuasiSemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                     : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
 
  infix  _≈_ _≈ᵢ_ _≤_
  field
    Carrier           : Set a
    Image             : Set i
    _≈_               : Rel Carrier ℓ₁
    _≈ᵢ_              : Rel Image ℓ₂
    _≤_               : Rel Image ℓ₃
    0#                : Image
    d                 : DistanceFunction Carrier Image
    isQuasiSemiMetric : IsQuasiSemiMetric _≈_ _≈ᵢ_ _≤_ 0# d
 
  open IsQuasiSemiMetric isQuasiSemiMetric public
 
  preMetric : PreMetric a i ℓ₁ ℓ₂ ℓ₃
  preMetric = record
    { isPreMetric = isPreMetric
    }
 
  open PreMetric preMetric public
    using (protoMetric)
 
------------------------------------------------------------------------
-- SemiMetric
 
record SemiMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  infix  _≈_ _≈ᵢ_ _≤_
  field
    Carrier      : Set a
    Image        : Set i
    _≈_          : Rel Carrier ℓ₁
    _≈ᵢ_         : Rel Image ℓ₂
    _≤_          : Rel Image ℓ₃
    0#           : Image
    d            : DistanceFunction Carrier Image
    isSemiMetric : IsSemiMetric _≈_ _≈ᵢ_ _≤_ 0# d
 
  open IsSemiMetric isSemiMetric public
 
  quasiSemiMetric : QuasiSemiMetric a i ℓ₁ ℓ₂ ℓ₃
  quasiSemiMetric = record
    { isQuasiSemiMetric = isQuasiSemiMetric
    }
 
  open QuasiSemiMetric quasiSemiMetric public
    using (protoMetric; preMetric)
 
------------------------------------------------------------------------
-- GeneralMetric
 
-- Note that this package is not necessarily a metric in the classical
-- sense as there is no way to ensure that the _∙_ operator really
-- represents addition. See `Function.Metric.Nat` and
-- `Function.Metric.Rational` for more specialised `Metric` and
-- `UltraMetric` packages.
 
-- See the discussion accompanying the `IsGeneralMetric` structure for
-- more details.
 
record GeneralMetric (a i ℓ₁ ℓ₂ ℓ₃ : Level)
                   : Set (suc (a ⊔ i ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃)) where
  infix  _≈_ _≈ᵢ_ _≤_
  infixl  _∙_
  field
    Carrier         : Set a
    Image           : Set i
    _≈_             : Rel Carrier ℓ₁
    _≈ᵢ_            : Rel Image ℓ₂
    _≤_             : Rel Image ℓ₃
    0#              : Image
    _∙_             : Op₂ Image
    d               : DistanceFunction Carrier Image
    isGeneralMetric : IsGeneralMetric _≈_ _≈ᵢ_ _≤_ 0# _∙_ d
 
  open IsGeneralMetric isGeneralMetric public
 
  semiMetric : SemiMetric a i ℓ₁ ℓ₂ ℓ₃
  semiMetric = record
    { isSemiMetric = isSemiMetric
    }
 
  open SemiMetric semiMetric public
    using (protoMetric; preMetric; quasiSemiMetric)