Qualified import of PropositionalEquality.Core fixing agda#2280

Author: jamesmckinna

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 as ≡ using (_≡_)
 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

src/Codata/Guarded/Stream/Properties.agda

@@ -20,7 +20,7 @@ open import Data.Product.Base 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.Core as P using (_≡_; cong; cong₂)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 
@@ -39,7 +39,7 @@ cong-lookup : ∀ {as bs : Stream A} → as ≈ bs → ∀ n → lookup as n ≡
 cong-lookup = B.lookup⁺
 
 cong-take : ∀ n {as bs : Stream A} → as ≈ bs → take n as ≡ take n bs
-cong-take zero    as≈bs = P.refl
+cong-take zero    as≈bs = ≡.refl
 cong-take (suc n) as≈bs = cong₂ _∷_ (as≈bs .head) (cong-take n (as≈bs .tail))
 
 cong-drop : ∀ n {as bs : Stream A} → as ≈ bs → drop n as ≈ drop n bs
@@ -63,7 +63,7 @@ cong-concat ass≈bss = cong-++-concat [] ass≈bss
     cong-++-concat : ∀ (as : List A) {ass bss} → ass ≈ bss → ++-concat as ass ≈ ++-concat as bss
     cong-++-concat [] ass≈bss .head = cong List⁺.head (ass≈bss .head)
     cong-++-concat [] ass≈bss .tail rewrite ass≈bss .head = cong-++-concat _ (ass≈bss .tail)
-    cong-++-concat (a ∷ as) ass≈bss .head = P.refl
+    cong-++-concat (a ∷ as) ass≈bss .head = ≡.refl
     cong-++-concat (a ∷ as) ass≈bss .tail = cong-++-concat as ass≈bss
 
 cong-interleave : {as bs cs ds : Stream A} → as ≈ bs → cs ≈ ds →
@@ -79,11 +79,11 @@ cong-chunksOf n as≈bs .tail = cong-chunksOf n (cong-drop n as≈bs)
 -- Properties of repeat
 
 lookup-repeat : ∀ n (a : A) → lookup (repeat a) n ≡ a
-lookup-repeat zero    a = P.refl
+lookup-repeat zero    a = ≡.refl
 lookup-repeat (suc n) a = lookup-repeat n a
 
 splitAt-repeat : ∀ n (a : A) → splitAt n (repeat a) ≡ (Vec.replicate n a , repeat a)
-splitAt-repeat zero    a = P.refl
+splitAt-repeat zero    a = ≡.refl
 splitAt-repeat (suc n) a = cong (Prod.map₁ (a ∷_)) (splitAt-repeat n a)
 
 take-repeat : ∀ n (a : A) → take n (repeat a) ≡ Vec.replicate n a
@@ -93,28 +93,28 @@ drop-repeat : ∀ n (a : A) → drop n (repeat a) ≡ repeat a
 drop-repeat n a = cong proj₂ (splitAt-repeat n a)
 
 map-repeat : ∀ (f : A → B) a → map f (repeat a) ≈ repeat (f a)
-map-repeat f a .head = P.refl
+map-repeat f a .head = ≡.refl
 map-repeat f a .tail = map-repeat f a
 
 ap-repeat : ∀ (f : A → B) a → ap (repeat f) (repeat a) ≈ repeat (f a)
-ap-repeat f a .head = P.refl
+ap-repeat f a .head = ≡.refl
 ap-repeat f a .tail = ap-repeat f a
 
 ap-repeatˡ : ∀ (f : A → B) as → ap (repeat f) as ≈ map f as
-ap-repeatˡ f as .head = P.refl
+ap-repeatˡ f as .head = ≡.refl
 ap-repeatˡ f as .tail = ap-repeatˡ f (as .tail)
 
 ap-repeatʳ : ∀ (fs : Stream (A → B)) a → ap fs (repeat a) ≈ map (_$′ a) fs
-ap-repeatʳ fs a .head = P.refl
+ap-repeatʳ fs a .head = ≡.refl
 ap-repeatʳ fs a .tail = ap-repeatʳ (fs .tail) a
 
 interleave-repeat : (a : A) → interleave (repeat a) (repeat a) ≈ repeat a
-interleave-repeat a .head = P.refl
+interleave-repeat a .head = ≡.refl
 interleave-repeat a .tail = interleave-repeat a
 
 zipWith-repeat : ∀ (f : A → B → C) a b →
                  zipWith f (repeat a) (repeat b) ≈ repeat (f a b)
