    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bundles for metrics over ℕ
    ------------------------------------------------------------------------

    -- Unfortunately, unlike definitions and structures, the bundles over
    -- general metric spaces cannot be reused as it is impossible to
    -- constrain the image set to ℕ.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Function.Metric.Nat.Bundles where

    open import Data.Nat.Base hiding (suc; _⊔_)
    open import Function.Base using (const)
    open import Level using (Level; suc; _⊔_)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)
    open import Relation.Binary.PropositionalEquality.Properties
      using (isEquivalence)
    open import Function.Metric.Nat.Core using (DistanceFunction)
    open import Function.Metric.Nat.Structures
      using (IsProtoMetric; IsPreMetric; IsQuasiSemiMetric; IsSemiMetric
            ; IsMetric; IsUltraMetric)
    open import Function.Metric.Bundles as Base using (GeneralMetric)

    ------------------------------------------------------------------------
    -- Proto-metric

    record ProtoMetric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier       : Set a
        _≈_           : Rel Carrier ℓ
        d             : DistanceFunction Carrier
        isProtoMetric : IsProtoMetric _≈_ d

      open IsProtoMetric isProtoMetric public

    ------------------------------------------------------------------------
    -- PreMetric

    record PreMetric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier     : Set a
        _≈_         : Rel Carrier ℓ
        d           : DistanceFunction Carrier
        isPreMetric : IsPreMetric _≈_ d

      open IsPreMetric isPreMetric public

      protoMetric : ProtoMetric a ℓ
      protoMetric = record
        { isProtoMetric = isProtoMetric
        }

    ------------------------------------------------------------------------
    -- QuasiSemiMetric

    record QuasiSemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier           : Set a
        _≈_               : Rel Carrier ℓ
        d                 : DistanceFunction Carrier
        isQuasiSemiMetric : IsQuasiSemiMetric _≈_ d

      open IsQuasiSemiMetric isQuasiSemiMetric public

      preMetric : PreMetric a ℓ
      preMetric = record
        { isPreMetric = isPreMetric
        }

      open PreMetric preMetric public
        using (protoMetric)

    ------------------------------------------------------------------------
    -- SemiMetric

    record SemiMetric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier      : Set a
        _≈_          : Rel Carrier ℓ
        d            : DistanceFunction Carrier
        isSemiMetric : IsSemiMetric _≈_ d

      open IsSemiMetric isSemiMetric public

      quasiSemiMetric : QuasiSemiMetric a ℓ
      quasiSemiMetric = record
        { isQuasiSemiMetric = isQuasiSemiMetric
        }

      open QuasiSemiMetric quasiSemiMetric public
        using (protoMetric; preMetric)

    ------------------------------------------------------------------------
    -- Metrics

    record Metric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier  : Set a
        _≈_      : Rel Carrier ℓ
        d        : DistanceFunction Carrier
        isMetric : IsMetric _≈_ d

      open IsMetric isMetric public

      semiMetric : SemiMetric a ℓ
      semiMetric = record
        { isSemiMetric = isSemiMetric
        }

      open SemiMetric semiMetric public
        using (protoMetric; preMetric; quasiSemiMetric)

    ------------------------------------------------------------------------
    -- UltraMetrics

    record UltraMetric a ℓ : Set (suc (a ⊔ ℓ)) where
      infix 4 _≈_
      field
        Carrier       : Set a
        _≈_           : Rel Carrier ℓ
        d             : DistanceFunction Carrier
        isUltraMetric : IsUltraMetric _≈_ d

      open IsUltraMetric isUltraMetric public

      semiMetric : SemiMetric a ℓ
      semiMetric = record
        { isSemiMetric = isSemiMetric
        }

      open SemiMetric semiMetric public
        using (protoMetric; preMetric; quasiSemiMetric)