Qualified import of PropositionalEquality fixing agda#2280

Author: jamesmckinna

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/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/Codata/Musical/Colist.agda

@@ -33,7 +33,7 @@ open import Relation.Binary.Definitions using (Transitive; Antisymmetric)
 import Relation.Binary.Construct.FromRel as Ind
 import Relation.Binary.Reasoning.Preorder as ≲-Reasoning
 import Relation.Binary.Reasoning.PartialOrder as ≤-Reasoning
-open import Relation.Binary.PropositionalEquality as P using (_≡_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_)
 open import Relation.Binary.Reasoning.Syntax
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
@@ -107,23 +107,23 @@ Any-∈ {P = P} = mk↔ₛ′
   from∘to
   where
   to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
-  to (here  p) = _ , here P.refl , p
+  to (here  p) = _ , here ≡.refl , p
   to (there p) = Product.map id (Product.map there id) (to p)
 
   from : ∀ {x xs} → x ∈ xs → P x → Any P xs
-  from (here P.refl) p = here p
+  from (here ≡.refl) p = here p
   from (there x∈xs)  p = there (from x∈xs p)
 
   to∘from : ∀ {x xs} (x∈xs : x ∈ xs) (p : P x) →
             to (from x∈xs p) ≡ (x , x∈xs , p)
-  to∘from (here P.refl) p = P.refl
+  to∘from (here ≡.refl) p = ≡.refl
   to∘from (there x∈xs)  p =
-    P.cong (Product.map id (Product.map there id)) (to∘from x∈xs p)
+    ≡.cong (Product.map id (Product.map there id)) (to∘from x∈xs p)
 
   from∘to : ∀ {xs} (p : Any P xs) →
             let (x , x∈xs , px) = to p in from x∈xs px ≡ p
-  from∘to (here _)  = P.refl
-  from∘to (there p) = P.cong there (from∘to p)
+  from∘to (here _)  = ≡.refl
+  from∘to (there p) = ≡.cong there (from∘to p)
 
 -- Prefixes are subsets.
 
@@ -176,8 +176,8 @@ module ⊑-Reasoning {a} {A : Set a} where
 
 ⊆-Preorder : ∀ {ℓ} → Set ℓ → Preorder _ _ _
 ⊆-Preorder A = Ind.preorder (setoid A) _∈_
-                 (λ xs≈ys → ⊑⇒⊆ (⊑P.reflexive xs≈ys))
-  where module ⊑P = Poset (⊑-Poset A)
+                 (λ xs≈ys → ⊑⇒⊆ (⊑A.reflexive xs≈ys))
+  where module ⊑A = Poset (⊑-Poset A)
 
 -- Example uses:
 --
