Skip to content

Commit fdb4e57

Browse files
authored
Add Raw bundles to Relation.Binary.* hierarchy (#2491)
* add `Raw` bundles for binary relation hierarchy * added `rawX` manifest fields to each `X` bundle * fixed knock-on ambiguity bugs * fixed knock-on ambiguity bugs * tighten `import`s * response to review feedback: refactor in favou rof a single underlying `RawRelation`
1 parent 18f001c commit fdb4e57

File tree

7 files changed

+111
-53
lines changed

7 files changed

+111
-53
lines changed

CHANGELOG.md

+6
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,12 @@ New modules
142142
Data.Refinement.Properties
143143
```
144144

145+
* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
146+
```agda
147+
Relation.Binary.Bundles.Raw
148+
```
149+
plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
150+
145151
Additions to existing modules
146152
-----------------------------
147153

src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@ open import Relation.Unary using (Pred; _∩_)
2929

3030
open import Data.Tree.AVL.Indexed sto as AVL
3131
open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
32-
open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (_≉_; sym; trans)
32+
open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
3333

3434
open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
3535

src/Data/Tree/AVL/Map/Membership/Propositional.agda

+11-25
Original file line numberDiff line numberDiff line change
@@ -13,40 +13,26 @@ module Data.Tree.AVL.Map.Membership.Propositional
1313
{a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
1414
where
1515

16-
open import Data.Bool.Base using (true; false)
17-
open import Data.Maybe.Base using (just; nothing; is-just)
18-
open import Data.Product.Base using (_×_; ∃-syntax; _,_; proj₁; proj₂)
19-
open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
20-
open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
21-
open import Function.Base using (_∘_; _∘′_)
16+
open import Data.Product.Base using (_×_)
17+
open import Data.Product.Relation.Binary.Pointwise.NonDependent
18+
using ()
19+
renaming (Pointwise to _×ᴿ_)
2220
open import Level using (Level)
2321

24-
open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
2522
open import Relation.Binary.Core using (Rel)
26-
open import Relation.Binary.Construct.Intersection using (_∩_)
27-
open import Relation.Binary.PropositionalEquality.Core
28-
using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
29-
open import Relation.Nullary using (Reflects; ¬_; yes; no)
30-
open import Relation.Nullary.Negation using (contradiction)
23+
open import Relation.Binary.PropositionalEquality.Core using (_≡_)
24+
open import Relation.Nullary.Negation.Core using (¬_)
25+
26+
open StrictTotalOrder strictTotalOrder using (_≈_) renaming (Carrier to Key)
27+
open import Data.Tree.AVL.Map strictTotalOrder using (Map)
28+
open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder using (Any)
3129

32-
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
33-
open Eq using (_≉_; refl; sym; trans)
34-
open import Data.Tree.AVL strictTotalOrder using (tree)
35-
open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
36-
import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny
37-
import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties strictTotalOrder as IAnyₚ
38-
open import Data.Tree.AVL.Key strictTotalOrder using (⊥⁺<[_]<⊤⁺)
39-
open import Data.Tree.AVL.Map strictTotalOrder
40-
open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ using (Any)
41-
open import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Any using (tree)
4230

4331
private
4432
variable
45-
v p q : Level
33+
v : Level
4634
V : Set v
4735
m : Map V
48-
k k′ : Key
49-
x x′ y y′ : V
5036
kx : Key × V
5137

5238
infix 4 _≈ₖᵥ_

src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ open import Relation.Nullary using (Reflects; ¬_; yes; no)
3030
open import Relation.Nullary.Negation using (contradiction)
3131

3232
open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
33-
open Eq using (_≉_; refl; sym; trans)
33+
open Eq using (refl; sym; trans)
3434
open import Data.Tree.AVL strictTotalOrder using (tree)
3535
open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
3636
import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny

src/Relation/Binary/Bundles.agda

+31-25
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ open import Function.Base using (flip)
1414
open import Level using (Level; suc; _⊔_)
1515
open import Relation.Nullary.Negation.Core using (¬_)
1616
open import Relation.Binary.Core using (Rel)
17+
open import Relation.Binary.Bundles.Raw
1718
open import Relation.Binary.Structures -- most of it
1819

1920
------------------------------------------------------------------------
@@ -29,9 +30,11 @@ record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
2930

3031
open IsPartialEquivalence isPartialEquivalence public
3132

32-
infix 4 _≉_
33-
_≉_ : Rel Carrier _
34-
x ≉ y = ¬ (x ≈ y)
33+
rawSetoid : RawSetoid _ _
34+
rawSetoid = record { _≈_ = _≈_ }
35+
36+
open RawSetoid rawSetoid public
37+
hiding (Carrier; _≈_ )
3538

3639

3740
record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -94,19 +97,13 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
9497

9598
open Setoid setoid public
9699

97-
infix 4 _⋦_
98-
_⋦_ : Rel Carrier _
99-
x ⋦ y = ¬ (x ≲ y)
100-
101-
infix 4 _≳_
102-
_≳_ = flip _≲_
103-
104-
infix 4 _⋧_
105-
_⋧_ = flip _⋦_
100+
rawRelation : RawRelation _ _ _
101+
rawRelation = record { _≈_ = _≈_ ; _∼_ = _≲_ }
106102

103+
open RawRelation rawRelation public
104+
renaming (_≁_ to _⋦_; _∼ᵒ_ to _≳_; _≁ᵒ_ to _⋧_)
105+
hiding (Carrier; _≈_)
107106
-- Deprecated.
108-
infix 4 _∼_
109-
_∼_ = _≲_
110107
{-# WARNING_ON_USAGE _∼_
111108
"Warning: _∼_ was deprecated in v2.0.
112109
Please use _≲_ instead. "
@@ -183,14 +180,17 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
183180
}
184181

185182
open Preorder preorder public
186-
hiding (Carrier; _≈_; _≲_; isPreorder)
183+
hiding (Carrier; _≈_; _≲_; isPreorder; _⋦_; _≳_; _⋧_)
187184
renaming
188-
( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_
189-
; ≲-respˡ-≈ to ≤-respˡ-≈
185+
( ≲-respˡ-≈ to ≤-respˡ-≈
190186
; ≲-respʳ-≈ to ≤-respʳ-≈
191187
; ≲-resp-≈ to ≤-resp-≈
192188
)
193189

190+
open RawRelation rawRelation public
191+
renaming (_≁_ to _≰_; _∼ᵒ_ to _≥_; _≁ᵒ_ to _≱_)
192+
hiding (Carrier; _≈_ ; _∼_; _≉_; rawSetoid)
193+
194194

195195
record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
196196
infix 4 _≈_ _≤_
@@ -239,15 +239,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
239239

240240
open Setoid setoid public
241241

242-
infix 4 _≮_
243-
_≮_ : Rel Carrier _
244-
x ≮ y = ¬ (x < y)
242+
rawRelation : RawRelation _ _ _
243+
rawRelation = record { _≈_ = _≈_ ; _∼_ = _<_ }
245244

246-
infix 4 _>_
247-
_>_ = flip _<_
248-
249-
infix 4 _≯_
250-
_≯_ = flip _≮_
245+
open RawRelation rawRelation public
246+
renaming (_≁_ to _≮_; _∼ᵒ_ to _>_; _≁ᵒ_ to _≯_)
247+
hiding (Carrier; _≈_ ; _∼_)
251248

252249

253250
record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -418,3 +415,12 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
418415
isApartnessRelation : IsApartnessRelation _≈_ _#_
419416

420417
open IsApartnessRelation isApartnessRelation public
418+
hiding (_¬#_)
419+
420+
rawRelation : RawRelation _ _ _
421+
rawRelation = record { _≈_ = _≈_ ; _∼_ = _#_ }
422+
423+
open RawRelation rawRelation public
424+
renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
425+
hiding (Carrier; _≈_ ; _∼_)
426+

src/Relation/Binary/Bundles/Raw.agda

+60
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
------------------------------------------------------------------------
2+
-- The Agda standard library
3+
--
4+
-- Raw bundles for homogeneous binary relations
5+
------------------------------------------------------------------------
6+
7+
-- The contents of this module should be accessed via `Relation.Binary`.
8+
9+
{-# OPTIONS --cubical-compatible --safe #-}
10+
11+
module Relation.Binary.Bundles.Raw where
12+
13+
open import Function.Base using (flip)
14+
open import Level using (Level; suc; _⊔_)
15+
open import Relation.Binary.Core using (Rel)
16+
open import Relation.Nullary.Negation.Core using (¬_)
17+
18+
19+
------------------------------------------------------------------------
20+
-- RawSetoid
21+
------------------------------------------------------------------------
22+
23+
record RawSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
24+
infix 4 _≈_
25+
field
26+
Carrier : Set a
27+
_≈_ : Rel Carrier ℓ
28+
29+
infix 4 _≉_
30+
_≉_ : Rel Carrier _
31+
x ≉ y = ¬ (x ≈ y)
32+
33+
34+
------------------------------------------------------------------------
35+
-- RawRelation: basis for Relation.Binary.Bundles.*Order
36+
------------------------------------------------------------------------
37+
38+
record RawRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
39+
infix 4 _≈_ _∼_
40+
field
41+
Carrier : Set c
42+
_≈_ : Rel Carrier ℓ₁ -- The underlying equality.
43+
_∼_ : Rel Carrier ℓ₂ -- The underlying relation.
44+
45+
rawSetoid : RawSetoid c ℓ₁
46+
rawSetoid = record { _≈_ = _≈_ }
47+
48+
open RawSetoid rawSetoid public
49+
using (_≉_)
50+
51+
infix 4 _≁_
52+
_≁_ : Rel Carrier _
53+
x ≁ y = ¬ (x ∼ y)
54+
55+
infix 4 _∼ᵒ_
56+
_∼ᵒ_ = flip _∼_
57+
58+
infix 4 _≁ᵒ_
59+
_≁ᵒ_ = flip _≁_
60+

src/Relation/Binary/Properties/Poset.agda

+1-1
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ open Poset P renaming (Carrier to A)
2525

2626
import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
2727
import Relation.Binary.Properties.Preorder preorder as PreorderProperties
28-
open Eq using (_≉_)
28+
2929

3030
------------------------------------------------------------------------
3131
-- The _≥_ relation is also a poset.

0 commit comments

Comments
 (0)