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: 2 people

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

src/Algebra/Solver/Ring.agda

@@ -42,7 +42,7 @@ open import Algebra.Properties.Semiring.Exp semiring
 open import Relation.Binary
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Binary.Reasoning.Setoid setoid
-import Relation.Binary.PropositionalEquality as PropEq
+import Relation.Binary.PropositionalEquality.Core as PropEq
 import Relation.Binary.Reflection as Reflection
 
 open import Data.Nat.Base using (ℕ; suc; zero)

src/Algebra/Solver/Ring/NaturalCoefficients.agda

@@ -14,7 +14,7 @@ open import Algebra.Solver.Ring.AlmostCommutativeRing
 open import Data.Nat.Base as ℕ
 open import Data.Product.Base using (module Σ)
 open import Function.Base using (id)
-open import Relation.Binary.PropositionalEquality using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_)
 
 module Algebra.Solver.Ring.NaturalCoefficients
   {r₁ r₂} (R : CommutativeSemiring r₁ r₂)

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

@@ -20,7 +20,7 @@ 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 as P
+import Relation.Binary.PropositionalEquality.Core as P
 
 open CommutativeSemiring R
 open SemiringMultiplication semiring

src/Codata/Guarded/Stream/Properties.agda

@@ -20,7 +20,7 @@ open import Data.Product as Prod using (_×_; _,_; proj₁; proj₂)
 open import Data.Vec.Base as Vec using (Vec; _∷_)
 open import Function.Base using (const; flip; id; _∘′_; _$′_; _⟨_⟩_; _∘₂′_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; cong; cong₂)
 
 private
   variable

src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda

@@ -13,7 +13,8 @@ open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∘_; _on_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as P
 
 private
   variable

src/Codata/Musical/Cofin.agda

@@ -12,7 +12,7 @@ open import Codata.Musical.Notation
 open import Codata.Musical.Conat as Conat using (Coℕ; suc; ∞ℕ)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Fin.Base using (Fin; zero; suc)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
 open import Function.Base using (_∋_)
 
 ------------------------------------------------------------------------

src/Codata/Musical/Colist/Infinite-merge.agda

@@ -23,7 +23,7 @@ open import Function.Inverse as Inv using (_↔_; Inverse; inverse)
 import Function.Related as Related
 open import Function.Related.TypeIsomorphisms
 import Induction.WellFounded as WF
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 import Relation.Binary.Construct.On as On
 
 ------------------------------------------------------------------------

src/Codata/Musical/Conat.agda

@@ -12,7 +12,7 @@ open import Codata.Musical.Notation
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Function.Base using (_∋_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 ------------------------------------------------------------------------
 -- Re-exporting the type and basic operations

src/Codata/Musical/Covec.agda

@@ -18,7 +18,7 @@ open import Data.Product using (_,_)
 open import Function.Base using (_∋_)
 open import Level using (Level)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
   variable

src/Codata/Musical/Stream.agda

@@ -14,7 +14,7 @@ open import Codata.Musical.Colist using (Colist; []; _∷_)
 open import Data.Vec.Base using (Vec; []; _∷_)
 open import Data.Nat.Base using (ℕ; zero; suc)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
 
 private
   variable

src/Codata/Sized/Colist.agda

@@ -27,7 +27,7 @@ open import Codata.Sized.Cowriter as CW using (Cowriter; _∷_)
 open import Codata.Sized.Delay as Delay using (Delay ; now ; later)
 open import Codata.Sized.Stream using (Stream ; _∷_)
 
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 private
   variable

src/Codata/Sized/Colist/Bisimilarity.agda

@@ -16,7 +16,8 @@ open import Data.List.Base using (List; []; _∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Data.List.NonEmpty as List⁺  using (List⁺; _∷_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable

src/Codata/Sized/Colist/Properties.agda

@@ -31,7 +31,7 @@ open import Data.Product as Prod using (_×_; _,_; uncurry)
 open import Data.These.Base as These using (These; this; that; these)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Function.Base
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; [_])
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 private
   variable

src/Codata/Sized/Covec/Bisimilarity.agda

@@ -14,7 +14,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.Conat hiding (_⊔_)
 open import Codata.Sized.Covec
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) (i : Size) :
            ∀ m n (xs : Covec A ∞ m) (ys : Covec B ∞ n) → Set (r ⊔ a ⊔ b) where

src/Codata/Sized/Covec/Properties.agda

@@ -14,7 +14,7 @@ open import Codata.Sized.Conat
 open import Codata.Sized.Covec
 open import Codata.Sized.Covec.Bisimilarity
 open import Function.Base using (id; _∘_)
-open import Relation.Binary.PropositionalEquality as Eq
+open import Relation.Binary.PropositionalEquality.Core as Eq
 
 -- Functor laws
 

src/Codata/Sized/Cowriter/Bisimilarity.agda

@@ -13,7 +13,8 @@ open import Size
 open import Codata.Sized.Thunk
 open import Codata.Sized.Cowriter
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable

src/Codata/Sized/Delay/Bisimilarity.agda

@@ -13,7 +13,7 @@ open import Codata.Sized.Thunk
 open import Codata.Sized.Delay
 open import Level
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 data Bisim {a b r} {A : Set a} {B : Set b} (R : A → B → Set r) i :
            (xs : Delay A ∞) (ys : Delay B ∞) → Set (a ⊔ b ⊔ r) where

src/Codata/Sized/Delay/Properties.agda

@@ -17,7 +17,7 @@ open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)
 open import Codata.Sized.Delay
 open import Codata.Sized.Delay.Bisimilarity
 open import Function.Base using (id; _∘′_)
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
 
 module _ {a} {A : Set a} where
 

src/Codata/Sized/M/Bisimilarity.agda

