    ------------------------------------------------------------------------
    -- 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 4 _≈_ _≈ᵢ_ _≤_
      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 4 _≈_ _≈ᵢ_ _≤_
      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 4 _≈_ _≈ᵢ_ _≤_
      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 4 _≈_ _≈ᵢ_ _≤_
      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 4 _≈_ _≈ᵢ_ _≤_
      infixl 6 _∙_
      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)