------------------------------------------------------------------------ -- The Agda standard library -- -- Core definitions for metrics over ℕ ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Function.Metric.Nat.Definitions where open import Algebra.Core using (Op₂) open import Data.Nat.Base open import Level using (Level) open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality.Core using (_≡_) open import Function.Metric.Nat.Core import Function.Metric.Definitions as Base private variable a : Level A : Set a ------------------------------------------------------------------------ -- Properties -- Basic Congruent : Rel A DistanceFunction A Set _ Congruent _≈ₐ_ d = Base.Congruent _≈ₐ_ _≡_ d Indiscernable : Rel A DistanceFunction A Set _ Indiscernable _≈ₐ_ d = Base.Indiscernable _≈ₐ_ _≡_ d 0 Definite : Rel A DistanceFunction A Set _ Definite _≈ₐ_ d = Base.Definite _≈ₐ_ _≡_ d 0 Symmetric : DistanceFunction A Set _ Symmetric = Base.Symmetric _≡_ Bounded : DistanceFunction A Set _ Bounded = Base.Bounded _≤_ TranslationInvariant : Op₂ A DistanceFunction A Set _ TranslationInvariant = Base.TranslationInvariant _≡_ -- Inequalities TriangleInequality : DistanceFunction A Set _ TriangleInequality = Base.TriangleInequality _≤_ _+_ MaxTriangleInequality : DistanceFunction A Set _ MaxTriangleInequality = Base.TriangleInequality _≤_ _⊔_ -- Contractions Contracting : (A A) DistanceFunction A Set _ Contracting = Base.Contracting _≤_ ContractingOnOrbits : (A A) DistanceFunction A Set _ ContractingOnOrbits = Base.ContractingOnOrbits _≤_ StrictlyContracting : Rel A (A A) DistanceFunction A Set _ StrictlyContracting _≈_ = Base.StrictlyContracting _≈_ _<_ StrictlyContractingOnOrbits : Rel A (A A) DistanceFunction A Set _ StrictlyContractingOnOrbits _≈_ = Base.StrictlyContractingOnOrbits _≈_ _<_