Qualified import of HeterogeneousEquality.Core fixing agda#2280

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/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/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/Data/Container/Indexed/WithK.agda

@@ -20,8 +20,8 @@ open import Data.Product.Base
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_; refl)
-open import Relation.Binary.HeterogeneousEquality as H using (_≅_; refl)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
+open import Relation.Binary.HeterogeneousEquality as ≅ using (_≅_; refl)
 open import Relation.Binary.Indexed.Heterogeneous
 
 ------------------------------------------------------------------------
@@ -43,7 +43,7 @@ private
          {xs : ⟦ C ⟧ X o₁} {ys : ⟦ C ⟧ X o₂} → Extensionality r ℓ →
          Eq C X X (λ x₁ x₂ → x₁ ≅ x₂) xs ys → xs ≅ ys
   Eq⇒≅ {xs = c , k} {.c , k′} ext (refl , refl , k≈k′) =
-    H.cong (_,_ c) (ext (λ _ → refl) (λ r → k≈k′ r r refl))
+    ≅.cong (_,_ c) (ext (λ _ → refl) (λ r → k≈k′ r r refl))
 
 setoid : ∀ {i o c r s} {I : Set i} {O : Set o} →
          Container I O c r → IndexedSetoid I s _ → IndexedSetoid O _ _
@@ -122,7 +122,7 @@ module PlainMorphism {i o c r} {I : Set i} {O : Set o} where
     module Y = IndexedSetoid Y
 
     lemma : ∀ {i j} (eq : i ≡ j) {x} →
-            P.subst Y.Carrier eq (f x) Y.≈ f (P.subst X eq x)
+            ≡.subst Y.Carrier eq (f x) Y.≈ f (≡.subst X eq x)
     lemma refl = Y.refl
 
   -- In fact, all natural functions of the right type are container
@@ -135,7 +135,7 @@ module PlainMorphism {i o c r} {I : Set i} {O : Set o} where
                      Eq C₂ X.Carrier X.Carrier X._≈_
                        (proj₁ nt X.Carrier xs) (⟪ m ⟫ X.Carrier {o} xs)
   complete {C₁} {C₂} (nt , nat) = m , (λ X xs → nat X
-    (λ { (r , eq) → P.subst (IndexedSetoid.Carrier X) eq (proj₂ xs r) })
+    (λ { (r , eq) → ≡.subst (IndexedSetoid.Carrier X) eq (proj₂ xs r) })
     (proj₁ xs , (λ r → r , refl)))
     where
 
@@ -167,9 +167,9 @@ module PlainMorphism {i o c r} {I : Set i} {O : Set o} where
     module X = IndexedSetoid X
 
     lemma : ∀ {i j k} (eq₁ : i ≡ j) (eq₂ : j ≡ k) {x} →
-      P.subst X.Carrier (P.trans eq₁ eq₂) x
+      ≡.subst X.Carrier (≡.trans eq₁ eq₂) x
       X.≈
-      P.subst X.Carrier eq₂ (P.subst X.Carrier eq₁ x)
+      ≡.subst X.Carrier eq₂ (≡.subst X.Carrier eq₁ x)
     lemma refl refl = X.refl
 
 ------------------------------------------------------------------------

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

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

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

@@ -17,19 +17,19 @@ open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions
   using (Reflexive; Symmetric; Transitive)
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.PropositionalEquality.Core as P
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; subst; cong)
 
 module _ {s p x r} {X : Set x} (C : Container s p) (R : Rel X r) where
 
   refl : Reflexive R → Reflexive (Pointwise C R)
-  refl R-refl = P.refl , λ p → R-refl
+  refl R-refl = ≡.refl , λ p → R-refl
 
   sym : Symmetric R → Symmetric (Pointwise C R)
-  sym R-sym (P.refl , f) = P.refl , λ p → R-sym (f p)
+  sym R-sym (≡.refl , f) = ≡.refl , λ p → R-sym (f p)
 
   trans : Transitive R → Transitive (Pointwise C R)
-  trans R-trans (P.refl , f) (P.refl , g) = P.refl , λ p → R-trans (f p) (g p)
+  trans R-trans (≡.refl , f) (≡.refl , g) = ≡.refl , λ p → R-trans (f p) (g p)
 
 private
 
@@ -38,4 +38,4 @@ private
 
   Eq⇒≡ : ∀ {s p x} {C : Container s p} {X : Set x} {xs ys : ⟦ C ⟧ X} →
          Extensionality p x → Pointwise C _≡_ xs ys → xs ≡ ys
-  Eq⇒≡ ext (P.refl , f≈f′) = cong -,_ (ext f≈f′)
+  Eq⇒≡ ext (≡.refl , f≈f′) = cong -,_ (ext f≈f′)

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.Core as P using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl)
 open import Function.Base using (_$_)
 
 ------------------------------------------------------------------------
@@ -85,7 +85,7 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
   Pred = λ n → ∃ λ ds → fromDigits ds ≡ n
 
   cons : ∀ {m} (r : Digit base) → Pred m → Pred (toℕ r + m * base)
-  cons r (ds , eq) = (r ∷ ds , P.cong (λ i → toℕ r + i * base) eq)
+  cons r (ds , eq) = (r ∷ ds , ≡.cong (λ i → toℕ r + i * base) eq)
 
   open ≤-Reasoning
   open +-*-Solver
@@ -104,7 +104,7 @@ toDigits base@(suc (suc k)) n = <′-rec Pred helper n
 
   helper : ∀ n → <′-Rec Pred n → Pred n
   helper n                       rec with n divMod base
