Add Raw bundles to Relation.Binary.* hierarchy

CHANGELOG.md

@@ -110,6 +110,12 @@ New modules
 
 * `Data.List.Relation.Binary.Permutation.Propositional.Properties.WithK`
 
+* Raw bundles for the `Relation.Binary.Bundles` hierarchy:
+  ```agda
+  Relation.Binary.Bundles.Raw
+  ```
+  plus adding `rawX` fields to each of `Relation.Binary.Bundles.X`.
+
 Additions to existing modules
 -----------------------------
 

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

@@ -29,7 +29,7 @@ open import Relation.Unary using (Pred; _∩_)
 
 open import Data.Tree.AVL.Indexed sto as AVL
 open import Data.Tree.AVL.Indexed.Relation.Unary.Any sto as Any
-open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (_≉_; sym; trans)
+open StrictTotalOrder sto renaming (Carrier to Key; trans to <-trans); open Eq using (sym; trans)
 
 open import Relation.Binary.Construct.Add.Extrema.Strict _<_ using ([<]-injective)
 

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

@@ -13,40 +13,26 @@ module Data.Tree.AVL.Map.Membership.Propositional
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Data.Bool.Base using (true; false)
-open import Data.Maybe.Base using (just; nothing; is-just)
-open import Data.Product.Base using (_×_; ∃-syntax; _,_; proj₁; proj₂)
-open import Data.Product.Relation.Binary.Pointwise.NonDependent renaming (Pointwise to _×ᴿ_)
-open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base using (_∘_; _∘′_)
+open import Data.Product.Base using (_×_)
+open import Data.Product.Relation.Binary.Pointwise.NonDependent
+  using ()
+  renaming (Pointwise to _×ᴿ_)
 open import Level using (Level)
 
-open import Relation.Binary.Definitions using (Transitive; Symmetric; _Respectsˡ_)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Construct.Intersection using (_∩_)
-open import Relation.Binary.PropositionalEquality.Core
-  using (_≡_; cong) renaming (refl to ≡-refl; sym to ≡-sym; trans to ≡-trans)
-open import Relation.Nullary using (Reflects; ¬_; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+open StrictTotalOrder strictTotalOrder using (_≈_) renaming (Carrier to Key)
+open import Data.Tree.AVL.Map strictTotalOrder using (Map)
+open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder using (Any)
 
-open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
-open Eq using (_≉_; refl; sym; trans)
-open import Data.Tree.AVL strictTotalOrder using (tree)
-open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
-import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny
-import Data.Tree.AVL.Indexed.Relation.Unary.Any.Properties strictTotalOrder as IAnyₚ
-open import Data.Tree.AVL.Key strictTotalOrder using (⊥⁺<[_]<⊤⁺)
-open import Data.Tree.AVL.Map strictTotalOrder
-open import Data.Tree.AVL.Map.Relation.Unary.Any strictTotalOrder as Mapₚ using (Any)
-open import Data.Tree.AVL.Relation.Unary.Any strictTotalOrder as Any using (tree)
 
 private
   variable
-    v p q : Level
+    v : Level
     V : Set v
     m : Map V
-    k k′ : Key
-    x x′ y y′ : V
     kx : Key × V
 
 infix 4 _≈ₖᵥ_

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

@@ -30,7 +30,7 @@ open import Relation.Nullary using (Reflects; ¬_; yes; no)
 open import Relation.Nullary.Negation using (contradiction)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key) hiding (trans)
-open Eq using (_≉_; refl; sym; trans)
+open Eq using (refl; sym; trans)
 open import Data.Tree.AVL strictTotalOrder using (tree)
 open import Data.Tree.AVL.Indexed strictTotalOrder using (key)
 import Data.Tree.AVL.Indexed.Relation.Unary.Any strictTotalOrder as IAny

src/Relation/Binary/Bundles.agda

@@ -14,6 +14,7 @@ open import Function.Base using (flip)
 open import Level using (Level; suc; _⊔_)
 open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Bundles.Raw
 open import Relation.Binary.Structures -- most of it
 
 ------------------------------------------------------------------------
@@ -29,9 +30,11 @@ record PartialSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
 
   open IsPartialEquivalence isPartialEquivalence public
 
-  infix 4 _≉_
-  _≉_ : Rel Carrier _
-  x ≉ y = ¬ (x ≈ y)
+  rawSetoid : RawSetoid _ _
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    hiding (Carrier; _≈_ )
 
 
 record Setoid c ℓ : Set (suc (c ⊔ ℓ)) where
@@ -94,15 +97,11 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
-  infix 4 _⋦_
-  _⋦_ : Rel Carrier _
-  x ⋦ y = ¬ (x ≲ y)
-
-  infix 4 _≳_
-  _≳_ = flip _≲_
+  rawPreorder : RawPreorder _ _ _
+  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≲_ }
 
-  infix 4 _⋧_
-  _⋧_ = flip _⋦_
+  open RawPreorder rawPreorder public
+    hiding (Carrier; _≈_ ; _≲_)
 
   -- Deprecated.
   infix 4 _∼_
@@ -153,14 +152,17 @@ record Poset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     }
 
   open Preorder preorder public
-    hiding (Carrier; _≈_; _≲_; isPreorder)
+    hiding (Carrier; _≈_; _≲_; isPreorder; _⋦_; _≳_; _⋧_)
     renaming