-zipWith-repeat f a b .head = P.refl
+zipWith-repeat f a b .head = ≡.refl
 zipWith-repeat f a b .tail = zipWith-repeat f a b
 
 chunksOf-repeat : ∀ n (a : A) → chunksOf n (repeat a) ≈ repeat (Vec.replicate n a)
@@ -125,52 +125,52 @@ chunksOf-repeat n a = begin go where
   go : chunksOf n (repeat a) ≈∞ repeat (Vec.replicate n a)
   go .head = take-repeat n a
   go .tail =
-    chunksOf n (drop n (repeat a)) ≡⟨ P.cong (chunksOf n) (drop-repeat n a) ⟩
+    chunksOf n (drop n (repeat a)) ≡⟨ ≡.cong (chunksOf n) (drop-repeat n a) ⟩
     chunksOf n (repeat a)          ↺⟨ go ⟩
     repeat (Vec.replicate n a)     ∎
 
 ------------------------------------------------------------------------
 -- Properties of map
 
 map-const : (a : A) (bs : Stream B) → map (const a) bs ≈ repeat a
-map-const a bs .head = P.refl
+map-const a bs .head = ≡.refl
 map-const a bs .tail = map-const a (bs .tail)
 
 map-id : (as : Stream A) → map id as ≈ as
-map-id as .head = P.refl
+map-id as .head = ≡.refl
 map-id as .tail = map-id (as .tail)
 
 map-∘ : ∀ (g : B → C) (f : A → B) as → map g (map f as) ≈ map (g ∘′ f) as
-map-∘ g f as .head = P.refl
+map-∘ g f as .head = ≡.refl
 map-∘ g f as .tail = map-∘ g f (as .tail)
 
 map-unfold : ∀ (g : B → C) (f : A → A × B) a →
              map g (unfold f a) ≈ unfold (Prod.map₂ g ∘′ f) a
-map-unfold g f a .head = P.refl
+map-unfold g f a .head = ≡.refl
 map-unfold g f a .tail = map-unfold g f (proj₁ (f a))
 
 map-drop : ∀ (f : A → B) n as → map f (drop n as) ≡ drop n (map f as)
-map-drop f zero    as = P.refl
+map-drop f zero    as = ≡.refl
 map-drop f (suc n) as = map-drop f n (as .tail)
 
 map-zipWith : ∀ (g : C → D) (f : A → B → C) as bs →
               map g (zipWith f as bs) ≈ zipWith (g ∘₂′ f) as bs
-map-zipWith g f as bs .head = P.refl
+map-zipWith g f as bs .head = ≡.refl
 map-zipWith g f as bs .tail = map-zipWith g f (as .tail) (bs .tail)
 
 map-interleave : ∀ (f : A → B) as bs →
                  map f (interleave as bs) ≈ interleave (map f as) (map f bs)
-map-interleave f as bs .head = P.refl
+map-interleave f as bs .head = ≡.refl
 map-interleave f as bs .tail = map-interleave f bs (as .tail)
 
 map-concat : ∀ (f : A → B) ass → map f (concat ass) ≈ concat (map (List⁺.map f) ass)
 map-concat f ass = map-++-concat [] ass
   where
     open Concat
     map-++-concat : ∀ acc ass → map f (++-concat acc ass) ≈ ++-concat (List.map f acc) (map (List⁺.map f) ass)
-    map-++-concat [] ass .head = P.refl
+    map-++-concat [] ass .head = ≡.refl
     map-++-concat [] ass .tail = map-++-concat (ass .head .List⁺.tail) (ass .tail)
-    map-++-concat (a ∷ as) ass .head = P.refl
+    map-++-concat (a ∷ as) ass .head = ≡.refl
     map-++-concat (a ∷ as) ass .tail = map-++-concat as ass
 
 map-cycle : ∀ (f : A → B) as → map f (cycle as) ≈ cycle (List⁺.map f as)
@@ -186,29 +186,29 @@ map-cycle f as = run
 -- Properties of lookup
 
 lookup-drop : ∀ m (as : Stream A) n → lookup (drop m as) n ≡ lookup as (m + n)
-lookup-drop zero    as n = P.refl
+lookup-drop zero    as n = ≡.refl
 lookup-drop (suc m) as n = lookup-drop m (as .tail) n
 
 lookup-map : ∀ n (f : A → B) as → lookup (map f as) n ≡ f (lookup as n)
-lookup-map zero    f as = P.refl
+lookup-map zero    f as = ≡.refl
 lookup-map (suc n) f as = lookup-map n f (as . tail)
 
 lookup-iterate : ∀ n f (x : A) → lookup (iterate f x) n ≡ ℕ.iterate f x n
