Add Raw bundles to Relation.Binary.* hierarchy (agda#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`

Author: jamesmckinna

CHANGELOG.md

@@ -142,6 +142,12 @@ New modules
   Data.Refinement.Properties
   ```
 
+* 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,19 +97,13 @@ record Preorder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
 
     open Setoid setoid public
 
-  infix 4 _⋦_
-  _⋦_ : Rel Carrier _
-  x ⋦ y = ¬ (x ≲ y)
-
-  infix 4 _≳_
-  _≳_ = flip _≲_
-
-  infix 4 _⋧_
-  _⋧_ = flip _⋦_
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _≲_ }
 
+  open RawRelation rawRelation public
+    renaming (_≁_ to _⋦_; _∼ᵒ_ to _≳_; _≁ᵒ_ to _⋧_)
+    hiding (Carrier; _≈_)
   -- Deprecated.
-  infix 4 _∼_
-  _∼_ = _≲_
   {-# WARNING_ON_USAGE _∼_
   "Warning: _∼_ was deprecated in v2.0.
   Please use _≲_ instead. "
@@ -183,14 +180,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 RawRelation rawRelation public
+    renaming (_≁_ to _≰_; _∼ᵒ_ to _≥_; _≁ᵒ_ to _≱_)
+    hiding (Carrier; _≈_ ; _∼_; _≉_; rawSetoid)
+
 
 record DecPoset c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   infix 4 _≈_ _≤_
@@ -239,15 +239,12 @@ record StrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂))
 
     open Setoid setoid public
 
-  infix 4 _≮_
-  _≮_ : Rel Carrier _
-  x ≮ y = ¬ (x < y)
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _<_ }
 
-  infix 4 _>_
-  _>_ = flip _<_
-
-  infix 4 _≯_
-  _≯_ = flip _≮_
+  open RawRelation rawRelation public
+    renaming (_≁_ to _≮_; _∼ᵒ_ to _>_; _≁ᵒ_ to _≯_)
+    hiding (Carrier; _≈_ ; _∼_)
 
 
 record DecStrictPartialOrder c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -418,3 +415,12 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     isApartnessRelation : IsApartnessRelation _≈_ _#_
 
   open IsApartnessRelation isApartnessRelation public
+    hiding (_¬#_)
+
+  rawRelation : RawRelation _ _ _
+  rawRelation = record { _≈_ = _≈_ ; _∼_ = _#_ }
+
+  open RawRelation rawRelation public
+    renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
+    hiding (Carrier; _≈_ ; _∼_)
+

src/Relation/Binary/Bundles/Raw.agda

@@ -0,0 +1,60 @@
+------------------------------------------------------------------------
+-- 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)
+
+
+------------------------------------------------------------------------
+-- RawRelation: basis for Relation.Binary.Bundles.*Order
+------------------------------------------------------------------------
+
+record RawRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _∼_
+  field
+    Carrier    : Set c
+    _≈_        : Rel Carrier ℓ₁  -- The underlying equality.
+    _∼_        : Rel Carrier ℓ₂  -- The underlying 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 _≁_
+

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.