Qualified import of PropositionalEquality etc. fixing #2280

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) ρ ⟩

src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda

@@ -20,13 +20,13 @@ import Algebra.Properties.Semiring.Mult as SemiringMultiplication
 open import Data.Maybe.Base using (Maybe; map)
 open import Data.Nat using (_≟_)
 open import Relation.Binary.Consequences using (dec⇒weaklyDec)
-import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.PropositionalEquality.Core as ≡
 
 open CommutativeSemiring R
 open SemiringMultiplication semiring
 
 private
  dec : ∀ m n → Maybe (m × 1# ≈ n × 1#)
- dec m n = map (λ { P.refl → refl }) (dec⇒weaklyDec _≟_ m n)
+ dec m n = map (λ { ≡.refl → refl }) (dec⇒weaklyDec _≟_ m n)
 
 open import Algebra.Solver.Ring.NaturalCoefficients R dec public