```------------------------------------------------------------------------
-- The Agda standard library
--
-- Structures for homogeneous binary relations
------------------------------------------------------------------------

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

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

open import Relation.Binary.Core

module Relation.Binary.Structures
{a ℓ} {A : Set a} -- The underlying set
(_≈_ : Rel A ℓ)   -- The underlying equality relation
where

open import Data.Product.Base using (proj₁; proj₂; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary.Negation.Core using (¬_)
open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
open import Relation.Binary.Consequences
open import Relation.Binary.Definitions

private
variable
ℓ₂ : Level

------------------------------------------------------------------------
-- Equivalences
------------------------------------------------------------------------
-- Note all the following equivalences refer to the equality provided
-- as a module parameter at the top of this file.

record IsPartialEquivalence : Set (a ⊔ ℓ) where
field
sym   : Symmetric _≈_
trans : Transitive _≈_

-- The preorders of this library are defined in terms of an underlying
-- equivalence relation, and hence equivalence relations are not
-- defined in terms of preorders.

-- To preserve backwards compatability, equivalence relations are
-- not defined in terms of their partial counterparts.

record IsEquivalence : Set (a ⊔ ℓ) where
field
refl  : Reflexive _≈_
sym   : Symmetric _≈_
trans : Transitive _≈_

reflexive : _≡_ ⇒ _≈_
reflexive P.refl = refl

isPartialEquivalence : IsPartialEquivalence
isPartialEquivalence = record
{ sym = sym
; trans = trans
}

record IsDecEquivalence : Set (a ⊔ ℓ) where
infix 4 _≟_
field
isEquivalence : IsEquivalence
_≟_           : Decidable _≈_

open IsEquivalence isEquivalence public

------------------------------------------------------------------------
-- Preorders
------------------------------------------------------------------------

record IsPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isEquivalence : IsEquivalence
-- Reflexivity is expressed in terms of the underlying equality:
reflexive     : _≈_ ⇒ _≲_
trans         : Transitive _≲_

module Eq = IsEquivalence isEquivalence

refl : Reflexive _≲_
refl = reflexive Eq.refl

≲-respˡ-≈ : _≲_ Respectsˡ _≈_
≲-respˡ-≈ x≈y x∼z = trans (reflexive (Eq.sym x≈y)) x∼z

≲-respʳ-≈ : _≲_ Respectsʳ _≈_
≲-respʳ-≈ x≈y z∼x = trans z∼x (reflexive x≈y)

≲-resp-≈ : _≲_ Respects₂ _≈_
≲-resp-≈ = ≲-respʳ-≈ , ≲-respˡ-≈

∼-respˡ-≈ = ≲-respˡ-≈
{-# WARNING_ON_USAGE ∼-respˡ-≈
"Warning: ∼-respˡ-≈ was deprecated in v2.0.
#-}
∼-respʳ-≈ = ≲-respʳ-≈
{-# WARNING_ON_USAGE ∼-respʳ-≈
"Warning: ∼-respʳ-≈ was deprecated in v2.0.
#-}
∼-resp-≈ = ≲-resp-≈
{-# WARNING_ON_USAGE ∼-resp-≈
"Warning: ∼-resp-≈ was deprecated in v2.0.
#-}

record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isPreorder : IsPreorder _≲_
total      : Total _≲_

open IsPreorder isPreorder public

------------------------------------------------------------------------
-- Partial orders
------------------------------------------------------------------------

record IsPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isPreorder : IsPreorder _≤_
antisym    : Antisymmetric _≈_ _≤_

open IsPreorder isPreorder public
renaming
( ∼-respˡ-≈ to ≤-respˡ-≈
; ∼-respʳ-≈ to ≤-respʳ-≈
; ∼-resp-≈  to ≤-resp-≈
)

record IsDecPartialOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
infix 4 _≟_ _≤?_
field
isPartialOrder : IsPartialOrder _≤_
_≟_            : Decidable _≈_
_≤?_           : Decidable _≤_

open IsPartialOrder isPartialOrder public
hiding (module Eq)

module Eq where

isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_           = _≟_
}

open IsDecEquivalence isDecEquivalence public

record IsStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isEquivalence : IsEquivalence
irrefl        : Irreflexive _≈_ _<_
trans         : Transitive _<_
<-resp-≈      : _<_ Respects₂ _≈_

module Eq = IsEquivalence isEquivalence

asym : Asymmetric _<_
asym {x} {y} = trans∧irr⇒asym Eq.refl trans irrefl {x = x} {y}

<-respʳ-≈ : _<_ Respectsʳ _≈_
<-respʳ-≈ = proj₁ <-resp-≈

<-respˡ-≈ : _<_ Respectsˡ _≈_
<-respˡ-≈ = proj₂ <-resp-≈

record IsDecStrictPartialOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
infix 4 _≟_ _<?_
field
isStrictPartialOrder : IsStrictPartialOrder _<_
_≟_                  : Decidable _≈_
_<?_                 : Decidable _<_

private
module SPO = IsStrictPartialOrder isStrictPartialOrder

open SPO public hiding (module Eq)

module Eq where

isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = SPO.isEquivalence
; _≟_           = _≟_
}

open IsDecEquivalence isDecEquivalence public

------------------------------------------------------------------------
-- Total orders
------------------------------------------------------------------------

record IsTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isPartialOrder : IsPartialOrder _≤_
total          : Total _≤_

open IsPartialOrder isPartialOrder public

isTotalPreorder : IsTotalPreorder _≤_
isTotalPreorder = record
{ isPreorder = isPreorder
; total      = total
}

record IsDecTotalOrder (_≤_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
infix 4 _≟_ _≤?_
field
isTotalOrder : IsTotalOrder _≤_
_≟_          : Decidable _≈_
_≤?_         : Decidable _≤_

open IsTotalOrder isTotalOrder public
hiding (module Eq)

isDecPartialOrder : IsDecPartialOrder _≤_
isDecPartialOrder = record
{ isPartialOrder = isPartialOrder
; _≟_            = _≟_
; _≤?_           = _≤?_
}

module Eq where

isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_           = _≟_
}

open IsDecEquivalence isDecEquivalence public

-- Note that these orders are decidable. The current implementation
-- of `Trichotomous` subsumes irreflexivity and asymmetry. See
-- `Relation.Binary.Structures.Biased` for ways of constructing this
-- record without having to prove `isStrictPartialOrder`.

record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isStrictPartialOrder : IsStrictPartialOrder _<_
compare              : Trichotomous _≈_ _<_

open IsStrictPartialOrder isStrictPartialOrder public
hiding (module Eq)

-- `Trichotomous` necessarily separates out the equality case so
--  it implies decidability.
infix 4 _≟_ _<?_

_≟_ : Decidable _≈_
_≟_ = tri⇒dec≈ compare

_<?_ : Decidable _<_
_<?_ = tri⇒dec< compare

isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
isDecStrictPartialOrder = record
{ isStrictPartialOrder = isStrictPartialOrder
; _≟_                  = _≟_
; _<?_                 = _<?_
}

-- Redefine the `Eq` module to include decidability proofs
module Eq where

isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_           = _≟_
}

open IsDecEquivalence isDecEquivalence public

isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_           = _≟_
}
{-# WARNING_ON_USAGE isDecEquivalence
"Warning: isDecEquivalence was deprecated in v2.0.
#-}

record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isStrictTotalOrder : IsStrictTotalOrder _<_
dense              : Dense _<_

open IsStrictTotalOrder isStrictTotalOrder public

------------------------------------------------------------------------
-- Apartness relations
------------------------------------------------------------------------

record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
irrefl  : Irreflexive _≈_ _#_
sym     : Symmetric _#_
cotrans : Cotransitive _#_

_¬#_ : A → A → Set _
x ¬# y = ¬ (x # y)
```