------------------------------------------------------------------------ -- The Agda standard library -- -- Core definitions for metrics over ℕ ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Metric.Nat.Definitions where open import Algebra.Core using (Op₂) open import Data.Nat.Base using (ℕ; _≤_; _+_; _⊔_ ; _<_) open import Level using (Level) open import Relation.Binary.Core using (Rel) 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 _≈_ _<_