Eliminate many propositional equality imports (#2002)

* Eliminate many propositional equality imports

* Fix merge conflict in Data.Bool.Properties

Co-authored-by: G. Allais <[email protected]>

---------

Co-authored-by: G. Allais <[email protected]>

Author: Taneb

src/Algebra/Construct/LiftedChoice.agda

@@ -16,7 +16,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 as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Unary using (Pred)
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning

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 as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Operations.CommutativeMonoid
   {s₁ s₂} (CM : CommutativeMonoid s₁ s₂)

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

@@ -10,7 +10,6 @@
 open import Algebra.Bundles using (CommutativeMonoid)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Relation.Binary.Core using (_Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
 
 module Algebra.Properties.CommutativeMonoid.Mult.TCOptimised
   {a ℓ} (M : CommutativeMonoid a ℓ) where

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 as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 open import Relation.Nullary.Negation using (contradiction)
 
 module Algebra.Properties.CommutativeMonoid.Sum

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
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Properties.Monoid.Mult {a ℓ} (M : Monoid a ℓ) where
 

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 as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 module Algebra.Properties.Monoid.Mult.TCOptimised
   {a ℓ} (M : Monoid a ℓ) where

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
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Data.Nat.Properties as ℕ
 
 module Algebra.Properties.Semiring.Exp

src/Algebra/Solver/CommutativeMonoid.agda

@@ -27,7 +27,7 @@ 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.Core as P using (_≡_)
 open import Relation.Nullary.Decidable using (Dec)
 
 open CommutativeMonoid M

src/Algebra/Solver/CommutativeMonoid/Example.agda

@@ -8,7 +8,7 @@
 
 module Algebra.Solver.CommutativeMonoid.Example where
 
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 open import Data.Bool.Base using (_∨_)
 open import Data.Bool.Properties using (∨-commutativeMonoid)

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 using (Decidable)
 
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Reflection
 open import Relation.Nullary
 import Relation.Nullary.Decidable as Dec