    ------------------------------------------------------------------------
    -- 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)