    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Metrics with ℕ as the codomain of the metric function
    ------------------------------------------------------------------------

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

    module Function.Metric.Nat where

    open import Function.Metric.Nat.Core public
    open import Function.Metric.Nat.Definitions public
    open import Function.Metric.Nat.Structures public
    open import Function.Metric.Nat.Bundles public