diff --git a/CHANGELOG.md b/CHANGELOG.md index 5649103aee..b691fd1b8d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -850,18 +850,24 @@ Non-backwards compatible changes IO.Instances ``` -### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder` - -* Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its - converse relation could only be discussed *semantically* in terms of `flip _∼_` - in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` - -* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_` - introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties - in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible - has been achieved by redeclaring a deprecated version of the old name in the record. - Therefore, only _declarations_ of `PartialOrder` records will need their field names - updating. +### (Issue #2096) Introduction of flipped and negated relation symbols to bundles in `Relation.Binary.Bundles` + +* Previously, bundles such as `Preorder`, `Poset`, `TotalOrder` etc. did not have the flipped + and negated versions of the operators exposed. In some cases they could obtained by opening the + relevant `Relation.Binary.Properties.X` file but usually they had to be redefined every time. + +* To fix this, these bundles now all export all 4 versions of the operator: normal, converse, negated, + converse-negated. Accordingly they are no longer exported from the corresponding `Properties` file. + +* To make this work for `Preorder`, it was necessary to change the name of the relation symbol. + Previously, the symbol was `_∼_` which is (notationally) symmetric, so that its + converse relation could only be discussed *semantically* in terms of `flip _∼_`. + +* Now, the `Preorder` record field `_∼_` has been renamed to `_≲_`, with `_≳_` + introduced as a definition in `Relation.Binary.Bundles.Preorder`. + Partial backwards compatible has been achieved by redeclaring a deprecated version + of the old symbol in the record. Therefore, only _declarations_ of `PartialOrder` records will + need their field names updating. ### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary` diff --git a/README/Design/Hierarchies.agda b/README/Design/Hierarchies.agda index 09d5504a91..bc9220ba23 100644 --- a/README/Design/Hierarchies.agda +++ b/README/Design/Hierarchies.agda @@ -249,6 +249,43 @@ record Semigroup : Set (suc (a ⊔ ℓ)) where -- differently, as a function with an unknown domain an codomain is -- of little use. +------------------------- +-- Bundle re-exporting -- +------------------------- + +-- In general ensuring that bundles re-export everything in their +-- sub-bundles can get a little tricky. + +-- Imagine we have the following general scenario where bundle A is a +-- direct refinement of bundle C (i.e. the record `IsA` has a `IsC` field) +-- but is also morally a refinement of bundles B and D. + +-- Structures Bundles +-- ========== ======= +-- IsA A +-- / || \ / || \ +-- IsB IsC IsD B C D + +-- The procedure for re-exports in the bundles is as follows: + +-- 1. `open IsA isA public using (IsC, M)` where `M` is everything +-- exported by `IsA` that is not exported by `IsC`. + +-- 2. Construct `c : C` via the `isC` obtained in step 1. + +-- 3. `open C c public hiding (N)` where `N` is the list of fields +-- shared by both `A` and `C`. + +-- 4. Construct `b : B` via the `isB` obtained in step 1. + +-- 5. `open B b public using (O)` where `O` is everything exported +-- by `B` but not exported by `IsA`. + +-- 6. Construct `d : D` via the `isC` obtained in step 1. + +-- 7. `open D d public using (P)` where `P` is everything exported +-- by `D` but not exported by `IsA` + ------------------------------------------------------------------------ -- Other hierarchy modules ------------------------------------------------------------------------ diff --git a/src/Algebra/Lattice/Properties/Semilattice.agda b/src/Algebra/Lattice/Properties/Semilattice.agda index 38554aedfa..7b8135ced7 100644 --- a/src/Algebra/Lattice/Properties/Semilattice.agda +++ b/src/Algebra/Lattice/Properties/Semilattice.agda @@ -27,8 +27,8 @@ import Relation.Binary.Construct.NaturalOrder.Left _≈_ _∧_ poset : Poset c ℓ ℓ poset = LeftNaturalOrder.poset isSemilattice -open Poset poset using (_≤_; isPartialOrder) -open PosetProperties poset using (_≥_; ≥-isPartialOrder) +open Poset poset using (_≤_; _≥_; isPartialOrder) +open PosetProperties poset using (≥-isPartialOrder) ------------------------------------------------------------------------ -- Every algebraic semilattice can be turned into an order-theoretic one. diff --git a/src/Data/Product/Relation/Binary/Lex/Strict.agda b/src/Data/Product/Relation/Binary/Lex/Strict.agda index 42d139893d..39d86602f2 100644 --- a/src/Data/Product/Relation/Binary/Lex/Strict.agda +++ b/src/Data/Product/Relation/Binary/Lex/Strict.agda @@ -240,7 +240,7 @@ module _ {_≈₁_ : Rel A ℓ₁} {_<₁_ : Rel A ℓ₂} (isEquivalence pre₁) (isEquivalence pre₂) ; reflexive = ×-reflexive _≈₁_ _<₁_ _<₂_ (reflexive pre₂) ; trans = ×-transitive {_<₂_ = _<₂_} - (isEquivalence pre₁) (∼-resp-≈ pre₁) + (isEquivalence pre₁) (≲-resp-≈ pre₁) (trans pre₁) (trans pre₂) } where open IsPreorder diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index eb7975f376..641803f8ef 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -43,13 +43,15 @@ record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where isEquivalence : IsEquivalence _≈_ open IsEquivalence isEquivalence public + using (refl; reflexive; isPartialEquivalence) partialSetoid : PartialSetoid c ℓ partialSetoid = record { isPartialEquivalence = isPartialEquivalence } - open PartialSetoid partialSetoid public using (_≉_) + open PartialSetoid partialSetoid public + hiding (Carrier; _≈_; isPartialEquivalence) record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where @@ -60,14 +62,15 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where isDecEquivalence : IsDecEquivalence _≈_ open IsDecEquivalence isDecEquivalence public + using (_≟_; isEquivalence) setoid : Setoid c ℓ setoid = record { isEquivalence = isEquivalence } - open Setoid setoid public using (partialSetoid; _≉_) - + open Setoid setoid public + hiding (Carrier; _≈_; isEquivalence) ------------------------------------------------------------------------ -- Preorders @@ -99,6 +102,9 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≳_ _≳_ = flip _≲_ + infix 4 _⋧_ + _⋧_ = flip _⋦_ + -- Deprecated. infix 4 _∼_ _∼_ = _≲_ @@ -117,14 +123,15 @@ record TotalPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isTotalPreorder : IsTotalPreorder _≈_ _≲_ open IsTotalPreorder isTotalPreorder public - hiding (module Eq) + using (total; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ - preorder = record { isPreorder = isPreorder } + preorder = record + { isPreorder = isPreorder + } open Preorder preorder public - using (module Eq; _≳_; _⋦_) - + hiding (Carrier; _≈_; _≲_; isPreorder) ------------------------------------------------------------------------ -- Partial orders @@ -139,7 +146,7 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isPartialOrder : IsPartialOrder _≈_ _≤_ open IsPartialOrder isPartialOrder public - hiding (module Eq) + using (antisym; isPreorder) preorder : Preorder c ℓ₁ ℓ₂ preorder = record @@ -147,8 +154,13 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Preorder preorder public - using (module Eq) - renaming (_⋦_ to _≰_) + hiding (Carrier; _≈_; _≲_; isPreorder) + renaming + ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_ + ; ≲-respˡ-≈ to ≤-respˡ-≈ + ; ≲-respʳ-≈ to ≤-respʳ-≈ + ; ≲-resp-≈ to ≤-resp-≈ + ) record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where @@ -159,9 +171,10 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _≤_ : Rel Carrier ℓ₂ isDecPartialOrder : IsDecPartialOrder _≈_ _≤_ - private - module DPO = IsDecPartialOrder isDecPartialOrder - open DPO public hiding (module Eq) + private module DPO = IsDecPartialOrder isDecPartialOrder + + open DPO public + using (_≟_; _≤?_; isPartialOrder) poset : Poset c ℓ₁ ℓ₂ poset = record @@ -169,7 +182,7 @@ record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where } open Poset poset public - using (preorder; _≰_) + hiding (Carrier; _≈_; _≤_; isPartialOrder; module Eq) module Eq where decSetoid : DecSetoid c ℓ₁ @@ -203,6 +216,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) _≮_ : Rel Carrier _ x ≮ y = ¬ (x < y) + infix 4 _>_ + _>_ = flip _<_ + + infix 4 _≯_ + _≯_ = flip _≮_ + record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _<_ @@ -212,9 +231,10 @@ record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂ _<_ : Rel Carrier ℓ₂ isDecStrictPartialOrder : IsDecStrictPartialOrder _≈_ _<_ - private - module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder - open DSPO public hiding (module Eq) + private module DSPO = IsDecStrictPartialOrder isDecStrictPartialOrder + + open DSPO public + using (_