@@ -17,7 +17,7 @@ open import Data.Container.Relation.Binary.Pointwise using (Pointwise; _,_)
 open import Data.Product using (_,_)
 open import Function.Base using (_∋_)
 open import Relation.Binary
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
 
 data Bisim {s p} (C : Container s p) (i : Size) : Rel (M C ∞) (s ⊔ p) where
   inf : ∀ {t u} → Pointwise C (Thunk^R (Bisim C) i) t u → Bisim C i (inf t) (inf u)

src/Codata/Sized/M/Properties.agda

@@ -18,7 +18,8 @@ import Data.Container.Morphism as Mp
 open import Data.Product as Prod using (_,_)
 open import Data.Product.Properties hiding (map-cong)
 open import Function.Base using (_$′_; _∘′_)
-import Relation.Binary.PropositionalEquality as P
+import Relation.Binary.PropositionalEquality.Core as P
+import Relation.Binary.PropositionalEquality.Properties as P
 
 open import Data.Container.Relation.Binary.Pointwise using (_,_)
 import Data.Container.Relation.Binary.Equality.Setoid as EqSetoid

src/Codata/Sized/Stream/Bisimilarity.agda

@@ -15,7 +15,8 @@ open import Level
 open import Data.List.NonEmpty as List⁺ using (_∷_)
 open import Data.List.Relation.Binary.Pointwise using (Pointwise; []; _∷_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as Eq using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as Eq
 
 private
   variable

src/Codata/Sized/Stream/Properties.agda

@@ -24,7 +24,7 @@ open import Data.Product as Prod using (_,_)
 open import Data.Vec.Base as Vec using (_∷_)
 
 open import Function.Base using (id; _$_; _∘′_; const)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; _≢_)
 
 private
   variable

src/Data/AVL/Indexed/WithK.agda

@@ -7,7 +7,7 @@
 {-# OPTIONS --with-K --safe #-}
 
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; subst)
 
 module Data.AVL.Indexed.WithK
        {k r} (Key : Set k) {_<_ : Rel Key r}

src/Data/AVL/IndexedMap.agda

@@ -8,7 +8,7 @@
 
 open import Data.Product as Prod
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality using (_≡_; cong; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; cong; subst)
 import Data.Tree.AVL.Value
 
 module Data.AVL.IndexedMap

src/Data/Bool.agda

@@ -10,8 +10,7 @@ module Data.Bool where
 
 open import Relation.Nullary
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as PropEq
-  using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 ------------------------------------------------------------------------
 -- The boolean type and some operations

src/Data/Bool/Properties.agda

@@ -22,7 +22,8 @@ open import Function.Equivalence
 open import Induction.WellFounded using (WellFounded; Acc; acc)
 open import Level using (Level; 0ℓ)
 open import Relation.Binary hiding (_⇔_)
-open import Relation.Binary.PropositionalEquality hiding ([_])
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Nullary.Reflects using (ofʸ; ofⁿ)
 open import Relation.Nullary.Decidable.Core using (True; does; proof; yes; no)
 import Relation.Unary as U

src/Data/Char/Properties.agda

@@ -22,8 +22,9 @@ import Relation.Binary.Construct.On as On
 import Relation.Binary.Construct.Subst.Equality as Subst
 import Relation.Binary.Construct.Closure.Reflexive as Refl
 import Relation.Binary.Construct.Closure.Reflexive.Properties as Reflₚ
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; _≢_; refl; cong; sym; trans; subst)
+import Relation.Binary.PropositionalEquality.Properties as PropEq
 
 ------------------------------------------------------------------------
 -- Primitive properties

src/Data/Container/Indexed/WithK.agda

@@ -19,7 +19,7 @@ open import Data.Product as Prod hiding (map)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
 open import Relation.Binary.Indexed.Heterogeneous
 

src/Data/Container/Relation/Binary/Pointwise.agda

@@ -12,7 +12,7 @@ open import Data.Product using (_,_; Σ-syntax; -,_; proj₁; proj₂)
 open import Function
 open import Level using (_⊔_)
 open import Relation.Binary using (REL; _⇒_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; subst; cong)
 
 open import Data.Container.Core using (Container; ⟦_⟧)

src/Data/Container/Relation/Binary/Pointwise/Properties.agda

@@ -14,7 +14,7 @@ open import Data.Container.Relation.Binary.Pointwise
 open import Data.Product using (_,_; Σ-syntax; -,_)
 open import Level using (_⊔_)
 open import Relation.Binary
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality.Core as P
   using (_≡_; subst; cong)
 
 module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where

src/Data/Digit.agda

@@ -21,7 +21,7 @@ open import Data.Nat.DivMod
 open import Data.Nat.Induction
 open import Relation.Nullary.Decidable using (True; does; toWitness)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
 open import Function.Base using (_$_)
 
 ------------------------------------------------------------------------

src/Data/Digit/Properties.agda

@@ -16,7 +16,7 @@ open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
 import Data.Vec.Relation.Unary.Unique.Propositional.Properties as Uniqueₚ
 open import Data.Vec.Relation.Unary.AllPairs using (allPairs?)
 open import Relation.Nullary.Decidable using (True; from-yes; ¬?)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Function.Base using (_∘_)
 
 module Data.Digit.Properties where

src/Data/Fin/Substitution/Example.agda

@@ -14,7 +14,7 @@ open import Data.Fin.Substitution.Lemmas
 open import Data.Nat.Base hiding (_/_)
 open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
-open import Relation.Binary.PropositionalEquality as PropEq
+open import Relation.Binary.PropositionalEquality.Core as PropEq
   using (_≡_; refl; sym; cong; cong₂)
 open PropEq.≡-Reasoning
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive