------------------------------------------------------------------------ -- The Agda standard library -- -- Definitions of properties over distance functions ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Function.Metric`. {-# OPTIONS --cubical-compatible --safe #-} module Function.Metric.Definitions where open import Algebra.Core using (Op₂) open import Data.Product.Base using (∃) open import Function.Metric.Core using (DistanceFunction) open import Level using (Level) open import Relation.Binary.Core using (Rel; _Preserves₂_⟶_⟶_) open import Relation.Nullary.Negation using (¬_) private variable a i ℓ ℓ₁ ℓ₂ : Level A : Set a I : Set i ------------------------------------------------------------------------ -- Properties Congruent : Rel A ℓ₁ → Rel I ℓ₂ → DistanceFunction A I → Set _ Congruent _≈ₐ_ _≈ᵢ_ d = d Preserves₂ _≈ₐ_ ⟶ _≈ₐ_ ⟶ _≈ᵢ_ Indiscernable : Rel A ℓ₁ → Rel I ℓ₂ → DistanceFunction A I → I → Set _ Indiscernable _≈ₐ_ _≈ᵢ_ d 0# = ∀ {x y} → d x y ≈ᵢ 0# → x ≈ₐ y Definite : Rel A ℓ₁ → Rel I ℓ₂ → DistanceFunction A I → I → Set _ Definite _≈ₐ_ _≈ᵢ_ d 0# = ∀ {x y} → x ≈ₐ y → d x y ≈ᵢ 0# NonNegative : Rel I ℓ₂ → DistanceFunction A I → I → Set _ NonNegative _≤_ d 0# = ∀ {x y} → 0# ≤ d x y Symmetric : Rel I ℓ → DistanceFunction A I → Set _ Symmetric _≈_ d = ∀ x y → d x y ≈ d y x TriangleInequality : Rel I ℓ → Op₂ I → DistanceFunction A I → _ TriangleInequality _≤_ _∙_ d = ∀ x y z → d x z ≤ (d x y ∙ d y z) Bounded : Rel I ℓ → DistanceFunction A I → Set _ Bounded _≤_ d = ∃ λ n → ∀ x y → d x y ≤ n TranslationInvariant : Rel I ℓ₂ → Op₂ A → DistanceFunction A I → Set _ TranslationInvariant _≈_ _∙_ d = ∀ {x y a} → d (x ∙ a) (y ∙ a) ≈ d x y Contracting : Rel I ℓ → (A → A) → DistanceFunction A I → Set _ Contracting _≤_ f d = ∀ x y → d (f x) (f y) ≤ d x y ContractingOnOrbits : Rel I ℓ → (A → A) → DistanceFunction A I → Set _ ContractingOnOrbits _≤_ f d = ∀ x → d (f x) (f (f x)) ≤ d x (f x) StrictlyContracting : Rel A ℓ₁ → Rel I ℓ₂ → (A → A) → DistanceFunction A I → Set _ StrictlyContracting _≈_ _<_ f d = ∀ {x y} → ¬ (y ≈ x) → d (f x) (f y) < d x y StrictlyContractingOnOrbits : Rel A ℓ₁ → Rel I ℓ₂ → (A → A) → DistanceFunction A I → Set _ StrictlyContractingOnOrbits _≈_ _<_ f d = ∀ {x} → ¬ (f x ≈ x) → d (f x) (f (f x)) < d x (f x)