Qualified import of reasoning modules fixing #2280

src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda

@@ -21,7 +21,7 @@ open CommutativeRing commutativeRing using (ring; *-commutativeMonoid)
 open import Algebra.Properties.Ring ring
   using (-0#≈0#; -‿distribˡ-*; -‿distribʳ-*; -‿anti-homo-+; -‿involutive)
 open import Relation.Binary.Definitions using (Symmetric)
-import Relation.Binary.Reasoning.Setoid as ReasonSetoid
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 open import Algebra.Properties.CommutativeMonoid *-commutativeMonoid
 
 private variable
@@ -50,7 +50,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   helper (x⁻¹ , x⁻¹*x≈1 , x*x⁻¹≈1) (y⁻¹ , y⁻¹*y≈1 , y*y⁻¹≈1)
     = invertibleˡ⇒# (y⁻¹ * x⁻¹ , y⁻¹*x⁻¹*x*y≈1)
     where
-    open ReasonSetoid setoid
+    open ≈-Reasoning setoid
 
     y⁻¹*x⁻¹*x*y≈1 : y⁻¹ * x⁻¹ * (x * y - 0#) ≈ 1#
     y⁻¹*x⁻¹*x*y≈1 = begin
@@ -67,7 +67,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
 #-sym : Symmetric _#_
 #-sym {x} {y} x#y = invertibleˡ⇒# (- x-y⁻¹ , x-y⁻¹*y-x≈1)
   where
-  open ReasonSetoid setoid
+  open ≈-Reasoning setoid
   InvX-Y : Invertible _≈_ 1# _*_ (x - y)
   InvX-Y = #⇒invertible x#y
 
@@ -96,7 +96,7 @@ x#0y#0→xy#0 {x} {y} x#0 y#0 = helper (#⇒invertible x#0) (#⇒invertible y#0)
   helper (x-z⁻¹ , x-z⁻¹*x-z≈1# , x-z*x-z⁻¹≈1#)
     = invertibleˡ⇒# (x-z⁻¹ , x-z⁻¹*y-z≈1)
     where
-    open ReasonSetoid setoid
+    open ≈-Reasoning setoid
 
     x-z⁻¹*y-z≈1 : x-z⁻¹ * (y - z) ≈ 1#
     x-z⁻¹*y-z≈1 = begin

src/Algebra/Construct/LexProduct.agda

@@ -16,7 +16,7 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
 open import Relation.Nullary using (¬_; does; yes; no)
 open import Relation.Nullary.Negation using (contradiction; contradiction₂)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct
   {ℓ₁ ℓ₂ ℓ₃ ℓ₄} (M : Magma ℓ₁ ℓ₂) (N : Magma ℓ₃ ℓ₄)

src/Algebra/Construct/LiftedChoice.agda

@@ -20,7 +20,7 @@ open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary using (Pred)
 
-import Relation.Binary.Reasoning.Setoid as EqReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
@@ -46,7 +46,7 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
 
   private module M = IsSelectiveMagma ∙-isSelectiveMagma
   open M hiding (sel; isMagma)
-  open EqReasoning setoid
+  open ≈-Reasoning setoid
 
   module _ (f : A → B) where
 

src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda

@@ -18,7 +18,7 @@ import Algebra.Lattice.Properties.Lattice as LatticeProperties
 open import Data.Product.Base using (_,_; map)
 open import Relation.Binary.Bundles using (Setoid)
 import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Lattice.Morphism.LatticeMonomorphism
   {a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
@@ -73,7 +73,7 @@ module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where
   setoid : Setoid b ℓ₂
   setoid = record { isEquivalence = isEquivalence }
 
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   ∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_
   ∨-absorbs-∧ x y = injective (begin

src/Algebra/Module/Bundles.agda

@@ -37,7 +37,7 @@ open import Function.Base
 open import Level
 open import Relation.Binary.Core using (Rel)
 open import Relation.Nullary    using (¬_)
-import Relation.Binary.Reasoning.Setoid as SetR
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
@@ -364,7 +364,7 @@ record Semimodule (commutativeSemiring : CommutativeSemiring r ℓr) m ℓm
           ; rawBisemimodule; _≉ᴹ_
           )
 
-  open SetR ≈ᴹ-setoid
+  open ≈-Reasoning ≈ᴹ-setoid
 
   *ₗ-comm : L.Commutative _*ₗ_
   *ₗ-comm x y m = begin

src/Algebra/Module/Consequences.agda

@@ -16,7 +16,7 @@ open import Function.Base using (flip)
 open import Level using (Level)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
-import Relation.Binary.Reasoning.Setoid as Rea
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
@@ -27,7 +27,7 @@ private
 module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where
 
   open Setoid S
-  open Rea S
+  open ≈-Reasoning S
   open Defs _≈ᴬ_
 
   private

src/Algebra/Morphism.agda

@@ -14,7 +14,7 @@ import Algebra.Properties.Group as GroupP
 open import Function.Base
 open import Level
 open import Relation.Binary.Core using (Rel; _Preserves_⟶_)
-import Relation.Binary.Reasoning.Setoid as EqR
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 private
   variable
@@ -137,7 +137,7 @@ module _ {c₁ ℓ₁ c₂ ℓ₂}
     open IsMonoidMorphism mn-homo public
 
     ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
-    ⁻¹-homo x = let open EqR T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
+    ⁻¹-homo x = let open ≈-Reasoning T.setoid in T.uniqueˡ-⁻¹ ⟦ x F.⁻¹ ⟧ ⟦ x ⟧ $ begin
       ⟦ x F.⁻¹ ⟧ T.∙ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (x F.⁻¹) x) ⟩
       ⟦ x F.⁻¹ F.∙ x ⟧     ≈⟨ ⟦⟧-cong (F.inverseˡ x) ⟩
       ⟦ F.ε ⟧              ≈⟨ ε-homo ⟩

src/Algebra/Morphism/Consequences.agda

@@ -13,7 +13,7 @@ open import Algebra.Morphism.Definitions
 open import Data.Product.Base using (_,_)
 open import Function.Base using (id; _∘_)
 open import Function.Definitions
-import Relation.Binary.Reasoning.Setoid as EqR
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------
 -- If f and g are mutually inverse maps between A and B, g is congruent,
@@ -34,7 +34,7 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
     g (f (g x) ∙₂ f (g y)) ≈⟨ g-cong (homo (g x) (g y)) ⟨
     g (f (g x ∙₁ g y))     ≈⟨ invʳ M₂.refl ⟩
     g x ∙₁ g y             ∎
-    where open EqR M₁.setoid
+    where open ≈-Reasoning M₁.setoid
 
   homomorphic₂-inj  : ∀ {f g} → Injective _≈₁_ _≈₂_ f →
                       Inverseˡ _≈₁_ _≈₂_ f g →
@@ -45,4 +45,4 @@ module _ {α α= β β=} (M₁ : Magma α α=) (M₂ : Magma β β=) where
     x ∙₂ y              ≈⟨ M₂.∙-cong (invˡ M₁.refl) (invˡ M₁.refl) ⟨
     f (g x) ∙₂ f (g y)  ≈⟨ homo (g x) (g y) ⟨
     f (g x ∙₁ g y)      ∎)
-    where open EqR M₂.setoid
+    where open ≈-Reasoning M₂.setoid

src/Algebra/Morphism/GroupMonomorphism.agda

@@ -27,7 +27,7 @@ open RawGroup G₂ renaming
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Product.Base using (_,_)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------
 -- Re-export all properties of monoid monomorphisms
@@ -41,7 +41,7 @@ open import Algebra.Morphism.MonoidMonomorphism
 module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁ _∙_
   inverseˡ invˡ x = injective (begin
@@ -72,7 +72,7 @@ module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 module _ (◦-isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂) where
 
   open IsAbelianGroup ◦-isAbelianGroup renaming (∙-cong to ◦-cong; ⁻¹-cong to ⁻¹₂-cong)
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   ⁻¹-distrib-∙ : (∀ x y → (x ◦ y) ⁻¹₂ ≈₂ (x ⁻¹₂) ◦ (y ⁻¹₂)) → (∀ x y → (x ∙ y) ⁻¹₁ ≈₁ (x ⁻¹₁) ∙ (y ⁻¹₁))
   ⁻¹-distrib-∙ ⁻¹-distrib-∙ x y = injective (begin

src/Algebra/Morphism/MagmaMonomorphism.agda

@@ -27,7 +27,7 @@ open import Algebra.Structures
 open import Algebra.Definitions
 open import Data.Product.Base using (map)
 open import Data.Sum.Base using (inj₁; inj₂)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
 
 ------------------------------------------------------------------------
@@ -36,7 +36,7 @@ import Relation.Binary.Morphism.RelMonomorphism isRelMonomorphism as RelMorphism
 module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   cong : Congruent₂ _≈₁_ _∙_
   cong {x} {y} {u} {v} x≈y u≈v = injective (begin

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -25,7 +25,7 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; 
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Product.Base using (map)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------
 -- Re-export all properties of magma monomorphisms
@@ -39,7 +39,7 @@ open import Algebra.Morphism.MagmaMonomorphism
 module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
 
   open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   identityˡ : LeftIdentity _≈₂_ ε₂ _◦_ → LeftIdentity _≈₁_ ε₁ _∙_
   identityˡ idˡ x = injective (begin

src/Algebra/Morphism/RingMonomorphism.agda

@@ -29,7 +29,7 @@ open RawRing R₂ renaming
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Product.Base using (proj₁; proj₂; _,_)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------
 -- Re-export all properties of group and monoid monomorphisms
@@ -83,7 +83,7 @@ module _ (+-isGroup : IsGroup _≈₂_ _⊕_ 0#₂ ⊝_)
 
   open IsGroup +-isGroup hiding (setoid; refl; sym)
   open IsMagma *-isMagma renaming (∙-cong to ◦-cong)
-  open SetoidReasoning setoid
+  open ≈-Reasoning setoid
 
   distribˡ : _DistributesOverˡ_ _≈₂_ _⊛_ _⊕_ → _DistributesOverˡ_ _≈₁_ _*_ _+_
   distribˡ distribˡ x y z = injective (begin

src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda

@@ -8,15 +8,15 @@
 
 open import Algebra using (CommutativeSemigroup)
 open import Data.Product.Base using (_,_)
-import Relation.Binary.Reasoning.Setoid as EqReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Properties.CommutativeSemigroup.Divisibility
   {a ℓ} (CS : CommutativeSemigroup a ℓ)
   where
 
 open CommutativeSemigroup CS
 open import Algebra.Properties.CommutativeSemigroup CS using (x∙yz≈xz∙y; x∙yz≈y∙xz)
-open EqReasoning setoid
+open ≈-Reasoning setoid
 
 ------------------------------------------------------------------------
 -- Re-export the contents of divisibility over semigroups

src/Algebra/Solver/CommutativeMonoid.agda

@@ -22,16 +22,16 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)
 
-import Relation.Binary.Reasoning.Setoid as EqReasoning
+import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 import Relation.Binary.Reflection as Reflection
 import Relation.Nullary.Decidable as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Decidable using (Dec)
 
 open CommutativeMonoid M
-open EqReasoning setoid
+open ≈-Reasoning setoid
 
 private
   variable
@@ -189,7 +189,7 @@ prove′ e₁ e₂ =
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
     R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
+      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
       ⟦ normalise e₂ ⟧⇓ ρ  ∎)
 
 -- This procedure can be combined with from-just.

src/Algebra/Solver/IdempotentCommutativeMonoid.agda

@@ -20,19 +20,19 @@ open import Data.Vec.Base using (Vec; []; _∷_; lookup; replicate)
 
 open import Function.Base using (_∘_)
 
-import Relation.Binary.Reasoning.Setoid  as EqReasoning
+import Relation.Binary.Reasoning.Setoid  as ≈-Reasoning
 import Relation.Binary.Reflection            as Reflection
 import Relation.Nullary.Decidable            as Dec
 import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
 
-open import Relation.Binary.PropositionalEquality as P using (_≡_; decSetoid)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; decSetoid)
 open import Relation.Nullary.Decidable using (Dec)
 
 module Algebra.Solver.IdempotentCommutativeMonoid
   {m₁ m₂} (M : IdempotentCommutativeMonoid m₁ m₂) where
 
 open IdempotentCommutativeMonoid M
-open EqReasoning setoid
+open ≈-Reasoning setoid
 
 private
   variable
@@ -202,7 +202,7 @@ prove′ e₁ e₂ =
   lemma : normalise e₁ ≡ normalise e₂ → ∀ ρ → ⟦ e₁ ⟧ ρ ≈ ⟦ e₂ ⟧ ρ
   lemma eq ρ =
     R.prove ρ e₁ e₂ (begin
-      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ P.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
+      ⟦ normalise e₁ ⟧⇓ ρ  ≡⟨ ≡.cong (λ e → ⟦ e ⟧⇓ ρ) eq ⟩
       ⟦ normalise e₂ ⟧⇓ ρ  ∎)
 
 -- This procedure can be combined with from-just.

src/Codata/Musical/Colist.agda

@@ -31,8 +31,8 @@ open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Bundles using (Poset; Setoid; Preorder)
 open import Relation.Binary.Definitions using (Transitive; Antisymmetric)
 import Relation.Binary.Construct.FromRel as Ind
-import Relation.Binary.Reasoning.Preorder as PreR
-import Relation.Binary.Reasoning.PartialOrder as POR
+import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
+import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning
 open import Relation.Binary.PropositionalEquality as P using (_≡_)
 open import Relation.Binary.Reasoning.Syntax
 open import Relation.Nullary.Reflects using (invert)
@@ -164,7 +164,7 @@ Any-∈ {P = P} = mk↔ₛ′
   antisym (x ∷ p₁) p₂ = x ∷ ♯ antisym (♭ p₁) (tail p₂)
 
 module ⊑-Reasoning {a} {A : Set a} where
-  private module Base = POR (⊑-Poset A)
+  private module Base = ≤-Reasoning (⊑-Poset A)
 
   open Base public hiding (step-<; step-≤)
 
@@ -188,7 +188,7 @@ module ⊑-Reasoning {a} {A : Set a} where
 --      ys ≡⟨ ys≡zs ⟩
 --      zs  ∎
 module ⊆-Reasoning {A : Set a} where
-  private module Base = PreR (⊆-Preorder A)
+  private module Base = ≲-Reasoning (⊆-Preorder A)
 
   open Base public
     hiding (step-≲; step-∼)