Qualified import of PropositionalEquality etc. fixing #2280 (#2293)

* Qualified import of `PropositionalEquality` fixing #2280

* Qualified import of `PropositionalEquality.Core` fixing #2280

* Qualified import of `HeterogeneousEquality.Core` fixing #2280

* simplified imports; fixed `README` link

* simplified imports

Author: jamesmckinna

src/Algebra/Construct/LiftedChoice.agda

@@ -17,7 +17,7 @@ open import Relation.Nullary using (¬_; yes; no)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Product.Base using (_×_; _,_)
 open import Level using (Level; _⊔_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Unary using (Pred)
 
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
@@ -55,8 +55,8 @@ module _ {_≈_ : Rel B ℓ} {_∙_ : Op₂ B}
 
     sel-≡ : Selective _≡_ _◦_
     sel-≡ x y with M.sel (f x) (f y)
-    ... | inj₁ _ = inj₁ P.refl
-    ... | inj₂ _ = inj₂ P.refl
+    ... | inj₁ _ = inj₁ ≡.refl
+    ... | inj₂ _ = inj₂ ≡.refl
 
     distrib : ∀ x y → ((f x) ∙ (f y)) ≈ f (x ◦ y)
     distrib x y with M.sel (f x) (f y)

src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda

@@ -26,7 +26,7 @@ open import Data.Vec.Properties using (lookup-map)
 open import Data.Vec.Relation.Binary.Pointwise.Extensional as PW
   using (Pointwise; ext)
 open import Function.Base using (_∘_; _$_; flip)
-open import Relation.Binary.PropositionalEquality as P using (_≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_)
 import Relation.Binary.Reflection as Reflection
 
 -- Expressions made up of variables and the operations of a boolean
@@ -68,7 +68,7 @@ module Naturality
   (f : Applicative.Morphism A₁ A₂)
   where
 
-  open P.≡-Reasoning
+  open ≡.≡-Reasoning
   open Applicative.Morphism f
   open Semantics A₁ renaming (⟦_⟧ to ⟦_⟧₁)
   open Semantics A₂ renaming (⟦_⟧ to ⟦_⟧₂)
@@ -77,21 +77,21 @@ module Naturality
 
   natural : ∀ {n} (e : Expr n) → op ∘ ⟦ e ⟧₁ ≗ ⟦ e ⟧₂ ∘ Vec.map op
   natural (var x) ρ = begin
-    op (Vec.lookup ρ x)                                            ≡⟨ P.sym $ lookup-map x op ρ ⟩
+    op (Vec.lookup ρ x)                                            ≡⟨ ≡.sym $ lookup-map x op ρ ⟩
     Vec.lookup (Vec.map op ρ) x                                    ∎
   natural (e₁ or e₂) ρ = begin
     op (_∨_ <$>₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ)                       ≡⟨ op-⊛ _ _ ⟩
-    op (_∨_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ _⊛₂_ (op-<$> _ _) P.refl ⟩
-    _∨_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ (λ e₁ e₂ → _∨_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
+    op (_∨_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ ≡.cong₂ _⊛₂_ (op-<$> _ _) ≡.refl ⟩
+    _∨_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ ≡.cong₂ (λ e₁ e₂ → _∨_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
     _∨_ <$>₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ)  ∎
   natural (e₁ and e₂) ρ = begin
     op (_∧_ <$>₁ ⟦ e₁ ⟧₁ ρ ⊛₁ ⟦ e₂ ⟧₁ ρ)                       ≡⟨ op-⊛ _ _ ⟩
-    op (_∧_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ _⊛₂_ (op-<$> _ _) P.refl ⟩
-    _∧_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ P.cong₂ (λ e₁ e₂ → _∧_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
+    op (_∧_ <$>₁ ⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ ≡.cong₂ _⊛₂_ (op-<$> _ _) ≡.refl ⟩
+    _∧_ <$>₂ op (⟦ e₁ ⟧₁ ρ) ⊛₂ op (⟦ e₂ ⟧₁ ρ)                  ≡⟨ ≡.cong₂ (λ e₁ e₂ → _∧_ <$>₂ e₁ ⊛₂ e₂) (natural e₁ ρ) (natural e₂ ρ) ⟩
     _∧_ <$>₂ ⟦ e₁ ⟧₂ (Vec.map op ρ) ⊛₂ ⟦ e₂ ⟧₂ (Vec.map op ρ)  ∎
   natural (not e) ρ = begin
     op (¬_ <$>₁ ⟦ e ⟧₁ ρ)                                      ≡⟨ op-<$> _ _ ⟩
-    ¬_ <$>₂ op (⟦ e ⟧₁ ρ)                                      ≡⟨ P.cong (¬_ <$>₂_) (natural e ρ) ⟩
+    ¬_ <$>₂ op (⟦ e ⟧₁ ρ)                                      ≡⟨ ≡.cong (¬_ <$>₂_) (natural e ρ) ⟩
     ¬_ <$>₂ ⟦ e ⟧₂ (Vec.map op ρ)                              ∎
   natural top ρ = begin
     op (pure₁ ⊤)                                                   ≡⟨ op-pure _ ⟩

src/Algebra/Operations/CommutativeMonoid.agda

@@ -12,7 +12,7 @@ open import Data.Fin.Base using (Fin; zero)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid
   {s₁ s₂} (CM : CommutativeMonoid s₁ s₂)
@@ -58,7 +58,7 @@ suc n ×′ x = x + n ×′ x
 ×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′)
 
 ×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×-cong {u} P.refl x≈x′ = ×-congʳ u x≈x′
+×-cong {u} ≡.refl x≈x′ = ×-congʳ u x≈x′
 
 -- _×_ is homomorphic with respect to _ℕ+_/_+_.
 
@@ -98,7 +98,7 @@ suc n ×′ x = x + n ×′ x
 -- _×′_ preserves equality.
 
 ×′-cong : _×′_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×′-cong {n} {_} {x} {y} P.refl x≈y = begin
+×′-cong {n} {_} {x} {y} ≡.refl x≈y = begin
   n  ×′ x ≈⟨ sym (×≈×′ n x) ⟩
   n  ×  x ≈⟨ ×-congʳ n x≈y ⟩
   n  ×  y ≈⟨ ×≈×′ n y ⟩

src/Algebra/Properties/CommutativeMonoid/Sum.agda

@@ -14,7 +14,7 @@ open import Data.Fin.Permutation as Perm using (Permutation; _⟨$⟩ˡ_; _⟨$
 open import Data.Fin.Patterns using (0F)
 open import Data.Vec.Functional
 open import Function.Base using (_∘_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Nullary.Negation using (contradiction)
 
 module Algebra.Properties.CommutativeMonoid.Sum
@@ -90,9 +90,9 @@ sum-permute {zero}  {suc n} f π = contradiction π (Perm.refute λ())
 sum-permute {suc m} {zero}  f π = contradiction π (Perm.refute λ())
 sum-permute {suc m} {suc n} f π = begin
   sum f                                    ≡⟨⟩
-  f 0F  + sum f/0                          ≡⟨ P.cong (_+ sum f/0) (P.cong f (Perm.inverseʳ π)) ⟨
+  f 0F  + sum f/0                          ≡⟨ ≡.cong (_+ sum f/0) (≡.cong f (Perm.inverseʳ π)) ⟨
   πf π₀ + sum f/0                          ≈⟨ +-congˡ (sum-permute f/0 (Perm.remove π₀ π)) ⟩
-  πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0)  ≡⟨ P.cong (πf π₀ +_) (sum-cong-≗ (P.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟨
+  πf π₀ + sum (rearrange (π/0 ⟨$⟩ʳ_) f/0)  ≡⟨ ≡.cong (πf π₀ +_) (sum-cong-≗ (≡.cong f ∘ Perm.punchIn-permute′ π 0F)) ⟨
   πf π₀ + sum (removeAt πf π₀)             ≈⟨ sym (sum-remove πf) ⟩
   sum πf                                   ∎
   where

src/Algebra/Properties/Monoid/Mult.agda

@@ -9,7 +9,7 @@
 open import Algebra.Bundles using (Monoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
 
@@ -44,7 +44,7 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
 ×-congʳ (suc n) x≈x′ = +-cong x≈x′ (×-congʳ n x≈x′)
 
 ×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×-cong {n} P.refl x≈x′ = ×-congʳ n x≈x′
+×-cong {n} ≡.refl x≈x′ = ×-congʳ n x≈x′
 
 ×-congˡ : ∀ {x} → (_× x) Preserves _≡_ ⟶ _≈_
 ×-congˡ m≡n = ×-cong m≡n refl

src/Algebra/Properties/Monoid/Mult/TCOptimised.agda

@@ -10,7 +10,7 @@
 open import Algebra.Bundles using (Monoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 module Algebra.Properties.Monoid.Mult.TCOptimised
   {a ℓ} (M : Monoid a ℓ) where
@@ -75,7 +75,7 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
 ×-congʳ (suc n@(suc _)) x≈y = +-cong (×-congʳ n x≈y) x≈y
 
 ×-cong : _×_ Preserves₂ _≡_ ⟶ _≈_ ⟶ _≈_
-×-cong {n} P.refl x≈y = ×-congʳ n x≈y
+×-cong {n} ≡.refl x≈y = ×-congʳ n x≈y
 
 ×-assocˡ : ∀ x m n → m × (n × x) ≈ (m ℕ.* n) × x
 ×-assocˡ x m n = begin

src/Algebra/Properties/Monoid/Sum.agda

@@ -13,7 +13,7 @@ open import Data.Fin.Base using (zero; suc)
 open import Data.Unit using (tt)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≗_; _≡_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≗_; _≡_)
 
 module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
 
@@ -61,8 +61,8 @@ sum-cong-≋ {zero}  xs≋ys = refl
 sum-cong-≋ {suc n} xs≋ys = +-cong (xs≋ys zero) (sum-cong-≋ (xs≋ys ∘ suc))
 
 sum-cong-≗ : ∀ {n} → sum {n} Preserves _≗_ ⟶ _≡_
-sum-cong-≗ {zero}  xs≗ys = P.refl
-sum-cong-≗ {suc n} xs≗ys = P.cong₂ _+_ (xs≗ys zero) (sum-cong-≗ (xs≗ys ∘ suc))
+sum-cong-≗ {zero}  xs≗ys = ≡.refl
+sum-cong-≗ {suc n} xs≗ys = ≡.cong₂ _+_ (xs≗ys zero) (sum-cong-≗ (xs≗ys ∘ suc))
 
 sum-replicate : ∀ n {x} → sum (replicate n x) ≈ n × x
 sum-replicate zero    = refl

src/Algebra/Properties/Semiring/Exp.agda

@@ -9,7 +9,7 @@
 open import Algebra
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Data.Nat.Properties as ℕ
 
 module Algebra.Properties.Semiring.Exp

src/Algebra/Solver/Monoid.agda

@@ -22,7 +22,7 @@ open import Data.Vec.Base using (Vec; lookup)
 open import Function.Base using (_∘_; _$_)
 open import Relation.Binary.Definitions using (Decidable)
 
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong)
 import Relation.Binary.Reflection
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec
@@ -128,7 +128,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/Ring.agda

@@ -41,7 +41,7 @@ open import Algebra.Properties.Semiring.Exp semiring
 
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
-import Relation.Binary.PropositionalEquality.Core as PropEq
+import Relation.Binary.PropositionalEquality.Core as ≡
 import Relation.Binary.Reflection as Reflection
 
 open import Data.Nat.Base using (ℕ; suc; zero)
@@ -534,7 +534,7 @@ correct (con c)  ρ = correct-con c ρ
 correct (var i)  ρ = correct-var i ρ
 correct (p :^ k) ρ = begin
   ⟦ normalise p ^N k ⟧N ρ  ≈⟨ ^N-homo (normalise p) k ρ ⟩
-  ⟦ p ⟧↓ ρ ^ k             ≈⟨ correct p ρ ⟨ ^-cong ⟩ PropEq.refl {x = k} ⟩
+  ⟦ p ⟧↓ ρ ^ k             ≈⟨ correct p ρ ⟨ ^-cong ⟩ ≡.refl {x = k} ⟩
   ⟦ p ⟧ ρ ^ k              ∎
 correct (:- p) ρ = begin
   ⟦ -N normalise p ⟧N ρ  ≈⟨ -N‿-homo (normalise p) ρ ⟩