refactor: fix agda#2587

Author: jamesmckinna

CHANGELOG.md

@@ -17,6 +17,10 @@ Non-backwards compatible changes
   significantly faster. However, its reduction behaviour on open terms may have
   changed.
 
+* The definitions of `Algebra.Structures.IsHeytingCommutativeRing` and
+  `Algebra.Structures.IsHeytingCommutativeRing` have been refactored, together
+  with that of `Relation.Binary.Definitions.Tight` on which they depend.
+
 Minor improvements
 ------------------
 

src/Algebra/Apartness/Bundles.agda

@@ -10,7 +10,7 @@ module Algebra.Apartness.Bundles where
 
 open import Level using (_⊔_; suc)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Bundles using (ApartnessRelation)
+open import Relation.Binary.Bundles using (TightApartnessRelation)
 open import Algebra.Core using (Op₁; Op₂)
 open import Algebra.Bundles using (CommutativeRing)
 open import Algebra.Apartness.Structures
@@ -36,8 +36,8 @@ record HeytingCommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ
   commutativeRing : CommutativeRing c ℓ₁
   commutativeRing = record { isCommutativeRing = isCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  tightApartnessRelation : TightApartnessRelation c ℓ₁ ℓ₂
+  tightApartnessRelation = record { isTightApartnessRelation = isTightApartnessRelation }
 
 
 record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
@@ -61,5 +61,5 @@ record HeytingField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
   heytingCommutativeRing : HeytingCommutativeRing c ℓ₁ ℓ₂
   heytingCommutativeRing = record { isHeytingCommutativeRing = isHeytingCommutativeRing }
 
-  apartnessRelation : ApartnessRelation c ℓ₁ ℓ₂
-  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+  open HeytingCommutativeRing heytingCommutativeRing public
+    using (commutativeRing; tightApartnessRelation)

src/Algebra/Apartness/Structures.agda

@@ -17,27 +17,21 @@ module Algebra.Apartness.Structures
   where
 
 open import Level using (_⊔_; suc)
-open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₂)
 open import Algebra.Definitions _≈_ using (Invertible)
 open import Algebra.Structures _≈_ using (IsCommutativeRing)
-open import Relation.Binary.Structures using (IsEquivalence; IsApartnessRelation)
-open import Relation.Binary.Definitions using (Tight)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Binary.Structures
+  using (IsEquivalence; IsApartnessRelation; IsTightApartnessRelation)
 import Relation.Binary.Properties.ApartnessRelation as AR
 
 
 record IsHeytingCommutativeRing : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
-    isCommutativeRing   : IsCommutativeRing _+_ _*_ -_ 0# 1#
-    isApartnessRelation : IsApartnessRelation _≈_ _#_
+    isCommutativeRing        : IsCommutativeRing _+_ _*_ -_ 0# 1#
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
 
   open IsCommutativeRing isCommutativeRing public
-  open IsApartnessRelation isApartnessRelation public
-
-  field
-    #⇒invertible : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
-    invertible⇒# : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+  open IsTightApartnessRelation isTightApartnessRelation public
 
   ¬#-isEquivalence : IsEquivalence _¬#_
   ¬#-isEquivalence = AR.¬#-isEquivalence refl isApartnessRelation
@@ -47,6 +41,10 @@ record IsHeytingField : Set (c ⊔ ℓ₁ ⊔ ℓ₂) where
 
   field
     isHeytingCommutativeRing : IsHeytingCommutativeRing
-    tight                    : Tight _≈_ _#_
 
   open IsHeytingCommutativeRing isHeytingCommutativeRing public
+
+  field
+    #⇒invertible             : ∀ {x y} → x # y → Invertible 1# _*_ (x - y)
+    invertible⇒#             : ∀ {x y} → Invertible 1# _*_ (x - y) → x # y
+

src/Data/Rational/Properties.agda

@@ -1299,15 +1299,14 @@ module _ where
   isHeytingCommutativeRing : IsHeytingCommutativeRing _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingCommutativeRing = record
     { isCommutativeRing = isCommutativeRing
-    ; isApartnessRelation = ≉-isApartnessRelation
-    ; #⇒invertible = #⇒invertible
-    ; invertible⇒# = invertible⇒#
+    ; isTightApartnessRelation = ≉-isTightApartnessRelation
     }
 
   isHeytingField : IsHeytingField _≡_ _≢_ _+_ _*_ -_ 0ℚ 1ℚ
   isHeytingField = record
     { isHeytingCommutativeRing = isHeytingCommutativeRing
-    ; tight = ≉-tight
+    ; #⇒invertible = #⇒invertible
+    ; invertible⇒# = invertible⇒#
     }
 
   heytingCommutativeRing : HeytingCommutativeRing 0ℓ 0ℓ 0ℓ

src/Data/Rational/Unnormalised/Properties.agda

@@ -35,7 +35,7 @@ open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_
 open import Relation.Binary.Bundles
   using (Setoid; DecSetoid; Preorder; TotalPreorder; Poset; TotalOrder; DecTotalOrder; StrictPartialOrder; StrictTotalOrder; DenseLinearOrder)
 open import Relation.Binary.Structures
