{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core
module Relation.Binary.Structures
{a ℓ} {A : Set a}
(_≈_ : Rel A ℓ)
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 ≡ using (_≡_)
open import Relation.Binary.Consequences
open import Relation.Binary.Definitions
private
variable
ℓ₂ : Level
record IsPartialEquivalence : Set (a ⊔ ℓ) where
field
sym : Symmetric _≈_
trans : Transitive _≈_
record IsEquivalence : Set (a ⊔ ℓ) where
field
refl : Reflexive _≈_
sym : Symmetric _≈_
trans : Transitive _≈_
reflexive : _≡_ ⇒ _≈_
reflexive ≡.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
record IsPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isEquivalence : IsEquivalence
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.
Please use ≲-respˡ-≈ instead. "
#-}
∼-respʳ-≈ = ≲-respʳ-≈
{-# WARNING_ON_USAGE ∼-respʳ-≈
"Warning: ∼-respʳ-≈ was deprecated in v2.0.
Please use ≲-respʳ-≈ instead. "
#-}
∼-resp-≈ = ≲-resp-≈
{-# WARNING_ON_USAGE ∼-resp-≈
"Warning: ∼-resp-≈ was deprecated in v2.0.
Please use ≲-resp-≈ instead. "
#-}
record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isPreorder : IsPreorder _≲_
total : Total _≲_
open IsPreorder isPreorder public
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
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
record IsStrictTotalOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isStrictPartialOrder : IsStrictPartialOrder _<_
compare : Trichotomous _≈_ _<_
open IsStrictPartialOrder isStrictPartialOrder public
hiding (module Eq)
infix 4 _≟_ _<?_
_≟_ : Decidable _≈_
_≟_ = tri⇒dec≈ compare
_<?_ : Decidable _<_
_<?_ = tri⇒dec< compare
isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
isDecStrictPartialOrder = record
{ isStrictPartialOrder = isStrictPartialOrder
; _≟_ = _≟_
; _<?_ = _<?_
}
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.
Please use Eq.isDecEquivalence instead. "
#-}
record IsDenseLinearOrder (_<_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isStrictTotalOrder : IsStrictTotalOrder _<_
dense : Dense _<_
open IsStrictTotalOrder isStrictTotalOrder public
record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
irrefl : Irreflexive _≈_ _#_
sym : Symmetric _#_
cotrans : Cotransitive _#_
_¬#_ : A → A → Set _
x ¬# y = ¬ (x # y)