------------------------------------------------------------------------
-- 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
open import Relation.Binary.PropositionalEquality
  using (_≡_; isEquivalence)

open import Function.Metric.Nat.Core
open import Function.Metric.Nat.Structures
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)