From d2d7b9fd6bbf42f4080639e8236beb3c045e5dd6 Mon Sep 17 00:00:00 2001 From: James Wood Date: Mon, 21 Aug 2023 16:54:43 +0100 Subject: [PATCH 01/11] [ new ] symmetric core of a binary relation --- CHANGELOG.md | 5 ++ .../Binary/Construct/SymmetricCore.agda | 86 +++++++++++++++++++ src/Relation/Binary/Definitions.agda | 6 ++ 3 files changed, 97 insertions(+) create mode 100644 src/Relation/Binary/Construct/SymmetricCore.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index d454783b0b..b88aba406b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -29,6 +29,11 @@ Deprecated names New modules ----------- +* Symmetric interior of a binary relation + ``` + Relation.Binary.Construct.Interior.Symmetric + ``` + Additions to existing modules ----------------------------- diff --git a/src/Relation/Binary/Construct/SymmetricCore.agda b/src/Relation/Binary/Construct/SymmetricCore.agda new file mode 100644 index 0000000000..cf2e4c71f1 --- /dev/null +++ b/src/Relation/Binary/Construct/SymmetricCore.agda @@ -0,0 +1,86 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Symmetric core of a binary relation +------------------------------------------------------------------------ + +{-# OPTIONS --cubical-compatible --safe #-} + +module Relation.Binary.Construct.SymmetricCore where + +open import Function.Base using (flip) +open import Level +open import Relation.Binary + +private + variable + a b c ℓ r s t : Level + A : Set a + R : Rel A r + S : Rel A s + T : Rel A t + +------------------------------------------------------------------------ +-- Definition + +record SymCore (R : Rel A ℓ) (x y : A) : Set ℓ where + constructor _,_ + field + holds : R x y + sdolh : R y x +open SymCore public + +------------------------------------------------------------------------ +-- Properties + +-- Symmetric cores are symmetric +symmetric : Symmetric (SymCore R) +symmetric (r , r′) = r′ , r + +-- SymCore preserves various properties +reflexive : Reflexive R → Reflexive (SymCore R) +reflexive refl = refl , refl + +transitive′ : + Trans R S T → Trans S R T → Trans (SymCore R) (SymCore S) (SymCore T) +transitive′ trans trans′ (r , r′) (s , s′) = trans r s , trans′ s′ r′ + +transitive : Transitive R → Transitive (SymCore R) +transitive {R = R} tr = transitive′ {R = R} tr tr + +-- The symmetric core of a strict relation is empty +Empty-SymCore : Asymmetric R → Empty (SymCore R) +Empty-SymCore asym (r , r′) = asym r r′ + +-- A reflexive transitive relation _≤_ gives rise to a poset in which the +-- equivalence relation is SymCore _≤_ +record IsProset {a ℓ} {A : Set a} (≤ : Rel A ℓ) : Set (a ⊔ ℓ) where + field + refl : Reflexive ≤ + trans : Transitive ≤ + +record Proset c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≤_ + field + Carrier : Set c + _≤_ : Rel Carrier ℓ + isProset : IsProset _≤_ + +IsProset⇒IsPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → + IsProset ≤ → IsPartialOrder (SymCore ≤) ≤ +IsProset⇒IsPartialOrder {≤ = ≤} isProset = record + { isPreorder = record + { isEquivalence = record + { refl = reflexive refl + ; sym = symmetric + ; trans = transitive trans + } + ; reflexive = holds + ; trans = trans + } + ; antisym = _,_ + } where open IsProset isProset + +Proset⇒Poset : Proset c ℓ → Poset c ℓ ℓ +Proset⇒Poset record { isProset = isProset } = + record { isPartialOrder = IsProset⇒IsPartialOrder isProset } diff --git a/src/Relation/Binary/Definitions.agda b/src/Relation/Binary/Definitions.agda index 887cb7c4a6..55edb7cd5b 100644 --- a/src/Relation/Binary/Definitions.agda +++ b/src/Relation/Binary/Definitions.agda @@ -12,6 +12,7 @@ module Relation.Binary.Definitions where open import Agda.Builtin.Equality using (_≡_) +open import Data.Empty using (⊥) open import Data.Maybe.Base using (Maybe) open import Data.Product.Base using (_×_; ∃-syntax) open import Data.Sum.Base using (_⊎_) @@ -240,6 +241,11 @@ Recomputable _∼_ = ∀ {x y} → .(x ∼ y) → x ∼ y Universal : REL A B ℓ → Set _ Universal _∼_ = ∀ x y → x ∼ y +-- Empty - no elements are related + +Empty : REL A B ℓ → Set _ +Empty _∼_ = ∀ {x y} → x ∼ y → ⊥ + -- Non-emptiness - at least one pair of elements are related. record NonEmpty {A : Set a} {B : Set b} From 9f0d92845507f61f0213c387c4b0782fb7a39a63 Mon Sep 17 00:00:00 2001 From: James Wood Date: Mon, 21 Aug 2023 17:47:14 +0100 Subject: [PATCH 02/11] [ fix ] name clashes --- src/Data/Fin/Subset/Properties.agda | 2 +- src/Relation/Unary/Polymorphic/Properties.agda | 2 +- src/Relation/Unary/Properties.agda | 3 ++- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/Data/Fin/Subset/Properties.agda b/src/Data/Fin/Subset/Properties.agda index 6029b9a78c..d0fc2dd83a 100644 --- a/src/Data/Fin/Subset/Properties.agda +++ b/src/Data/Fin/Subset/Properties.agda @@ -35,7 +35,7 @@ open import Relation.Binary.Structures using (IsPreorder; IsPartialOrder; IsStrictPartialOrder; IsDecStrictPartialOrder) open import Relation.Binary.Bundles using (Preorder; Poset; StrictPartialOrder; DecStrictPartialOrder) -open import Relation.Binary.Definitions as B hiding (Decidable) +open import Relation.Binary.Definitions as B hiding (Decidable; Empty) open import Relation.Binary.PropositionalEquality open import Relation.Nullary.Decidable as Dec using (Dec; yes; no; _⊎-dec_) open import Relation.Nullary.Negation using (contradiction) diff --git a/src/Relation/Unary/Polymorphic/Properties.agda b/src/Relation/Unary/Polymorphic/Properties.agda index 3a59912e2b..91f332433f 100644 --- a/src/Relation/Unary/Polymorphic/Properties.agda +++ b/src/Relation/Unary/Polymorphic/Properties.agda @@ -10,7 +10,7 @@ module Relation.Unary.Polymorphic.Properties where open import Level using (Level) -open import Relation.Binary.Definitions hiding (Decidable; Universal) +open import Relation.Binary.Definitions hiding (Decidable; Universal; Empty) open import Relation.Nullary.Decidable using (yes; no) open import Relation.Unary hiding (∅; U) open import Relation.Unary.Polymorphic diff --git a/src/Relation/Unary/Properties.agda b/src/Relation/Unary/Properties.agda index 520f5e93c8..874869e271 100644 --- a/src/Relation/Unary/Properties.agda +++ b/src/Relation/Unary/Properties.agda @@ -13,7 +13,8 @@ open import Data.Sum.Base using (inj₁; inj₂) open import Data.Unit.Base using (tt) open import Level using (Level) open import Relation.Binary.Core as Binary -open import Relation.Binary.Definitions hiding (Decidable; Universal; Irrelevant) +open import Relation.Binary.Definitions + hiding (Decidable; Universal; Irrelevant; Empty) open import Relation.Binary.PropositionalEquality.Core using (refl) open import Relation.Unary open import Relation.Nullary.Decidable using (yes; no; _⊎-dec_; _×-dec_; ¬?) From bc2b8fb848745aa904b2cbe29345f7e4ea65e2ea Mon Sep 17 00:00:00 2001 From: James Wood Date: Mon, 21 Aug 2023 20:26:48 +0100 Subject: [PATCH 03/11] [ more ] respond to McKinna's comments --- .../Symmetric.agda} | 39 +++++++++++-------- 1 file changed, 22 insertions(+), 17 deletions(-) rename src/Relation/Binary/Construct/{SymmetricCore.agda => Interior/Symmetric.agda} (63%) diff --git a/src/Relation/Binary/Construct/SymmetricCore.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda similarity index 63% rename from src/Relation/Binary/Construct/SymmetricCore.agda rename to src/Relation/Binary/Construct/Interior/Symmetric.agda index cf2e4c71f1..fb1352a6ff 100644 --- a/src/Relation/Binary/Construct/SymmetricCore.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -1,12 +1,12 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Symmetric core of a binary relation +-- Symmetric interior of a binary relation ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} -module Relation.Binary.Construct.SymmetricCore where +module Relation.Binary.Construct.Interior.Symmetric where open import Function.Base using (flip) open import Level @@ -23,37 +23,42 @@ private ------------------------------------------------------------------------ -- Definition -record SymCore (R : Rel A ℓ) (x y : A) : Set ℓ where +record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where constructor _,_ field holds : R x y - sdolh : R y x -open SymCore public + op-holds : R y x +open SymInterior public ------------------------------------------------------------------------ -- Properties --- Symmetric cores are symmetric -symmetric : Symmetric (SymCore R) +-- The symmetric interior is symmetric. +symmetric : Symmetric (SymInterior R) symmetric (r , r′) = r′ , r --- SymCore preserves various properties -reflexive : Reflexive R → Reflexive (SymCore R) +-- The symmetric interior of R is greater than (or equal to) any other symmetric +-- relation contained by R. +unfold : Symmetric S → S ⇒ R → S ⇒ SymInterior R +unfold sym f s = f s , f (sym s) + +-- SymInterior preserves various properties. +reflexive : Reflexive R → Reflexive (SymInterior R) reflexive refl = refl , refl -transitive′ : - Trans R S T → Trans S R T → Trans (SymCore R) (SymCore S) (SymCore T) +transitive′ : Trans R S T → Trans S R T → + Trans (SymInterior R) (SymInterior S) (SymInterior T) transitive′ trans trans′ (r , r′) (s , s′) = trans r s , trans′ s′ r′ -transitive : Transitive R → Transitive (SymCore R) +transitive : Transitive R → Transitive (SymInterior R) transitive {R = R} tr = transitive′ {R = R} tr tr --- The symmetric core of a strict relation is empty -Empty-SymCore : Asymmetric R → Empty (SymCore R) -Empty-SymCore asym (r , r′) = asym r r′ +-- The symmetric interior of a strict relation is empty. +Empty-SymInterior : Asymmetric R → Empty (SymInterior R) +Empty-SymInterior asym (r , r′) = asym r r′ -- A reflexive transitive relation _≤_ gives rise to a poset in which the --- equivalence relation is SymCore _≤_ +-- equivalence relation is SymInterior _≤_. record IsProset {a ℓ} {A : Set a} (≤ : Rel A ℓ) : Set (a ⊔ ℓ) where field refl : Reflexive ≤ @@ -67,7 +72,7 @@ record Proset c ℓ : Set (suc (c ⊔ ℓ)) where isProset : IsProset _≤_ IsProset⇒IsPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → - IsProset ≤ → IsPartialOrder (SymCore ≤) ≤ + IsProset ≤ → IsPartialOrder (SymInterior ≤) ≤ IsProset⇒IsPartialOrder {≤ = ≤} isProset = record { isPreorder = record { isEquivalence = record From 5b8a0a032aa6dc45e5a6ce4e21cb041cfc67c2ed Mon Sep 17 00:00:00 2001 From: James Wood Date: Tue, 22 Aug 2023 11:53:52 +0100 Subject: [PATCH 04/11] =?UTF-8?q?[=20rename=20]=20fields=20to=20lhs?= =?UTF-8?q?=E2=89=A4rhs=20and=20rhs=E2=89=A4lhs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/Relation/Binary/Construct/Interior/Symmetric.agda | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index fb1352a6ff..e81d43d9b1 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -26,8 +26,8 @@ private record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where constructor _,_ field - holds : R x y - op-holds : R y x + lhs≤rhs : R x y + rhs≤lhs : R y x open SymInterior public ------------------------------------------------------------------------ @@ -80,7 +80,7 @@ IsProset⇒IsPartialOrder {≤ = ≤} isProset = record ; sym = symmetric ; trans = transitive trans } - ; reflexive = holds + ; reflexive = lhs≤rhs ; trans = trans } ; antisym = _,_ From 0217f3c2e79e8968d71c98680f21c9b5041bb9a7 Mon Sep 17 00:00:00 2001 From: James Wood Date: Wed, 23 Aug 2023 10:50:08 +0100 Subject: [PATCH 05/11] [ more ] incorporate parts of McKinna's review --- .../Binary/Construct/Interior/Symmetric.agda | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index e81d43d9b1..755f582ded 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -46,12 +46,12 @@ unfold sym f s = f s , f (sym s) reflexive : Reflexive R → Reflexive (SymInterior R) reflexive refl = refl , refl -transitive′ : Trans R S T → Trans S R T → +trans′ : Trans R S T → Trans S R T → Trans (SymInterior R) (SymInterior S) (SymInterior T) -transitive′ trans trans′ (r , r′) (s , s′) = trans r s , trans′ s′ r′ +trans′ trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′ transitive : Transitive R → Transitive (SymInterior R) -transitive {R = R} tr = transitive′ {R = R} tr tr +transitive {R = R} tr = trans′ {R = R} tr tr -- The symmetric interior of a strict relation is empty. Empty-SymInterior : Asymmetric R → Empty (SymInterior R) @@ -59,10 +59,10 @@ Empty-SymInterior asym (r , r′) = asym r r′ -- A reflexive transitive relation _≤_ gives rise to a poset in which the -- equivalence relation is SymInterior _≤_. -record IsProset {a ℓ} {A : Set a} (≤ : Rel A ℓ) : Set (a ⊔ ℓ) where +record IsProset {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) : Set (a ⊔ ℓ) where field - refl : Reflexive ≤ - trans : Transitive ≤ + refl : Reflexive _≤_ + trans : Transitive _≤_ record Proset c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≤_ From 03c8bd5b2db66842c104a479e72ac8d2ff145aa5 Mon Sep 17 00:00:00 2001 From: James Wood Date: Sat, 23 Sep 2023 15:09:55 +0100 Subject: [PATCH 06/11] [ minor ] remove implicit argument application from transitive --- src/Relation/Binary/Construct/Interior/Symmetric.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 755f582ded..9fc58f9ba9 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -51,7 +51,7 @@ trans′ : Trans R S T → Trans S R T → trans′ trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′ transitive : Transitive R → Transitive (SymInterior R) -transitive {R = R} tr = trans′ {R = R} tr tr +transitive tr = trans′ tr tr -- The symmetric interior of a strict relation is empty. Empty-SymInterior : Asymmetric R → Empty (SymInterior R) From 4f7eea6ed5ef8176d4906582593b7e42c00de95c Mon Sep 17 00:00:00 2001 From: James Wood Date: Sat, 23 Sep 2023 15:18:54 +0100 Subject: [PATCH 07/11] [ edit ] pull out isEquivalence and do some renaming --- .../Binary/Construct/Interior/Symmetric.agda | 48 ++++++++++--------- 1 file changed, 26 insertions(+), 22 deletions(-) diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 9fc58f9ba9..5d39232f00 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -33,6 +33,13 @@ open SymInterior public ------------------------------------------------------------------------ -- Properties +-- A reflexive transitive relation _≤_ gives rise to a poset in which the +-- equivalence relation is SymInterior _≤_. +record IsProset {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) : Set (a ⊔ ℓ) where + field + refl : Reflexive _≤_ + trans : Transitive _≤_ + -- The symmetric interior is symmetric. symmetric : Symmetric (SymInterior R) symmetric (r , r′) = r′ , r @@ -46,24 +53,17 @@ unfold sym f s = f s , f (sym s) reflexive : Reflexive R → Reflexive (SymInterior R) reflexive refl = refl , refl -trans′ : Trans R S T → Trans S R T → +trans : Trans R S T → Trans S R T → Trans (SymInterior R) (SymInterior S) (SymInterior T) -trans′ trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′ +trans trans-rs trans-sr (r , r′) (s , s′) = trans-rs r s , trans-sr s′ r′ transitive : Transitive R → Transitive (SymInterior R) -transitive tr = trans′ tr tr +transitive tr = trans tr tr -- The symmetric interior of a strict relation is empty. Empty-SymInterior : Asymmetric R → Empty (SymInterior R) Empty-SymInterior asym (r , r′) = asym r r′ --- A reflexive transitive relation _≤_ gives rise to a poset in which the --- equivalence relation is SymInterior _≤_. -record IsProset {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) : Set (a ⊔ ℓ) where - field - refl : Reflexive _≤_ - trans : Transitive _≤_ - record Proset c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≤_ field @@ -71,21 +71,25 @@ record Proset c ℓ : Set (suc (c ⊔ ℓ)) where _≤_ : Rel Carrier ℓ isProset : IsProset _≤_ -IsProset⇒IsPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → +isEquivalence : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → + IsProset ≤ → IsEquivalence (SymInterior ≤) +isEquivalence isProset = record + { refl = reflexive ≤-refl + ; sym = symmetric + ; trans = transitive ≤-trans + } where open IsProset isProset renaming (refl to ≤-refl; trans to ≤-trans) + +isPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → IsProset ≤ → IsPartialOrder (SymInterior ≤) ≤ -IsProset⇒IsPartialOrder {≤ = ≤} isProset = record +isPartialOrder isProset = record { isPreorder = record - { isEquivalence = record - { refl = reflexive refl - ; sym = symmetric - ; trans = transitive trans - } + { isEquivalence = isEquivalence isProset ; reflexive = lhs≤rhs - ; trans = trans + ; trans = ≤-trans } ; antisym = _,_ - } where open IsProset isProset + } where open IsProset isProset renaming (trans to ≤-trans) -Proset⇒Poset : Proset c ℓ → Poset c ℓ ℓ -Proset⇒Poset record { isProset = isProset } = - record { isPartialOrder = IsProset⇒IsPartialOrder isProset } +poset : Proset c ℓ → Poset c ℓ ℓ +poset record { isProset = isProset } = + record { isPartialOrder = isPartialOrder isProset } From 1e10ef6d6ad0e2098ed57cd82f481dc45fce9a28 Mon Sep 17 00:00:00 2001 From: James Wood Date: Sat, 30 Dec 2023 10:25:59 +0000 Subject: [PATCH 08/11] [ minor ] respond to easy comments --- CHANGELOG.md | 5 +++++ src/Relation/Binary/Construct/Interior/Symmetric.agda | 4 ++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index b88aba406b..01ae444041 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -90,3 +90,8 @@ Additions to existing modules ```agda map : (Char → Char) → String → String ``` + +* Added new definitions in `Relation.Binary.Definitions`: + ```agda + Empty _∼_ = ∀ {x y} → x ∼ y → ⊥ + ``` diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 5d39232f00..46c4239ec4 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -61,8 +61,8 @@ transitive : Transitive R → Transitive (SymInterior R) transitive tr = trans tr tr -- The symmetric interior of a strict relation is empty. -Empty-SymInterior : Asymmetric R → Empty (SymInterior R) -Empty-SymInterior asym (r , r′) = asym r r′ +asymmetric⇒empty : Asymmetric R → Empty (SymInterior R) +asymmetric⇒empty asym (r , r′) = asym r r′ record Proset c ℓ : Set (suc (c ⊔ ℓ)) where infix 4 _≤_ From 0aa58afe6ebf35e35a8bf2dbb0b8fdb84c68fc5b Mon Sep 17 00:00:00 2001 From: James Wood Date: Sat, 30 Dec 2023 10:46:30 +0000 Subject: [PATCH 09/11] [ refactor ] remove IsProset, and move Proset to main hierarchy --- src/Relation/Binary/Bundles.agda | 9 +++++ .../Binary/Construct/Interior/Symmetric.agda | 33 +++++++------------ 2 files changed, 20 insertions(+), 22 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index 641803f8ef..dcc9c4e99f 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -76,6 +76,15 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where -- Preorders ------------------------------------------------------------------------ +record Proset c ℓ : Set (suc (c ⊔ ℓ)) where + infix 4 _≤_ + field + Carrier : Set c + _≤_ : Rel Carrier ℓ + refl : Reflexive _≤_ + trans : Transitive _≤_ + + record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≲_ field diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 46c4239ec4..0fdf56b0ce 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -33,13 +33,6 @@ open SymInterior public ------------------------------------------------------------------------ -- Properties --- A reflexive transitive relation _≤_ gives rise to a poset in which the --- equivalence relation is SymInterior _≤_. -record IsProset {a ℓ} {A : Set a} (_≤_ : Rel A ℓ) : Set (a ⊔ ℓ) where - field - refl : Reflexive _≤_ - trans : Transitive _≤_ - -- The symmetric interior is symmetric. symmetric : Symmetric (SymInterior R) symmetric (r , r′) = r′ , r @@ -64,32 +57,28 @@ transitive tr = trans tr tr asymmetric⇒empty : Asymmetric R → Empty (SymInterior R) asymmetric⇒empty asym (r , r′) = asym r r′ -record Proset c ℓ : Set (suc (c ⊔ ℓ)) where - infix 4 _≤_ - field - Carrier : Set c - _≤_ : Rel Carrier ℓ - isProset : IsProset _≤_ +-- A reflexive transitive relation _≤_ gives rise to a poset in which the +-- equivalence relation is SymInterior _≤_. isEquivalence : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → - IsProset ≤ → IsEquivalence (SymInterior ≤) -isEquivalence isProset = record + Reflexive ≤ → Transitive ≤ → IsEquivalence (SymInterior ≤) +isEquivalence ≤-refl ≤-trans = record { refl = reflexive ≤-refl ; sym = symmetric ; trans = transitive ≤-trans - } where open IsProset isProset renaming (refl to ≤-refl; trans to ≤-trans) + } isPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → - IsProset ≤ → IsPartialOrder (SymInterior ≤) ≤ -isPartialOrder isProset = record + Reflexive ≤ → Transitive ≤ → IsPartialOrder (SymInterior ≤) ≤ +isPartialOrder ≤-refl ≤-trans = record { isPreorder = record - { isEquivalence = isEquivalence isProset + { isEquivalence = isEquivalence ≤-refl ≤-trans ; reflexive = lhs≤rhs ; trans = ≤-trans } ; antisym = _,_ - } where open IsProset isProset renaming (trans to ≤-trans) + } poset : Proset c ℓ → Poset c ℓ ℓ -poset record { isProset = isProset } = - record { isPartialOrder = isPartialOrder isProset } +poset record { _≤_ = ≤; refl = refl; trans = trans } = + record { _≤_ = ≤; isPartialOrder = isPartialOrder refl trans } From dca69cc9cd54c701a5b56e687770367a8fe67ffe Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Sun, 25 Feb 2024 19:24:05 +0800 Subject: [PATCH 10/11] Eliminate Proset --- src/Relation/Binary/Bundles.agda | 9 ------ .../Binary/Construct/Interior/Symmetric.agda | 31 +++++++++---------- 2 files changed, 15 insertions(+), 25 deletions(-) diff --git a/src/Relation/Binary/Bundles.agda b/src/Relation/Binary/Bundles.agda index dcc9c4e99f..641803f8ef 100644 --- a/src/Relation/Binary/Bundles.agda +++ b/src/Relation/Binary/Bundles.agda @@ -76,15 +76,6 @@ record DecSetoid c ℓ : Set (suc (c ⊔ ℓ)) where -- Preorders ------------------------------------------------------------------------ -record Proset c ℓ : Set (suc (c ⊔ ℓ)) where - infix 4 _≤_ - field - Carrier : Set c - _≤_ : Rel Carrier ℓ - refl : Reflexive _≤_ - trans : Transitive _≤_ - - record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 4 _≈_ _≲_ field diff --git a/src/Relation/Binary/Construct/Interior/Symmetric.agda b/src/Relation/Binary/Construct/Interior/Symmetric.agda index 0fdf56b0ce..a954dc99ec 100644 --- a/src/Relation/Binary/Construct/Interior/Symmetric.agda +++ b/src/Relation/Binary/Construct/Interior/Symmetric.agda @@ -16,9 +16,7 @@ private variable a b c ℓ r s t : Level A : Set a - R : Rel A r - S : Rel A s - T : Rel A t + R S T : Rel A r ------------------------------------------------------------------------ -- Definition @@ -28,6 +26,7 @@ record SymInterior (R : Rel A ℓ) (x y : A) : Set ℓ where field lhs≤rhs : R x y rhs≤lhs : R y x + open SymInterior public ------------------------------------------------------------------------ @@ -60,25 +59,25 @@ asymmetric⇒empty asym (r , r′) = asym r r′ -- A reflexive transitive relation _≤_ gives rise to a poset in which the -- equivalence relation is SymInterior _≤_. -isEquivalence : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → - Reflexive ≤ → Transitive ≤ → IsEquivalence (SymInterior ≤) -isEquivalence ≤-refl ≤-trans = record - { refl = reflexive ≤-refl +isEquivalence : Reflexive R → Transitive R → IsEquivalence (SymInterior R) +isEquivalence refl trans = record + { refl = reflexive refl ; sym = symmetric - ; trans = transitive ≤-trans + ; trans = transitive trans } -isPartialOrder : ∀ {a ℓ} {A : Set a} {≤ : Rel A ℓ} → - Reflexive ≤ → Transitive ≤ → IsPartialOrder (SymInterior ≤) ≤ -isPartialOrder ≤-refl ≤-trans = record +isPartialOrder : Reflexive R → Transitive R → IsPartialOrder (SymInterior R) R +isPartialOrder refl trans = record { isPreorder = record - { isEquivalence = isEquivalence ≤-refl ≤-trans + { isEquivalence = isEquivalence refl trans ; reflexive = lhs≤rhs - ; trans = ≤-trans + ; trans = trans } ; antisym = _,_ } -poset : Proset c ℓ → Poset c ℓ ℓ -poset record { _≤_ = ≤; refl = refl; trans = trans } = - record { _≤_ = ≤; isPartialOrder = isPartialOrder refl trans } +poset : ∀ {a} {A : Set a} {R : Rel A ℓ} → Reflexive R → Transitive R → Poset a ℓ ℓ +poset {R = R} refl trans = record + { _≤_ = R + ; isPartialOrder = isPartialOrder refl trans + } From 6d43ff96e9d3f06dcc7ea75e8c7f14c0b053d318 Mon Sep 17 00:00:00 2001 From: MatthewDaggitt Date: Mon, 26 Feb 2024 08:33:48 +0800 Subject: [PATCH 11/11] Fixed CHANGELOG typo --- CHANGELOG.md | 1 - 1 file changed, 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 7b1c4e7eac..8c0cb62b2f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -210,5 +210,4 @@ Additions to existing modules ↭-reflexive : xs ≡ ys → xs ↭ ys ↭-sym : Symmetric (Vector A) _↭_ ↭-trans : Transitive (Vector A) _↭_ ->>>>>>> master ```