1234567891011121314-------------------------------------------------------------------------- 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 publicopen import Function.Metric.Nat.Definitions publicopen import Function.Metric.Nat.Structures publicopen import Function.Metric.Nat.Bundles public