@@ -220,7 +220,7 @@ infixr 5 _∷_
 module Finite-injective where
 
  ∷-injective : ∀ {x : A} {xs p q} → (Finite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
- ∷-injective P.refl = P.refl
+ ∷-injective ≡.refl = ≡.refl
 
 -- Infinite xs means that xs has infinite length.
 
@@ -230,7 +230,7 @@ data Infinite {A : Set a} : Colist A → Set a where
 module Infinite-injective where
 
  ∷-injective : ∀ {x : A} {xs p q} → (Infinite (x ∷ xs) ∋ x ∷ p) ≡ x ∷ q → p ≡ q
- ∷-injective P.refl = P.refl
+ ∷-injective ≡.refl = ≡.refl
 
 -- Colists which are not finite are infinite.
 

src/Codata/Musical/Colist/Relation/Unary/Any/Properties.agda

@@ -21,7 +21,7 @@ open import Function.Base using (_∋_; _∘_)
 open import Function.Bundles
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality as ≡
   using (_≡_; refl; cong)
 open import Relation.Unary using (Pred)
 
@@ -66,15 +66,15 @@ Any-cong {A = A} {P} {Q} {xs} {ys} P↔Q xs≈ys =
 
   to∘from : ∀ {xs ys} (xs≈ys : xs ≈ ys) (q : Any Q ys) →
             to xs≈ys (from xs≈ys q) ≡ q
-  to∘from (x ∷ xs≈) (there q) = P.cong there (to∘from (♭ xs≈) q)
+  to∘from (x ∷ xs≈) (there q) = ≡.cong there (to∘from (♭ xs≈) q)
   to∘from (x ∷ xs≈) (here qx) =
-    P.cong here (Inverse.strictlyInverseˡ P↔Q qx)
+    ≡.cong here (Inverse.strictlyInverseˡ P↔Q qx)
 
   from∘to : ∀ {xs ys} (xs≈ys : xs ≈ ys) (p : Any P xs) →
             from xs≈ys (to xs≈ys p) ≡ p
-  from∘to (x ∷ xs≈) (there p) = P.cong there (from∘to (♭ xs≈) p)
+  from∘to (x ∷ xs≈) (there p) = ≡.cong there (from∘to (♭ xs≈) p)
   from∘to (x ∷ xs≈) (here px) =
-    P.cong here (Inverse.strictlyInverseʳ P↔Q px)
+    ≡.cong here (Inverse.strictlyInverseʳ P↔Q px)
 
 ------------------------------------------------------------------------
 -- map
@@ -164,7 +164,7 @@ lookup-index (there p) = lookup-index p
 index-Any-resp : ∀ {f : ∀ {x} → P x → Q x} {xs ys}
                  (xs≈ys : xs ≈ ys) (p : Any P xs) →
                  index (Any-resp f xs≈ys p) ≡ index p
-index-Any-resp (x ∷ xs≈) (here px) = P.refl
+index-Any-resp (x ∷ xs≈) (here px) = ≡.refl
 index-Any-resp (x ∷ xs≈) (there p) =
   cong suc (index-Any-resp (♭ xs≈) p)
 

src/Data/Container/Combinator/Properties.agda

@@ -18,7 +18,7 @@ open import Data.Sum.Base as S using (inj₁; inj₂; [_,_]′; [_,_])
 open import Function.Base as F using (_∘′_)
 open import Function.Bundles
 open import Level using (_⊔_; lower)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 -- I have proved some of the correctness statements under the
 -- assumption of functional extensionality. I could have reformulated
@@ -27,52 +27,52 @@ open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
 module Identity where
 
   correct : ∀ {s p x} {X : Set x} → ⟦ id {s} {p} ⟧ X ↔ F.id X
-  correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → P.refl) (λ _ → P.refl)
+  correct {X = X} = mk↔ₛ′ from-id to-id (λ _ → ≡.refl) (λ _ → ≡.refl)
 
 module Constant (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where
 
   correct : ∀ {x p y} (X : Set x) {Y : Set y} → ⟦ const {x} {p ⊔ y} X ⟧ Y ↔ F.const X Y
-  correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → P.refl) from∘to
+  correct {x} {y} X {Y} = mk↔ₛ′ (from-const X) (to-const X) (λ _ → ≡.refl) from∘to
     where
     from∘to : (x : ⟦ const X ⟧ Y) → to-const X (proj₁ x) ≡ x
-    from∘to xs = P.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
+    from∘to xs = ≡.cong (proj₁ xs ,_) (ext (λ x → ⊥-elim (lower x)))
 
 module Composition {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
 
   correct : ∀ {x} {X : Set x} → ⟦ C₁ ∘ C₂ ⟧ X ↔ (⟦ C₁ ⟧ F.∘ ⟦ C₂ ⟧) X
-  correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → P.refl) (λ _ → P.refl)
+  correct {X = X} = mk↔ₛ′ (from-∘ C₁ C₂) (to-∘ C₁ C₂) (λ _ → ≡.refl) (λ _ → ≡.refl)
 
 module Product (ext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′)
        {s₁ s₂ p₁ p₂} (C₁ : Container s₁ p₁) (C₂ : Container s₂ p₂) where
 
   correct : ∀ {x} {X : Set x} →  ⟦ C₁ × C₂ ⟧ X ↔ (⟦ C₁ ⟧ X Prod.× ⟦ C₂ ⟧ X)
-  correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → P.refl) from∘to
+  correct {X = X} = mk↔ₛ′ (from-× C₁ C₂) (to-× C₁ C₂) (λ _ → ≡.refl) from∘to
     where
     from∘to : (to-× C₁ C₂) F.∘ (from-× C₁ C₂) ≗ F.id
     from∘to (s , f) =
-      P.cong (s ,_) (ext [ (λ _ → P.refl) , (λ _ → P.refl) ])
+      ≡.cong (s ,_) (ext [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ])
 
 module IndexedProduct {i s p} {I : Set i} (Cᵢ : I → Container s p) where
 
   correct : ∀ {x} {X : Set x} → ⟦ Π I Cᵢ ⟧ X ↔ (∀ i → ⟦ Cᵢ i ⟧ X)
-  correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → P.refl) (λ _ → P.refl)
+  correct {X = X} = mk↔ₛ′ (from-Π I Cᵢ) (to-Π I Cᵢ) (λ _ → ≡.refl) (λ _ → ≡.refl)
 
 module Sum {s₁ s₂ p} (C₁ : Container s₁ p) (C₂ : Container s₂ p) where
 
   correct : ∀ {x} {X : Set x} → ⟦ C₁ ⊎ C₂ ⟧ X ↔ (⟦ C₁ ⟧ X S.⊎ ⟦ C₂ ⟧ X)
   correct {X = X} = mk↔ₛ′ (from-⊎ C₁ C₂) (to-⊎ C₁ C₂) to∘from from∘to
     where
     from∘to : (to-⊎ C₁ C₂) F.∘ (from-⊎ C₁ C₂) ≗ F.id
-    from∘to (inj₁ s₁ , f) = P.refl
-    from∘to (inj₂ s₂ , f) = P.refl
+    from∘to (inj₁ s₁ , f) = ≡.refl
+    from∘to (inj₂ s₂ , f) = ≡.refl
 
     to∘from : (from-⊎ C₁ C₂) F.∘ (to-⊎ C₁ C₂) ≗ F.id
-    to∘from = [ (λ _ → P.refl) , (λ _ → P.refl) ]
+    to∘from = [ (λ _ → ≡.refl) , (λ _ → ≡.refl) ]
 
 module IndexedSum {i s p} {I : Set i} (C : I → Container s p) where
 
   correct : ∀ {x} {X : Set x} → ⟦ Σ I C ⟧ X ↔ (∃ λ i → ⟦ C i ⟧ X)
-  correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → P.refl) (λ _ → P.refl)
+  correct {X = X} = mk↔ₛ′ (from-Σ I C) (to-Σ I C) (λ _ → ≡.refl) (λ _ → ≡.refl)
 
 module ConstantExponentiation {i s p} {I : Set i} (C : Container s p) where
 

src/Data/Container/Indexed.agda

@@ -18,7 +18,7 @@ open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
 open import Function using (_↔_; Inverse)
 open import Relation.Unary using (Pred; _⊆_)
 open import Relation.Binary.Core using (Rel; REL)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_; refl)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_; refl)
 
 ------------------------------------------------------------------------
 
@@ -98,7 +98,7 @@ module _ {i₁ i₂ o₁ o₂}
               Container I₁ O₁ c₁ r → (I₁ → I₂) → (O₁ → O₂) →
               Container I₂ O₂ c₂ r → Set _
   C₁ ⇒C[ f / g ] C₂ = ContainerMorphism C₁ C₂ f g _≡_ (λ R₂ R₁ → R₂ ≡ R₁)
-                                        (λ r₂≡r₁ r₂ → P.subst ⟨id⟩ r₂≡r₁ r₂)
+                                        (λ r₂≡r₁ r₂ → ≡.subst ⟨id⟩ r₂≡r₁ r₂)
 
 -- Degenerate cases where no reindexing is performed.
 
@@ -123,7 +123,7 @@ module _ {i o c r} {I : Set i} {O : Set o} where
 ⟪_⟫ : ∀ {i o c r ℓ} {I : Set i} {O : Set o} {C₁ C₂ : Container I O c r} →
       C₁ ⇒ C₂ → (X : Pred I ℓ) → ⟦ C₁ ⟧ X ⊆ ⟦ C₂ ⟧ X
 ⟪ m ⟫ X (c , k) = command m c , λ r₂ →
-  P.subst X (coherent m) (k (response m r₂))
+  ≡.subst X (coherent m) (k (response m r₂))
 
 module PlainMorphism {i o c r} {I : Set i} {O : Set o} where
 
@@ -145,7 +145,7 @@ module PlainMorphism {i o c r} {I : Set i} {O : Set o} where
   f ∘ g = record
     { command  = command  f ⟨∘⟩ command g
     ; response = response g ⟨∘⟩ response f
-    ; coherent = coherent g ⟨ P.trans ⟩ coherent f
+    ; coherent = coherent g ⟨ ≡.trans ⟩ coherent f
     }
 
   -- Identity commutes with ⟪_⟫.
