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

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

{-# OPTIONS --without-K --safe #-}

module Relation.Binary.Definitions where

open import Agda.Builtin.Equality using (_≡_)

open import Data.Maybe.Base using (Maybe)
open import Data.Product using (_×_)
open import Data.Sum.Base using (_⊎_)
open import Function.Base using (_on_; flip)
open import Level
open import Relation.Binary.Core
open import Relation.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

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

-- Generalised connex - exactly 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₁ _≤_ _⊑_ f = f Preserves (flip _≤_)  _⊑_

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 _≤_ _⊑_ _≼_  =  Preserves₂ _≤_  (flip _⊑_)  _≼_

AntitonicMonotonic : Rel A ℓ₁  Rel B ℓ₂  Rel C ℓ₃  (A  B  C)  Set _
AntitonicMonotonic _≤_ _⊑_ _≼_  =  Preserves₂ (flip _≤_)  _⊑_  _≼_

Antitonic₂ : Rel A ℓ₁  Rel B ℓ₂  Rel C ℓ₃  (A  B  C)  Set _
Antitonic₂ _≤_ _⊑_ _≼_  =  Preserves₂ (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 _∼_

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

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

WeaklyDecidable : REL A B   Set _
WeaklyDecidable _∼_ =  x y  Maybe (x  y)

-- Propositional equality is decidable for the type.

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

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

Irrelevant : REL A B   Set _
Irrelevant _∼_ =  {x y} (a b : x  y)  a  b

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

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

-- Universal - all pairs of elements are related

Universal : REL A B   Set _
Universal _∼_ =  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