-  ... | result zero    r eq = ([ r ] , P.sym eq)
+  ... | result zero    r eq = ([ r ] , ≡.sym eq)
   ... | result (suc x) r refl = cons r (rec (lem x k (toℕ r)))
 
 ------------------------------------------------------------------------

src/Data/Fin/Substitution/Example.agda

@@ -22,7 +22,7 @@ open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
 open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; refl; sym; cong; cong₂)
-open PropEq.≡-Reasoning
+open ≡.≡-Reasoning
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_)
 

src/Data/Graph/Acyclic.agda

@@ -27,7 +27,7 @@ open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Function.Base using (_$_; _∘′_; _∘_; id)
 open import Relation.Nullary
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 ------------------------------------------------------------------------
 -- A lemma
@@ -186,7 +186,7 @@ private
 
   test-nodes : nodes example ≡ (# 0 , 0) ∷ (# 1 , 1) ∷ (# 2 , 2) ∷
                                (# 3 , 3) ∷ (# 4 , 4) ∷ []
-  test-nodes = P.refl
+  test-nodes = ≡.refl
 
 
 module _ {ℓ e} {N : Set ℓ} {E : Set e} where
@@ -213,7 +213,7 @@ private
 
   test-edges : edges example ≡ (# 1 , 10 , # 1) ∷ (# 1 , 11 , # 1) ∷
                                (# 2 , 12 , # 0) ∷ []
-  test-edges = P.refl
+  test-edges = ≡.refl
 
 -- The successors of a given node i (edge label × node number relative
 -- to i).
@@ -225,7 +225,7 @@ sucs g i = successors $ head (g [ i ])
 private
 
   test-sucs : sucs example (# 1) ≡ (10 , # 1) ∷ (11 , # 1) ∷ []
-  test-sucs = P.refl
+  test-sucs = ≡.refl
 
 -- The predecessors of a given node i (node number relative to i ×
 -- edge label).
@@ -238,13 +238,13 @@ preds (c & g) (suc i) =
             (List.map (Prod.map suc id) $ preds g i)
   where
   p : ∀ {e} {E : Set e} {n} (i : Fin n) → E × Fin n → Maybe (Fin′ (suc i) × E)
-  p i (e , j) = Maybe.map (λ{ P.refl → zero , e }) (decToMaybe (i ≟ j))
+  p i (e , j) = Maybe.map (λ{ ≡.refl → zero , e }) (decToMaybe (i ≟ j))
 
 private
 
   test-preds : preds example (# 3) ≡
                (# 1 , 10) ∷ (# 1 , 11) ∷ (# 2 , 12) ∷ []
-  test-preds = P.refl
+  test-preds = ≡.refl
 
 ------------------------------------------------------------------------
 -- Operations
@@ -272,7 +272,7 @@ private
                  context (# 3 , 3) [] &
                  context (# 4 , 4) [] &
                  ∅)
-  test-number = P.refl
+  test-number = ≡.refl
 
 -- Reverses all the edges in the graph.
 
@@ -290,7 +290,7 @@ reverse {N = N} {E} g =
 private
 
   test-reverse : reverse (reverse example) ≡ example
-  test-reverse = P.refl
+  test-reverse = ≡.refl
 
 ------------------------------------------------------------------------
 -- Views
@@ -330,4 +330,4 @@ private
                     node 3 [] ∷
                     node 4 [] ∷
                     []
-  test-toForest = P.refl
+  test-toForest = ≡.refl

src/Data/List/Membership/Propositional/Properties/Core.agda

@@ -20,7 +20,7 @@ open import Data.List.Membership.Propositional
 open import Data.Product.Base as Product
   using (_,_; proj₁; proj₂; uncurry′; ∃; _×_)
 open import Level using (Level)
-open import Relation.Binary.PropositionalEquality.Core as P
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl)
 open import Relation.Unary using (Pred; _⊆_)
 
@@ -37,8 +37,8 @@ map∘find : ∀ {P : Pred A p} {xs}
            {f : _≡_ (proj₁ p′) ⊆ P} →
            f refl ≡ proj₂ (proj₂ p′) →
            Any.map f (proj₁ (proj₂ p′)) ≡ p
-map∘find (here  p) hyp = P.cong here  hyp
-map∘find (there p) hyp = P.cong there (map∘find p hyp)
+map∘find (here  p) hyp = ≡.cong here  hyp
+map∘find (there p) hyp = ≡.cong there (map∘find p hyp)
 
 find∘map : ∀ {P : Pred A p} {Q : Pred A q}
            {xs : List A} (p : Any P xs) (f : P ⊆ Q) →
@@ -61,13 +61,13 @@ find-∈ (there x∈xs) rewrite find-∈ x∈xs = refl
 lose∘find : ∀ {P : Pred A p} {xs : List A}
             (p : Any P xs) →
             uncurry′ lose (proj₂ (find p)) ≡ p
-lose∘find p = map∘find p P.refl
+lose∘find p = map∘find p ≡.refl
 
 find∘lose : ∀ (P : Pred A p) {x xs}
             (x∈xs : x ∈ xs) (pp : P x) →
             find {P = P} (lose x∈xs pp) ≡ (x , x∈xs , pp)
 find∘lose P x∈xs p
-  rewrite find∘map x∈xs (flip (P.subst P) p)
+  rewrite find∘map x∈xs (flip (≡.subst P) p)
         | find-∈ x∈xs
         = refl