-lookup-iterate zero    f x = P.refl
+lookup-iterate zero    f x = ≡.refl
 lookup-iterate (suc n) f x = lookup-iterate n f (f x)
 
 lookup-zipWith : ∀ n (f : A → B → C) as bs →
                  lookup (zipWith f as bs) n ≡ f (lookup as n) (lookup bs n)
-lookup-zipWith zero f as bs = P.refl
+lookup-zipWith zero f as bs = ≡.refl
 lookup-zipWith (suc n) f as bs = lookup-zipWith n f (as .tail) (bs .tail)
 
 lookup-unfold : ∀ n (f : A → A × B) a →
                 lookup (unfold f a) n ≡ proj₂ (f (ℕ.iterate (proj₁ ∘′ f) a n))
-lookup-unfold zero    f a = P.refl
+lookup-unfold zero    f a = ≡.refl
 lookup-unfold (suc n) f a = lookup-unfold n f (proj₁ (f a))
 
 lookup-tabulate : ∀ n (f : ℕ → A) → lookup (tabulate f) n ≡ f n
-lookup-tabulate zero f = P.refl
+lookup-tabulate zero f = ≡.refl
 lookup-tabulate (suc n) f = lookup-tabulate n (f ∘′ suc)
 
 lookup-transpose : ∀ n (ass : List (Stream A)) →
@@ -237,81 +237,81 @@ lookup-tails zero    as = B.refl
 lookup-tails (suc n) as = lookup-tails n (as .tail)
 
 lookup-evens : ∀ n (as : Stream A) → lookup (evens as) n ≡ lookup as (n * 2)
-lookup-evens zero    as = P.refl
+lookup-evens zero    as = ≡.refl
 lookup-evens (suc n) as = lookup-evens n (as .tail .tail)
 
 lookup-odds : ∀ n (as : Stream A) → lookup (odds as) n ≡ lookup as (suc (n * 2))
-lookup-odds zero    as = P.refl
+lookup-odds zero    as = ≡.refl
 lookup-odds (suc n) as = lookup-odds n (as .tail .tail)
 
 lookup-interleave-even : ∀ n (as bs : Stream A) →
                          lookup (interleave as bs) (n * 2) ≡ lookup as n
-lookup-interleave-even zero    as bs = P.refl
+lookup-interleave-even zero    as bs = ≡.refl
 lookup-interleave-even (suc n) as bs = lookup-interleave-even n (as .tail) (bs .tail)
 
 lookup-interleave-odd : ∀ n (as bs : Stream A) →
                         lookup (interleave as bs) (suc (n * 2)) ≡ lookup bs n
-lookup-interleave-odd zero    as bs = P.refl
+lookup-interleave-odd zero    as bs = ≡.refl
 lookup-interleave-odd (suc n) as bs = lookup-interleave-odd n (as .tail) (bs .tail)
 
 ------------------------------------------------------------------------
 -- Properties of take
 
 take-iterate : ∀ n f (x : A) → take n (iterate f x) ≡ Vec.iterate f x n
-take-iterate zero    f x = P.refl
+take-iterate zero    f x = ≡.refl
 take-iterate (suc n) f x = cong (x ∷_) (take-iterate n f (f x))
 
 take-zipWith : ∀ n (f : A → B → C) as bs →
                take n (zipWith f as bs) ≡ Vec.zipWith f (take n as) (take n bs)
-take-zipWith zero    f as bs = P.refl
+take-zipWith zero    f as bs = ≡.refl
 take-zipWith (suc n) f as bs =
   cong (f (as .head) (bs .head) ∷_) (take-zipWith n f (as .tail) (bs . tail))
 
 ------------------------------------------------------------------------
 -- Properties of drop
 
 drop-drop : ∀ m n (as : Stream A) → drop n (drop m as) ≡ drop (m + n) as
-drop-drop zero    n as = P.refl
+drop-drop zero    n as = ≡.refl
 drop-drop (suc m) n as = drop-drop m n (as .tail)
 
 drop-zipWith : ∀ n (f : A → B → C) as bs →
                drop n (zipWith f as bs) ≡ zipWith f (drop n as) (drop n bs)
-drop-zipWith zero    f as bs = P.refl
+drop-zipWith zero    f as bs = ≡.refl
 drop-zipWith (suc n) f as bs = drop-zipWith n f (as .tail) (bs .tail)
 
 drop-ap : ∀ n (fs : Stream (A → B)) as →
           drop n (ap fs as) ≡ ap (drop n fs) (drop n as)
