{-# OPTIONS --without-K --safe #-}
open import Relation.Binary.Core
module Relation.Binary.Structures
{a ℓ} {A : Set a}
(_≈_ : Rel A ℓ)
where
open import Data.Product using (proj₁; proj₂; _,_)
open import Level using (Level; _⊔_)
open import Relation.Nullary using (¬_)
open import Relation.Binary.PropositionalEquality.Core as P 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 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
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ˡ-≈
record IsTotalPreorder (_≲_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
field
isPreorder : IsPreorder _≲_
total : Total _≲_
open IsPreorder isPreorder public
renaming
( ∼-respˡ-≈ to ≲-respˡ-≈
; ∼-respʳ-≈ to ≲-respʳ-≈
; ∼-resp-≈ to ≲-resp-≈
)
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-≈
asymmetric = asym
{-# WARNING_ON_USAGE asymmetric
"Warning: asymmetric was deprecated in v0.16.
Please use asym instead."
#-}
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
isEquivalence : IsEquivalence
trans : Transitive _<_
compare : Trichotomous _≈_ _<_
infix 4 _≟_ _<?_
_≟_ : Decidable _≈_
_≟_ = tri⇒dec≈ compare
_<?_ : Decidable _<_
_<?_ = tri⇒dec< compare
isDecEquivalence : IsDecEquivalence
isDecEquivalence = record
{ isEquivalence = isEquivalence
; _≟_ = _≟_
}
module Eq = IsDecEquivalence isDecEquivalence
isStrictPartialOrder : IsStrictPartialOrder _<_
isStrictPartialOrder = record
{ isEquivalence = isEquivalence
; irrefl = tri⇒irr compare
; trans = trans
; <-resp-≈ = trans∧tri⇒resp Eq.sym Eq.trans trans compare
}
isDecStrictPartialOrder : IsDecStrictPartialOrder _<_
isDecStrictPartialOrder = record
{ isStrictPartialOrder = isStrictPartialOrder
; _≟_ = _≟_
; _<?_ = _<?_
}
open IsStrictPartialOrder isStrictPartialOrder public
using (irrefl; asym; <-respʳ-≈; <-respˡ-≈; <-resp-≈)