------------------------------------------------------------------------ -- The Agda standard library -- -- Bundles for homogeneous binary relations ------------------------------------------------------------------------ -- The contents of this module should be accessed via `Relation.Binary`. {-# OPTIONS --cubical-compatible --safe #-} module Relation.Binary.Bundles where open import Function.Base using (flip) open import Level using (Level; suc; _⊔_) open import Relation.Binary.Core using (Rel) open import Relation.Binary.Bundles.Raw using (RawRelation; RawSetoid) open import Relation.Binary.Structures -- most of it open import Relation.Nullary.Negation.Core using (¬_) ------------------------------------------------------------------------ -- Setoids ------------------------------------------------------------------------ record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where infix 4 _≈_ field Carrier : Set a _≈_ : Rel Carrier ℓ isPartialEquivalence : IsPartialEquivalence _≈_ open IsPartialEquivalence isPartialEquivalence public rawSetoid : RawSetoid _ _ rawSetoid = record { _≈_ = _≈_ } open RawSetoid rawSetoid public hiding (Carrier; _≈_ ) record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ isEquivalence : IsEquivalence _≈_ open IsEquivalence isEquivalence public using (refl; reflexive; isPartialEquivalence) partialSetoid : PartialSetoid c ℓ partialSetoid = record { isPartialEquivalence = isPartialEquivalence } open PartialSetoid partialSetoid public hiding (Carrier; _≈_; isPartialEquivalence) record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≈_ field Carrier : Set c _≈_ : Rel Carrier ℓ isDecEquivalence : IsDecEquivalence _≈_ open IsDecEquivalence isDecEquivalence public using (_≟_; isEquivalence) setoid : Setoid c ℓ setoid = record { isEquivalence = isEquivalence } open Setoid setoid public hiding (Carrier; _≈_; isEquivalence) ------------------------------------------------------------------------ -- Preorders ------------------------------------------------------------------------ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≲_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ -- The underlying equality. _≲_ : Rel Carrier ℓ₂ -- The relation. isPreorder : IsPreorder _≈_ _≲_ open IsPreorder isPreorder public hiding (module Eq) module Eq where setoid : Setoid c ℓ₁ setoid = record { isEquivalence = isEquivalence } open Setoid setoid public rawRelation : RawRelation _ _ _ rawRelation = record { _≈_ = _≈_ ; _∼_ = _≲_ } open RawRelation rawRelation public renaming (_≁_ to _⋦_; _∼ᵒ_ to _≳_; _≁ᵒ_ to _⋧_) hiding (Carrier; _≈_) -- Deprecated. {-# WARNING_ON_USAGE _∼_ "Warning: _∼_ was deprecated in v2.0. Please use _≲_ instead. " #-} record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≲_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ -- The underlying equality. _≲_ : Rel Carrier ℓ₂ -- The relation. isTotalPreorder : IsTotalPreorder _≈_ _≲_ open IsTotalPreorder isTotalPreorder public using (total; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record { isPreorder = isPreorder } open Preorder preorder public hiding (Carrier; _≈_; _≲_; isPreorder) record DecPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where field Carrier : Set c _≈_ : Rel Carrier ℓ₁ -- The underlying equality. _≲_ : Rel Carrier ℓ₂ -- The relation. isDecPreorder : IsDecPreorder _≈_ _≲_ private module DPO = IsDecPreorder isDecPreorder open DPO public using (_≟_; _≲?_; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record { isPreorder = isPreorder } open Preorder preorder public hiding (Carrier; _≈_; _≲_; isPreorder; module Eq) module Eq where decSetoid : DecSetoid c ℓ₁ decSetoid = record { isDecEquivalence = DPO.Eq.isDecEquivalence } open DecSetoid decSetoid public ------------------------------------------------------------------------ -- Partial orders ------------------------------------------------------------------------ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _≤_ : Rel Carrier ℓ₂ isPartialOrder : IsPartialOrder _≈_ _≤_ open IsPartialOrder isPartialOrder public using (antisym; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record { isPreorder = isPreorder } open Preorder preorder public hiding (Carrier; _≈_; _≲_; isPreorder; _⋦_; _≳_; _⋧_) renaming ( ≲-respˡ-≈ to ≤-respˡ-≈ ; ≲-respʳ-≈ to ≤-respʳ-≈ ; ≲-resp-≈ to ≤-resp-≈ ) open RawRelation rawRelation public renaming (_≁_ to _≰_; _∼ᵒ_ to _≥_; _≁ᵒ_ to _≱_) hiding (Carrier; _≈_ ; _∼_; _≉_; rawSetoid) record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _≤_ : Rel Carrier ℓ₂ isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ private module DPO = IsDecPartialOrder isDecPartialOrder open DPO public using (_≟_; _≤?_; isPartialOrder; isDecPreorder) poset : Poset c ℓ₁ ℓ₂ poset = record { isPartialOrder = isPartialOrder } open Poset poset public hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq) decPreorder : DecPreorder c ℓ₁ ℓ₂ decPreorder = record { isDecPreorder = isDecPreorder } open DecPreorder decPreorder public using (module Eq) record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _<_ : Rel Carrier ℓ₂ isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_ open IsStrictPartialOrder isStrictPartialOrder public hiding (module Eq) module Eq where setoid : Setoid c ℓ₁ setoid = record { isEquivalence = isEquivalence } open Setoid setoid public rawRelation : RawRelation _ _ _ rawRelation = record { _≈_ = _≈_ ; _∼_ = _<_ } open RawRelation rawRelation public renaming (_≁_ to _≮_; _∼ᵒ_ to _>_; _≁ᵒ_ to _≯_) hiding (Carrier; _≈_ ; _∼_) record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _<_ : Rel Carrier ℓ₂ isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder open DSPO public using (_<?_; _≟_; isStrictPartialOrder) strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂ strictPartialOrder = record { isStrictPartialOrder = isStrictPartialOrder } open StrictPartialOrder strictPartialOrder public hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq) module Eq where decSetoid : DecSetoid c ℓ₁ decSetoid = record { isDecEquivalence = DSPO.Eq.isDecEquivalence } open DecSetoid decSetoid public ------------------------------------------------------------------------ -- Total orders ------------------------------------------------------------------------ record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _≤_ : Rel Carrier ℓ₂ isTotalOrder : IsTotalOrder _≈_ _≤_ open IsTotalOrder isTotalOrder public using (total; isPartialOrder; isTotalPreorder) poset : Poset c ℓ₁ ℓ₂ poset = record { isPartialOrder = isPartialOrder } open Poset poset public hiding (Carrier; _≈_; _≤_; isPartialOrder) totalPreorder : TotalPreorder c ℓ₁ ℓ₂ totalPreorder = record { isTotalPreorder = isTotalPreorder } record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≤_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _≤_ : Rel Carrier ℓ₂ isDecTotalOrder : IsDecTotalOrder _≈_ _≤_ private module DTO = IsDecTotalOrder isDecTotalOrder open DTO public using (_≟_; _≤?_; isTotalOrder; isDecPartialOrder) totalOrder : TotalOrder c ℓ₁ ℓ₂ totalOrder = record { isTotalOrder = isTotalOrder } open TotalOrder totalOrder public hiding (Carrier; _≈_; _≤_; isTotalOrder; module Eq) decPoset : DecPoset c ℓ₁ ℓ₂ decPoset = record { isDecPartialOrder = isDecPartialOrder } open DecPoset decPoset public using (module Eq) -- Note that these orders are decidable. The current implementation -- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable -- definition capturing these three properties implies decidability -- as `Trichotomous` necessarily separates out the equality case. record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _<_ : Rel Carrier ℓ₂ isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_ open IsStrictTotalOrder isStrictTotalOrder public using ( _≟_; _<?_; compare; isStrictPartialOrder ; isDecStrictPartialOrder; isDecEquivalence ) strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂ strictPartialOrder = record { isStrictPartialOrder = isStrictPartialOrder } open StrictPartialOrder strictPartialOrder public hiding (Carrier; _≈_; _<_; isStrictPartialOrder; module Eq) decStrictPartialOrder : DecStrictPartialOrder c ℓ₁ ℓ₂ decStrictPartialOrder = record { isDecStrictPartialOrder = isDecStrictPartialOrder } open DecStrictPartialOrder decStrictPartialOrder public using (module Eq) decSetoid : DecSetoid c ℓ₁ decSetoid = record { isDecEquivalence = Eq.isDecEquivalence } {-# WARNING_ON_USAGE decSetoid "Warning: decSetoid was deprecated in v1.3. Please use Eq.decSetoid instead." #-} record DenseLinearOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _<_ : Rel Carrier ℓ₂ isDenseLinearOrder : IsDenseLinearOrder _≈_ _<_ open IsDenseLinearOrder isDenseLinearOrder public using (isStrictTotalOrder; dense) strictTotalOrder : StrictTotalOrder c ℓ₁ ℓ₂ strictTotalOrder = record { isStrictTotalOrder = isStrictTotalOrder } open StrictTotalOrder strictTotalOrder public hiding (Carrier; _≈_; _<_; isStrictTotalOrder) ------------------------------------------------------------------------ -- Apartness relations ------------------------------------------------------------------------ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _#_ field Carrier : Set c _≈_ : Rel Carrier ℓ₁ _#_ : Rel Carrier ℓ₂ isApartnessRelation : IsApartnessRelation _≈_ _#_ open IsApartnessRelation isApartnessRelation public hiding (_¬#_) rawRelation : RawRelation _ _ _ rawRelation = record { _≈_ = _≈_ ; _∼_ = _#_ } open RawRelation rawRelation public renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_) hiding (Carrier; _≈_ ; _∼_)