1
------------------------------------------------------------------------
2
-- Properties of homogeneous binary relations
3
------------------------------------------------------------------------
5
{-# OPTIONS --universe-polymorphism #-}
7
module Relation.Binary where
9
open import Data.Product
11
open import Data.Function
13
import Relation.Binary.PropositionalEquality.Core as PropEq
14
open import Relation.Binary.Consequences
15
open import Relation.Binary.Core as Core using (_≡_)
17
------------------------------------------------------------------------
18
-- Simple properties and equivalence relations
20
open Core public hiding (_≡_; refl; _≢_)
22
------------------------------------------------------------------------
25
record IsPreorder {a ℓ₁ ℓ₂} {A : Set a}
26
(_≈_ : Rel A ℓ₁) -- The underlying equality.
27
(_∼_ : Rel A ℓ₂) -- The relation.
28
: Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
30
isEquivalence : IsEquivalence _≈_
31
-- Reflexivity is expressed in terms of an underlying equality:
33
trans : Transitive _∼_
34
∼-resp-≈ : _∼_ Respects₂ _≈_
36
module Eq = IsEquivalence isEquivalence
39
refl = reflexive Eq.refl
41
record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
45
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
46
_∼_ : Rel Carrier ℓ₂ -- The relation.
47
isPreorder : IsPreorder _≈_ _∼_
49
open IsPreorder isPreorder public
51
------------------------------------------------------------------------
54
-- Equivalence relations are defined in Relation.Binary.Core.
56
record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
61
isEquivalence : IsEquivalence _≈_
63
open IsEquivalence isEquivalence public
65
isPreorder : IsPreorder _≡_ _≈_
67
{ isEquivalence = PropEq.isEquivalence
68
; reflexive = reflexive
70
; ∼-resp-≈ = PropEq.resp₂ _≈_
73
preorder : Preorder c zero ℓ
74
preorder = record { isPreorder = isPreorder }
76
------------------------------------------------------------------------
77
-- Decidable equivalence relations
79
record IsDecEquivalence {a ℓ} {A : Set a}
80
(_≈_ : Rel A ℓ) : Set (a ⊔ ℓ) where
83
isEquivalence : IsEquivalence _≈_
86
open IsEquivalence isEquivalence public
88
record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where
93
isDecEquivalence : IsDecEquivalence _≈_
95
open IsDecEquivalence isDecEquivalence public
98
setoid = record { isEquivalence = isEquivalence }
100
open Setoid setoid public using (preorder)
102
------------------------------------------------------------------------
105
record IsPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
106
(_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
107
Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
109
isPreorder : IsPreorder _≈_ _≤_
110
antisym : Antisymmetric _≈_ _≤_
112
open IsPreorder isPreorder public
113
renaming (∼-resp-≈ to ≤-resp-≈)
115
record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
121
isPartialOrder : IsPartialOrder _≈_ _≤_
123
open IsPartialOrder isPartialOrder public
125
preorder : Preorder c ℓ₁ ℓ₂
126
preorder = record { isPreorder = isPreorder }
128
------------------------------------------------------------------------
129
-- Strict partial orders
131
record IsStrictPartialOrder {a ℓ₁ ℓ₂} {A : Set a}
132
(_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
133
Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
135
isEquivalence : IsEquivalence _≈_
136
irrefl : Irreflexive _≈_ _<_
137
trans : Transitive _<_
138
<-resp-≈ : _<_ Respects₂ _≈_
140
module Eq = IsEquivalence isEquivalence
142
record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
148
isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
150
open IsStrictPartialOrder isStrictPartialOrder public
152
------------------------------------------------------------------------
155
record IsTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
156
(_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
157
Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
159
isPartialOrder : IsPartialOrder _≈_ _≤_
162
open IsPartialOrder isPartialOrder public
164
record TotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
170
isTotalOrder : IsTotalOrder _≈_ _≤_
172
open IsTotalOrder isTotalOrder public
174
poset : Poset c ℓ₁ ℓ₂
175
poset = record { isPartialOrder = isPartialOrder }
177
open Poset poset public using (preorder)
179
------------------------------------------------------------------------
180
-- Decidable total orders
182
record IsDecTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
183
(_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂) :
184
Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
187
isTotalOrder : IsTotalOrder _≈_ _≤_
192
module TO = IsTotalOrder isTotalOrder
193
open TO public hiding (module Eq)
197
isDecEquivalence : IsDecEquivalence _≈_
198
isDecEquivalence = record
199
{ isEquivalence = TO.isEquivalence
203
open IsDecEquivalence isDecEquivalence public
205
record DecTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
211
isDecTotalOrder : IsDecTotalOrder _≈_ _≤_
214
module DTO = IsDecTotalOrder isDecTotalOrder
215
open DTO public hiding (module Eq)
217
totalOrder : TotalOrder c ℓ₁ ℓ₂
218
totalOrder = record { isTotalOrder = isTotalOrder }
220
open TotalOrder totalOrder public using (poset; preorder)
224
decSetoid : DecSetoid c ℓ₁
225
decSetoid = record { isDecEquivalence = DTO.Eq.isDecEquivalence }
227
open DecSetoid decSetoid public
229
------------------------------------------------------------------------
230
-- Strict total orders
232
-- Note that these orders are decidable (see compare).
234
record IsStrictTotalOrder {a ℓ₁ ℓ₂} {A : Set a}
235
(_≈_ : Rel A ℓ₁) (_<_ : Rel A ℓ₂) :
236
Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
238
isEquivalence : IsEquivalence _≈_
239
trans : Transitive _<_
240
compare : Trichotomous _≈_ _<_
241
<-resp-≈ : _<_ Respects₂ _≈_
246
_≟_ = tri⟶dec≈ compare
249
_<?_ = tri⟶dec< compare
251
isDecEquivalence : IsDecEquivalence _≈_
252
isDecEquivalence = record
253
{ isEquivalence = isEquivalence
257
module Eq = IsDecEquivalence isDecEquivalence
259
isStrictPartialOrder : IsStrictPartialOrder _≈_ _<_
260
isStrictPartialOrder = record
261
{ isEquivalence = isEquivalence
262
; irrefl = tri⟶irr <-resp-≈ Eq.sym compare
264
; <-resp-≈ = <-resp-≈
267
open IsStrictPartialOrder isStrictPartialOrder public using (irrefl)
269
record StrictTotalOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
275
isStrictTotalOrder : IsStrictTotalOrder _≈_ _<_
277
open IsStrictTotalOrder isStrictTotalOrder public
280
strictPartialOrder : StrictPartialOrder c ℓ₁ ℓ₂
282
record { isStrictPartialOrder = isStrictPartialOrder }
284
decSetoid : DecSetoid c ℓ₁
285
decSetoid = record { isDecEquivalence = isDecEquivalence }
287
module Eq = DecSetoid decSetoid
added
removed
src/Relation/Binary.agda