-    ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_
-    ; ≲-respˡ-≈ to ≤-respˡ-≈
+    ( ≲-respˡ-≈ to ≤-respˡ-≈
     ; ≲-respʳ-≈ to ≤-respʳ-≈
     ; ≲-resp-≈  to ≤-resp-≈
     )
 
+  open RawPreorder rawPreorder public
+    renaming ( _⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
+    hiding (Carrier; _≈_ ; _≲_; _≉_; rawSetoid)
+
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≤_
@@ -211,15 +213,11 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
 
     open Setoid setoid public
 
-  infix 4 _≮_
-  _≮_ : Rel Carrier _
-  x ≮ y = ¬ (x < y)
+  rawStrictPartialOrder : RawStrictPartialOrder _ _ _
+  rawStrictPartialOrder = record { _≈_ = _≈_ ; _<_ = _<_ }
 
-  infix 4 _>_
-  _>_ = flip _<_
-
-  infix 4 _≯_
-  _≯_ = flip _≮_
+  open RawStrictPartialOrder rawStrictPartialOrder public
+    hiding (Carrier; _≈_ ; _<_)
 
 
 record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -390,3 +388,11 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     isApartnessRelation : IsApartnessRelation _≈_ _#_
 
   open IsApartnessRelation isApartnessRelation public
+    hiding (_¬#_)
+
+  rawApartnessRelation : RawApartnessRelation _ _ _
+  rawApartnessRelation = record { _≈_ = _≈_ ; _#_ = _#_ }
+
+  open RawApartnessRelation rawApartnessRelation public
+    hiding (Carrier; _≈_ ; _#_)
+

src/Relation/Binary/Bundles/Raw.agda

@@ -0,0 +1,118 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Raw bundles for homogeneous binary relations
+------------------------------------------------------------------------
+
+-- The contents of this module should be accessed via `Relation.Binary`.
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Binary.Bundles.Raw where
+
+open import Function.Base using (flip)
+open import Level using (Level; suc; _⊔_)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Nullary.Negation.Core using (¬_)
+
+
+------------------------------------------------------------------------
+-- RawSetoid
+------------------------------------------------------------------------
+
+record RawSetoid a ℓ : Set (suc (a ⊔ ℓ)) where
+  infix 4 _≈_
+  field
+    Carrier              : Set a
+    _≈_                  : Rel Carrier ℓ
+
+  infix 4 _≉_
+  _≉_ : Rel Carrier _
+  x ≉ y = ¬ (x ≈ y)
+
+
+------------------------------------------------------------------------
+-- RawPreorder
+------------------------------------------------------------------------
+
+record RawPreorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≲_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
+    _≲_        : Rel Carrier ℓ₂  -- The relation.
+
+  rawSetoid : RawSetoid c ℓ₁
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    using (_≉_)
+
+  infix 4 _⋦_
+  _⋦_ : Rel Carrier _
+  x ⋦ y = ¬ (x ≲ y)
+
+  infix 4 _≳_
+  _≳_ = flip _≲_
+
+  infix 4 _⋧_
+  _⋧_ = flip _⋦_
+
+
+------------------------------------------------------------------------
+-- RawPartialOrders
+------------------------------------------------------------------------
+
+record RawPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _≤_
+  field
+    Carrier        : Set c
+    _≈_            : Rel Carrier ℓ₁
+    _≤_            : Rel Carrier ℓ₂
+
+  rawPreorder : RawPreorder c ℓ₁ ℓ₂
+  rawPreorder = record { _≈_ = _≈_ ; _≲_ = _≤_ }
+
+  open RawPreorder rawPreorder public
+    hiding (Carrier; _≈_; _≲_)
+    renaming (_⋦_ to _≰_; _≳_ to _≥_; _⋧_ to _≱_)
+
+
+record RawStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _<_
+  field
+    Carrier              : Set c
+    _≈_                  : Rel Carrier ℓ₁
+    _<_                  : Rel Carrier ℓ₂
+
+  rawSetoid : RawSetoid c ℓ₁
+  rawSetoid = record { _≈_ = _≈_ }
+
+  open RawSetoid rawSetoid public
+    using (_≉_)
+
+  infix 4 _≮_
+  _≮_ : Rel Carrier _
+  x ≮ y = ¬ (x < y)
+
+  infix 4 _>_
+  _>_ = flip _<_
+
+  infix 4 _≯_
+  _≯_ = flip _≮_
+
+
+------------------------------------------------------------------------
+-- RawApartnessRelation
+------------------------------------------------------------------------
+
+record RawApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _#_
+  field
+    Carrier             : Set c
+    _≈_                 : Rel Carrier ℓ₁
+    _#_                 : Rel Carrier ℓ₂
+
+  infix 4 _¬#_
+  _¬#_ : Rel Carrier _
+  x ¬# y = ¬ (x # y)

src/Relation/Binary/Properties/Poset.agda

@@ -25,7 +25,7 @@ open Poset P renaming (Carrier to A)
 
 import Relation.Binary.Construct.NonStrictToStrict _≈_ _≤_ as ToStrict
 import Relation.Binary.Properties.Preorder preorder as PreorderProperties
-open Eq using (_≉_)
+
 
 ------------------------------------------------------------------------
 -- The _≥_ relation is also a poset.