{-# OPTIONS --without-K --safe #-}
module Relation.Binary.Bundles where
open import Level
open import Relation.Nullary using (¬_)
open import Relation.Binary.Core
open import Relation.Binary.Definitions
open import Relation.Binary.Structures
record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
field
Carrier : Set a
_≈_ : Rel Carrier ℓ
isPartialEquivalence : IsPartialEquivalence _≈_
open IsPartialEquivalence isPartialEquivalence public
infix 4 _≉_
_≉_ : Rel Carrier _
x ≉ y = ¬ (x ≈ y)
record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
isEquivalence : IsEquivalence _≈_
open IsEquivalence isEquivalence public
partialSetoid : PartialSetoid c ℓ
partialSetoid = record
{ isPartialEquivalence = isPartialEquivalence
}
open PartialSetoid partialSetoid public using (_≉_)
record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
infix 4 _≈_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ
isDecEquivalence : IsDecEquivalence _≈_
open IsDecEquivalence isDecEquivalence public
setoid : Setoid c ℓ
setoid = record
{ isEquivalence = isEquivalence
}
open Setoid setoid public using (partialSetoid; _≉_)
record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _∼_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_∼_ : Rel Carrier ℓ₂
isPreorder : IsPreorder _≈_ _∼_
open IsPreorder isPreorder public
hiding (module Eq)
module Eq where
setoid : Setoid c ℓ₁
setoid = record
{ isEquivalence = isEquivalence
}
open Setoid setoid public
record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≲_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≲_ : Rel Carrier ℓ₂
isTotalPreorder : IsTotalPreorder _≈_ _≲_
open IsTotalPreorder isTotalPreorder public
hiding (module Eq)
preorder : Preorder c ℓ₁ ℓ₂
preorder = record { isPreorder = isPreorder }
open Preorder preorder public
using (module Eq)
record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
isPartialOrder : IsPartialOrder _≈_ _≤_
open IsPartialOrder isPartialOrder public
hiding (module Eq)
preorder : Preorder c ℓ₁ ℓ₂
preorder = record
{ isPreorder = isPreorder
}
open Preorder preorder public
using (module Eq)
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 hiding (module Eq)
poset : Poset c ℓ₁ ℓ₂
poset = record
{ isPartialOrder = isPartialOrder
}
open Poset poset public
using (preorder)
module Eq where
decSetoid : DecSetoid c ℓ₁
decSetoid = record
{ isDecEquivalence = DPO.Eq.isDecEquivalence
}
open DecSetoid decSetoid public
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
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 hiding (module Eq)
strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
strictPartialOrder = record
{ isStrictPartialOrder = isStrictPartialOrder
}
module Eq where
decSetoid : DecSetoid c ℓ₁
decSetoid = record
{ isDecEquivalence = DSPO.Eq.isDecEquivalence
}
open DecSetoid decSetoid public
record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _≤_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_≤_ : Rel Carrier ℓ₂
isTotalOrder : IsTotalOrder _≈_ _≤_
open IsTotalOrder isTotalOrder public
hiding (module Eq)
poset : Poset c ℓ₁ ℓ₂
poset = record
{ isPartialOrder = isPartialOrder
}
open Poset poset public
using (module Eq; preorder)
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 hiding (module Eq)
totalOrder : TotalOrder c ℓ₁ ℓ₂
totalOrder = record
{ isTotalOrder = isTotalOrder
}
open TotalOrder totalOrder public using (poset; preorder)
decPoset : DecPoset c ℓ₁ ℓ₂
decPoset = record
{ isDecPartialOrder = isDecPartialOrder
}
open DecPoset decPoset public using (module Eq)
record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _<_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_<_ : Rel Carrier ℓ₂
isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
open IsStrictTotalOrder isStrictTotalOrder public
hiding (module Eq)
strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
strictPartialOrder = record
{ isStrictPartialOrder = isStrictPartialOrder
}
open StrictPartialOrder strictPartialOrder public
using (module Eq)
decSetoid : DecSetoid c ℓ₁
decSetoid = record
{ isDecEquivalence = isDecEquivalence
}
{-# WARNING_ON_USAGE decSetoid
"Warning: decSetoid was deprecated in v1.3.
Please use Eq.decSetoid instead."
#-}
record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
infix 4 _≈_ _#_
field
Carrier : Set c
_≈_ : Rel Carrier ℓ₁
_#_ : Rel Carrier ℓ₂
isApartnessRelation : IsApartnessRelation _≈_ _#_
open IsApartnessRelation isApartnessRelation public