    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Properties of binary relations
    ------------------------------------------------------------------------

    -- The contents of this module should be accessed via `Relation.Binary`.

    {-# OPTIONS --cubical-compatible --safe #-}

    module Relation.Binary.Definitions where

    open import Agda.Builtin.Equality using (_≡_)
    open import Data.Product.Base using (_×_; ∃-syntax)
    open import Data.Sum.Base using (_⊎_)
    open import Function.Base using (_on_; flip)
    open import Level using (Level; _⊔_; suc)
    open import Relation.Binary.Core
    open import Relation.Nullary as Nullary using (¬_; Dec)

    private
      variable
        a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level
        A : Set a
        B : Set b
        C : Set c

    ------------------------------------------------------------------------
    -- Definitions
    ------------------------------------------------------------------------

    -- Reflexivity - defined without an underlying equality. It could
    -- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`.

    -- Confusingly the convention in the library is to use the name "refl"
    -- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`,
    -- e.g. in the definition of `IsEquivalence` later in this file. This
    -- convention is a legacy from the early days of the library.

    Reflexive : Rel A ℓ → Set _
    Reflexive _∼_ = ∀ {x} → x ∼ x

    -- Generalised symmetry.

    Sym : REL A B ℓ₁ → REL B A ℓ₂ → Set _
    Sym P Q = P ⇒ flip Q

    -- Symmetry.

    Symmetric : Rel A ℓ → Set _
    Symmetric _∼_ = Sym _∼_ _∼_

    -- Generalised transitivity.

    Trans : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
    Trans P Q R = ∀ {i j k} → P i j → Q j k → R i k

    RightTrans : REL A B ℓ₁ → REL B B ℓ₂ → Set _
    RightTrans R S = Trans R S R

    LeftTrans : REL A A ℓ₁ → REL A B ℓ₂ → Set _
    LeftTrans S R = Trans S R R

    -- A flipped variant of generalised transitivity.

    TransFlip : REL A B ℓ₁ → REL B C ℓ₂ → REL A C ℓ₃ → Set _
    TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k

    -- Transitivity.

    Transitive : Rel A ℓ → Set _
    Transitive _∼_ = Trans _∼_ _∼_ _∼_

    -- Generalised antisymmetry

    Antisym : REL A B ℓ₁ → REL B A ℓ₂ → REL A B ℓ₃ → Set _
    Antisym R S E = ∀ {i j} → R i j → S j i → E i j

    -- Antisymmetry.

    Antisymmetric : Rel A ℓ₁ → Rel A ℓ₂ → Set _
    Antisymmetric _≈_ _≤_ = Antisym _≤_ _≤_ _≈_

    -- Irreflexivity - this is defined terms of the underlying equality.

    Irreflexive : REL A B ℓ₁ → REL A B ℓ₂ → Set _
    Irreflexive _≈_ _<_ = ∀ {x y} → x ≈ y → ¬ (x < y)

    -- Asymmetry.

    Asymmetric : Rel A ℓ → Set _
    Asymmetric _<_ = ∀ {x y} → x < y → ¬ (y < x)

    -- Density

    Dense : Rel A ℓ → Set _
    Dense _<_ = ∀ {x y} → x < y → ∃[ z ] x < z × z < y

    -- Generalised connex - at least one of the two relations holds.

    Connex : REL A B ℓ₁ → REL B A ℓ₂ → Set _
    Connex P Q = ∀ x y → P x y ⊎ Q y x

    -- Totality.

    Total : Rel A ℓ → Set _
    Total _∼_ = Connex _∼_ _∼_

    -- Generalised trichotomy - exactly one of three types has a witness.

    data Tri (A : Set a) (B : Set b) (C : Set c) : Set (a ⊔ b ⊔ c) where
      tri< : ( a :   A) (¬b : ¬ B) (¬c : ¬ C) → Tri A B C
      tri≈ : (¬a : ¬ A) ( b :   B) (¬c : ¬ C) → Tri A B C
      tri> : (¬a : ¬ A) (¬b : ¬ B) ( c :   C) → Tri A B C

    -- Trichotomy.

    Trichotomous : Rel A ℓ₁ → Rel A ℓ₂ → Set _
    Trichotomous _≈_ _<_ = ∀ x y → Tri (x < y) (x ≈ y) (x > y)
      where _>_ = flip _<_

    -- Generalised maximum element.

    Max : REL A B ℓ → B → Set _
    Max _≤_ T = ∀ x → x ≤ T

    -- Maximum element.

    Maximum : Rel A ℓ → A → Set _
    Maximum = Max

    -- Generalised minimum element.

    Min : REL A B ℓ → A → Set _
    Min R = Max (flip R)

    -- Minimum element.

    Minimum : Rel A ℓ → A → Set _
    Minimum = Min

    -- Definitions for apartness relations

    -- Note that Cotransitive's arguments are permuted with respect to Transitive's.
    Cotransitive : Rel A ℓ → Set _
    Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)

    Tight : Rel A ℓ₁ → Rel A ℓ₂ → Set _
    Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)

    -- Properties of order morphisms, aka order-preserving maps

    Monotonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
    Monotonic₁ _≤_ _⊑_ f = f Preserves _≤_ ⟶ _⊑_

    Antitonic₁ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
    Antitonic₁ _≤_ = Monotonic₁ (flip _≤_)

    LeftMonotonic : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
    LeftMonotonic _≤_ _⊑_ _∙_ = ∀ x → Monotonic₁ _≤_ _⊑_ (x ∙_)

    RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
    RightMonotonic _≤_ _⊑_ _∙_ = ∀ y → Monotonic₁ _≤_ _⊑_ (_∙ y)

    Monotonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
    Monotonic₂ _≤_ _⊑_ _≼_ ∙ = ∙ Preserves₂ _≤_ ⟶ _⊑_ ⟶ _≼_

    MonotonicAntitonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
    MonotonicAntitonic _≤_ _⊑_ = Monotonic₂ _≤_ (flip _⊑_)

    AntitonicMonotonic : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
    AntitonicMonotonic _≤_ = Monotonic₂ (flip _≤_)

    Antitonic₂ : Rel A ℓ₁ → Rel B ℓ₂ → Rel C ℓ₃ → (A → B → C) → Set _
    Antitonic₂ _≤_ _⊑_ = Monotonic₂ (flip _≤_) (flip _⊑_)

    Adjoint : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → (B → A) → Set _
    Adjoint _≤_ _⊑_ f g = ∀ {x y} → (f x ⊑ y → x ≤ g y) × (x ≤ g y → f x ⊑ y)

    -- Unary relations respecting a binary relation.

    _⟶_Respects_ : (A → Set ℓ₁) → (B → Set ℓ₂) → REL A B ℓ₃ → Set _
    P ⟶ Q Respects _∼_ = ∀ {x y} → x ∼ y → P x → Q y

    -- Unary relation respects a binary relation.

    _Respects_ : (A → Set ℓ₁) → Rel A ℓ₂ → Set _
    P Respects _∼_ = P ⟶ P Respects _∼_

    -- Right respecting - relatedness is preserved on the right by equality.

    _Respectsʳ_ : REL A B ℓ₁ → Rel B ℓ₂ → Set _
    _∼_ Respectsʳ _≈_ = ∀ {x} → (x ∼_) Respects _≈_

    -- Left respecting - relatedness is preserved on the left by equality.

    _Respectsˡ_ : REL A B ℓ₁ → Rel A ℓ₂ → Set _
    P Respectsˡ _∼_ = ∀ {y} → (flip P y) Respects _∼_

    -- Respecting - relatedness is preserved on both sides by equality

    _Respects₂_ : Rel A ℓ₁ → Rel A ℓ₂ → Set _
    P Respects₂ _∼_ = (P Respectsʳ _∼_) × (P Respectsˡ _∼_)

    -- Substitutivity - any two related elements satisfy exactly the same
    -- set of unary relations. Note that only the various derivatives
    -- of propositional equality can satisfy this property.

    Substitutive : Rel A ℓ₁ → (ℓ₂ : Level) → Set _
    Substitutive {A = A} _∼_ p = (P : A → Set p) → P Respects _∼_

    -- Irrelevancy - all proofs that a given pair of elements are related
    -- are indistinguishable.

    Irrelevant : REL A B ℓ → Set _
    Irrelevant _∼_ = ∀ {x y} → Nullary.Irrelevant (x ∼ y)

    -- Recomputability - we can rebuild a relevant proof given an
    -- irrelevant one.

    Recomputable : REL A B ℓ → Set _
    Recomputable _∼_ = ∀ {x y} → Nullary.Recomputable (x ∼ y)

    -- Stability

    Stable : REL A B ℓ → Set _
    Stable _∼_ = ∀ x y → Nullary.Stable (x ∼ y)

    -- Weak decidability - it is sometimes possible to determine if a given
    -- pair of elements are related.

    WeaklyDecidable : REL A B ℓ → Set _
    WeaklyDecidable _∼_ = ∀ x y → Nullary.WeaklyDecidable (x ∼ y)

    -- Decidability - it is possible to determine whether a given pair of
    -- elements are related.

    Decidable : REL A B ℓ → Set _
    Decidable _∼_ = ∀ x y → Dec (x ∼ y)

    -- Propositional equality is decidable for the type.

    DecidableEquality : (A : Set a) → Set _
    DecidableEquality A = Decidable {A = A} _≡_

    -- Universal - all pairs of elements are related

    Universal : REL A B ℓ → Set _
    Universal _∼_ = ∀ x y → x ∼ y

    -- Empty - no elements are related

    Empty : REL A B ℓ → Set _
    Empty _∼_ = ∀ {x y} → ¬ (x ∼ y)

    -- Non-emptiness - at least one pair of elements are related.

    record NonEmpty {A : Set a} {B : Set b}
                    (T : REL A B ℓ) : Set (a ⊔ b ⊔ ℓ) where
      constructor nonEmpty
      field
        {x}   : A
        {y}   : B
        proof : T x y