-  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
+  using (IsEquivalence; IsDecEquivalence; IsApartnessRelation; IsTightApartnessRelation; IsTotalPreorder; IsPreorder; IsPartialOrder; IsTotalOrder; IsDecTotalOrder; IsStrictPartialOrder; IsStrictTotalOrder; IsDenseLinearOrder)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive; Cotransitive; Tight; Decidable; Antisymmetric; Asymmetric; Dense; Total; Trans; Trichotomous; Irreflexive; Irrelevant; _Respectsˡ_; _Respectsʳ_; _Respects₂_; tri≈; tri<; tri>)
 import Relation.Binary.Consequences as BC
@@ -139,8 +139,13 @@ p ≃? q = Dec.map′ *≡* drop-*≡* (↥ p ℤ.* ↧ q ℤ.≟ ↥ q ℤ.* 
   }
 
 ≄-tight : Tight _≃_ _≄_
-proj₁ (≄-tight p q) ¬p≄q = Dec.decidable-stable (p ≃? q) ¬p≄q
-proj₂ (≄-tight p q) p≃q p≄q = p≄q p≃q
+≄-tight p q = Dec.decidable-stable (p ≃? q)
+
+≄-isTightApartnessRelation : IsTightApartnessRelation _≃_ _≄_
+≄-isTightApartnessRelation = record
+  { isApartnessRelation = ≄-isApartnessRelation
+  ; tight = ≄-tight
+  }
 
 ≃-setoid : Setoid 0ℓ 0ℓ
 ≃-setoid = record
@@ -1399,15 +1404,14 @@ nonNeg*nonNeg⇒nonNeg p q = nonNegative
 +-*-isHeytingCommutativeRing : IsHeytingCommutativeRing _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingCommutativeRing = record
   { isCommutativeRing   = +-*-isCommutativeRing
-  ; isApartnessRelation = ≄-isApartnessRelation
-  ; #⇒invertible        = ≄⇒invertible
-  ; invertible⇒#        = invertible⇒≄
+  ; isTightApartnessRelation = ≄-isTightApartnessRelation
   }
 
 +-*-isHeytingField : IsHeytingField _≃_ _≄_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
 +-*-isHeytingField = record
   { isHeytingCommutativeRing = +-*-isHeytingCommutativeRing
-  ; tight                    = ≄-tight
+  ; #⇒invertible        = ≄⇒invertible
+  ; invertible⇒#        = invertible⇒≄
   }
 
 ------------------------------------------------------------------------

src/Relation/Binary/Bundles.agda

@@ -424,3 +424,18 @@ record ApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) w
     renaming (_≁_ to _¬#_; _∼ᵒ_ to _#ᵒ_; _≁ᵒ_ to _¬#ᵒ_)
     hiding (Carrier; _≈_ ; _∼_)
 
+record TightApartnessRelation c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
+  infix 4 _≈_ _#_
+  field
+    Carrier                  : Set c
+    _≈_                      : Rel Carrier ℓ₁
+    _#_                      : Rel Carrier ℓ₂
+    isTightApartnessRelation : IsTightApartnessRelation _≈_ _#_
+
+  open IsTightApartnessRelation isTightApartnessRelation public
+    using (isApartnessRelation; tight)
+
+  apartnessRelation : ApartnessRelation _ _ _
+  apartnessRelation = record { isApartnessRelation = isApartnessRelation }
+
+  open ApartnessRelation apartnessRelation public

src/Relation/Binary/Definitions.agda

@@ -147,7 +147,7 @@ Cotransitive : Rel A ℓ → Set _
 Cotransitive _#_ = ∀ {x y} → x # y → ∀ z → (x # z) ⊎ (z # y)
 
 Tight : Rel A ℓ₁ → Rel A ℓ₂ → Set _
-Tight _≈_ _#_ = ∀ x y → (¬ x # y → x ≈ y) × (x ≈ y → ¬ x # y)
+Tight _≈_ _#_ = ∀ x y → ¬ x # y → x ≈ y
 
 -- Properties of order morphisms, aka order-preserving maps
 

src/Relation/Binary/Properties/DecSetoid.agda

@@ -40,4 +40,4 @@ open SetoidProperties setoid
 ≉-apartnessRelation = record { isApartnessRelation = ≉-isApartnessRelation }
 
 ≉-tight : Tight _≈_ _≉_
-≉-tight x y = decidable-stable (x ≟ y) , ≉-irrefl
+≉-tight x y = decidable-stable (x ≟ y)

src/Relation/Binary/Structures.agda

@@ -328,3 +328,10 @@ record IsApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) whe
 
   _¬#_ : A → A → Set _
   x ¬# y = ¬ (x # y)
+
+record IsTightApartnessRelation (_#_ : Rel A ℓ₂) : Set (a ⊔ ℓ ⊔ ℓ₂) where
+  field
+    isApartnessRelation : IsApartnessRelation _#_
+    tight               : Tight _≈_ _#_
+
+  open IsApartnessRelation isApartnessRelation public