    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Metrics with arbitrary domains and codomains
    ------------------------------------------------------------------------

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

    module Function.Metric where

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