-drop-ap zero    fs as = P.refl
+drop-ap zero    fs as = ≡.refl
 drop-ap (suc n) fs as = drop-ap n (fs .tail) (as .tail)
 
 drop-iterate : ∀ n f (x : A) → drop n (iterate f x) ≡ iterate f (ℕ.iterate f x n)
-drop-iterate zero    f x = P.refl
+drop-iterate zero    f x = ≡.refl
 drop-iterate (suc n) f x = drop-iterate n f (f x)
 
 ------------------------------------------------------------------------
 -- Properties of zipWith
 
 zipWith-defn : ∀ (f : A → B → C) as bs →
                zipWith f as bs ≈ (repeat f ⟨ ap ⟩ as ⟨ ap ⟩ bs)
-zipWith-defn f as bs .head = P.refl
+zipWith-defn f as bs .head = ≡.refl
 zipWith-defn f as bs .tail = zipWith-defn f (as .tail) (bs .tail)
 
 zipWith-const : (as : Stream A) (bs : Stream B) →
                 zipWith const as bs ≈ as
-zipWith-const as bs .head = P.refl
+zipWith-const as bs .head = ≡.refl
 zipWith-const as bs .tail = zipWith-const (as .tail) (bs .tail)
 
 zipWith-flip : ∀ (f : A → B → C) as bs →
                zipWith (flip f) as bs ≈ zipWith f bs as
-zipWith-flip f as bs .head = P.refl
+zipWith-flip f as bs .head = ≡.refl
 zipWith-flip f as bs .tail = zipWith-flip f (as .tail) (bs. tail)
 
 ------------------------------------------------------------------------
 -- Properties of interleave
 
 interleave-evens-odds : (as : Stream A) → interleave (evens as) (odds as) ≈ as
-interleave-evens-odds as .head       = P.refl
-interleave-evens-odds as .tail .head = P.refl
+interleave-evens-odds as .head       = ≡.refl
+interleave-evens-odds as .tail .head = ≡.refl
 interleave-evens-odds as .tail .tail = interleave-evens-odds (as .tail .tail)
 
 ------------------------------------------------------------------------

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

@@ -25,7 +25,7 @@ open import Function.Related.TypeIsomorphisms
 open import Level
 open import Relation.Unary using (Pred)
 import Induction.WellFounded as WF
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 import Relation.Binary.Construct.On as On
@@ -149,9 +149,9 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
 
   from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) →
                    from p₁ ≡ from p₂ → p₁ ≡ p₂
-  from-injective (here (inj₁ p))  (here (inj₁ .p)) P.refl = P.refl
+  from-injective (here (inj₁ p))  (here (inj₁ .p)) ≡.refl = ≡.refl
   from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq     =
-    P.cong (here ∘ inj₂) $
+    ≡.cong (here ∘ inj₂) $
     inj₁-injective $
     Injection.injective (↔⇒↣ (↔-sym (Any-⋎P _))) $
     there-injective eq
@@ -166,7 +166,7 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
                            (there-injective eq)
   ... | ()
   from-injective (there {x = _ , xs} p₁) (there p₂) eq =
-    P.cong there $
+    ≡.cong there $
     from-injective p₁ p₂ $
     inj₂-injective $
     Injection.injective (↔⇒↣ (↔-sym (Any-⋎P xs))) $
@@ -188,15 +188,15 @@ Any-merge {P = P} xss = mk↔ₛ′ (proj₁ ∘ to xss) from to∘from (proj₂
 
     step : ∀ p → WF.WfRec (_<′_ on size) InputPred p → InputPred p
     step ([]             , ())      rec
-    step ((x , xs) ∷ xss , here  p) rec = here (inj₁ p) , P.refl
+    step ((x , xs) ∷ xss , here  p) rec = here (inj₁ p) , ≡.refl
     step ((x , xs) ∷ xss , there p) rec
       with Inverse.to (Any-⋎P xs) p
          | Inverse.strictlyInverseʳ (Any-⋎P xs) p
          | index-Any-⋎P xs p
-    ... | inj₁ q | P.refl | _   = here (inj₂ q) , P.refl
-    ... | inj₂ q | P.refl | q≤p =
+    ... | inj₁ q | ≡.refl | _   = here (inj₂ q) , ≡.refl
+    ... | inj₂ q | ≡.refl | q≤p =
       Product.map there
-               (P.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
+               (≡.cong (there ∘ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
                (rec (s≤′s q≤p))
 
   to∘from = λ p → from-injective _ _ (proj₂ (to xss (from p)))