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

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

    module Function.Metric.Rational where

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