@@ -187,7 +187,7 @@ module CartesianMorphism
   morphism : C₁ ⇒ C₂
   morphism = record
     { command  = command m
-    ; response = P.subst ⟨id⟩ (response m)
+    ; response = ≡.subst ⟨id⟩ (response m)
     ; coherent = coherent m
     }
 

src/Data/Container/Indexed/Combinator.agda

@@ -21,7 +21,7 @@ open import Function.Indexed.Bundles using (_↔ᵢ_)
 open import Level
 open import Relation.Unary using (Pred; _⊆_; _∪_; _∩_; ⋃; ⋂)
   renaming (_⟨×⟩_ to _⟪×⟫_; _⟨⊙⟩_ to _⟪⊙⟫_; _⟨⊎⟩_ to _⟪⊎⟫_)
-open import Relation.Binary.PropositionalEquality as P
+open import Relation.Binary.PropositionalEquality as ≡
   using (_≗_; refl)
 
 private
@@ -167,7 +167,7 @@ module Constant (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
     from = < F.id , F.const ⊥-elim >
 
     to∘from : _
-    to∘from xs = P.cong (proj₁ xs ,_) (ext ⊥-elim)
+    to∘from xs = ≡.cong (proj₁ xs ,_) (ext ⊥-elim)
 
 module Duality where
 
@@ -202,7 +202,7 @@ module Product (ext : ∀ {ℓ} → Extensionality ℓ ℓ) where
 
     from∘to : from ⟨∘⟩ to ≗ F.id
     from∘to (c , _) =
-      P.cong (c ,_) (ext [ (λ _ → refl) , (λ _ → refl) ])
+      ≡.cong (c ,_) (ext [ (λ _ → refl) , (λ _ → refl) ])
 
 module IndexedProduct where
 
@@ -231,8 +231,8 @@ module Sum (ext : ∀ {ℓ₁ ℓ₂} → Extensionality ℓ₁ ℓ₂) where
     from (inj₂ (c , f)) = inj₂ c , λ{ (All.inj₂ r) → f r}
 
     from∘to : from ⟨∘⟩ to ≗ F.id
-    from∘to (inj₁ _ , _) = P.cong (inj₁ _ ,_) (ext λ{ (All.inj₁ r) → refl})
-    from∘to (inj₂ _ , _) = P.cong (inj₂ _ ,_) (ext λ{ (All.inj₂ r) → refl})
+    from∘to (inj₁ _ , _) = ≡.cong (inj₁ _ ,_) (ext λ{ (All.inj₁ r) → refl})
+    from∘to (inj₂ _ , _) = ≡.cong (inj₂ _ ,_) (ext λ{ (All.inj₂ r) → refl})
 
     to∘from : to ⟨∘⟩ from ≗ F.id
     to∘from =  [ (λ _ → refl) , (λ _ → refl) ]

src/Data/Container/Morphism/Properties.agda

@@ -12,7 +12,7 @@ open import Level using (_⊔_; suc)
 open import Function.Base as F using (_$_)
 open import Data.Product.Base using (∃; proj₁; proj₂; _,_)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≗_)
+open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; _≗_)
 
 open import Data.Container.Core
 open import Data.Container.Morphism
@@ -23,7 +23,7 @@ open import Data.Container.Relation.Binary.Equality.Setoid
 module _ {s p} (C : Container s p) where
 
   id-correct : ∀ {x} {X : Set x} → ⟪ id C ⟫ {X = X} ≗ F.id
-  id-correct x = P.refl
+  id-correct x = ≡.refl
 
 -- Composition.
 
@@ -33,7 +33,7 @@ module _ {s₁ s₂ s₃ p₁ p₂ p₃}
 
   ∘-correct : (f : C₂ ⇒ C₃) (g : C₁ ⇒ C₂) → ∀ {x} {X : Set x} →
               ⟪ f ∘ g ⟫ {X = X} ≗ (⟪ f ⟫ F.∘ ⟪ g ⟫)
-  ∘-correct f g xs = P.refl
+  ∘-correct f g xs = ≡.refl
 
 module _ {s₁ s₂ p₁ p₂} {C₁ : Container s₁ p₁} {C₂ : Container s₂ p₂} where