Qualified import of Properties modules fixing #2280

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

@@ -17,8 +17,8 @@ open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
   using (Reflexive; Sym; Trans; Antisym; Symmetric; Transitive)
 open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.PropositionalEquality.Core as P using (_≡_)
-import Relation.Binary.PropositionalEquality.Properties as P
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
+import Relation.Binary.PropositionalEquality.Properties as ≡
 
 private
   variable
@@ -114,16 +114,16 @@ module _ {A : Set a} where
  _≈_ = Pointwise _≡_
 
  refl : Reflexive _≈_
- refl = reflexive P.refl
+ refl = reflexive ≡.refl
 
  sym : Symmetric _≈_
- sym = symmetric P.sym
+ sym = symmetric ≡.sym
 
  trans : Transitive _≈_
- trans = transitive P.trans
+ trans = transitive ≡.trans
 
  ≈-setoid : Setoid _ _
- ≈-setoid = setoid (P.setoid A)
+ ≈-setoid = setoid (≡.setoid A)
 
 ------------------------------------------------------------------------
 -- Pointwise DSL
@@ -161,15 +161,15 @@ module pw-Reasoning (S : Setoid a ℓ) where
 
   `head : ∀ {as bs} → `Pointwise as bs → as .head ∼ bs .head
   `head (`lift rs)         = rs .head
-  `head (`refl eq)         = S.reflexive (P.cong head eq)
+  `head (`refl eq)         = S.reflexive (≡.cong head eq)
   `head (`bisim rs)        = S.reflexive (rs .head)
   `head (`step `rs)        = `rs .head
   `head (`sym `rs)         = S.sym (`head `rs)
   `head (`trans `rs₁ `rs₂) = S.trans (`head `rs₁) (`head `rs₂)
 
   `tail : ∀ {as bs} → `Pointwise as bs → `Pointwise (as .tail)  (bs .tail)
   `tail (`lift rs)         = `lift (rs .tail)
-  `tail (`refl eq)         = `refl (P.cong tail eq)
+  `tail (`refl eq)         = `refl (≡.cong tail eq)
   `tail (`bisim rs)        = `bisim (rs .tail)
   `tail (`step `rs)        = `rs .tail
   `tail (`sym `rs)         = `sym (`tail `rs)
@@ -196,8 +196,8 @@ module pw-Reasoning (S : Setoid a ℓ) where
   pattern _≈⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`bisim bs∼as)) bs∼cs
   pattern _≡⟨_⟩_  as as∼bs bs∼cs = `trans {as = as} (`refl as∼bs) bs∼cs
   pattern _≡⟨_⟨_ as bs∼as bs∼cs = `trans {as = as} (`sym (`refl bs∼as)) bs∼cs
-  pattern _≡⟨⟩_   as as∼bs       = `trans {as = as} (`refl P.refl) as∼bs
-  pattern _∎      as             = `refl  {as = as} P.refl
+  pattern _≡⟨⟩_   as as∼bs       = `trans {as = as} (`refl ≡.refl) as∼bs
+  pattern _∎      as             = `refl  {as = as} ≡.refl
 
 
   -- Deprecated v2.0
@@ -226,7 +226,7 @@ module pw-Reasoning (S : Setoid a ℓ) where
 
 module ≈-Reasoning {a} {A : Set a} where
 
-  open pw-Reasoning (P.setoid A) public
+  open pw-Reasoning (≡.setoid A) public
 
   infix 4 _≈∞_
   _≈∞_ = `Pointwise∞

src/Data/Char/Properties.agda

@@ -27,10 +27,10 @@ open import Relation.Binary.Definitions
 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.Core as PropEq
+import Relation.Binary.Construct.Closure.Reflexive.Properties as Refl
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; cong; sym; trans; subst)
-import Relation.Binary.PropositionalEquality.Properties as PropEq
+import Relation.Binary.PropositionalEquality.Properties as ≡
 
 ------------------------------------------------------------------------
 -- Primitive properties
@@ -59,13 +59,13 @@ _≟_ : Decidable {A = Char} _≡_
 x ≟ y = map′ ≈⇒≡ ≈-reflexive (toℕ x ℕ.≟ toℕ y)
 
 setoid : Setoid _ _
-setoid = PropEq.setoid Char
+setoid = ≡.setoid Char
 
 decSetoid : DecSetoid _ _
-decSetoid = PropEq.decSetoid _≟_
+decSetoid = ≡.decSetoid _≟_
 
 isDecEquivalence : IsDecEquivalence _≡_
-isDecEquivalence = PropEq.isDecEquivalence _≟_
+isDecEquivalence = ≡.isDecEquivalence _≟_
 
 ------------------------------------------------------------------------
 -- Boolean equality test.
@@ -114,11 +114,11 @@ _<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
 
 <-isStrictPartialOrder : IsStrictPartialOrder _≡_ _<_
 <-isStrictPartialOrder = record
-  { isEquivalence = PropEq.isEquivalence
+  { isEquivalence = ≡.isEquivalence
   ; irrefl        = <-irrefl
   ; trans         = λ {a} {b} {c} → <-trans {a} {b} {c}
-  ; <-resp-≈      = (λ {c} → PropEq.subst (c <_))
-                  , (λ {c} → PropEq.subst (_< c))
+  ; <-resp-≈      = (λ {c} → ≡.subst (c <_))
+                  , (λ {c} → ≡.subst (_< c))
   }
 
 <-isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_
@@ -142,20 +142,20 @@ _<?_ = On.decidable toℕ ℕ._<_ ℕ._<?_
 
 infix 4 _≤?_
 _≤?_ : Decidable _≤_
-_≤?_ = Reflₚ.decidable <-cmp
+_≤?_ = Refl.decidable <-cmp
 
 ≤-reflexive : _≡_ ⇒ _≤_
 ≤-reflexive = Refl.reflexive
 
 ≤-trans : Transitive _≤_
-≤-trans = Reflₚ.trans (λ {a} {b} {c} → <-trans {a} {b} {c})
+≤-trans = Refl.trans (λ {a} {b} {c} → <-trans {a} {b} {c})
 
 ≤-antisym : Antisymmetric _≡_ _≤_
-≤-antisym = Reflₚ.antisym _≡_ refl ℕ.<-asym
+≤-antisym = Refl.antisym _≡_ refl ℕ.<-asym
 
 ≤-isPreorder : IsPreorder _≡_ _≤_
 ≤-isPreorder = record
-  { isEquivalence = PropEq.isEquivalence
+  { isEquivalence = ≡.isEquivalence
   ; reflexive     = ≤-reflexive
   ; trans         = ≤-trans
   }

src/Data/Digit/Properties.agda

@@ -7,13 +7,13 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Data.Digit
-import Data.Char.Properties as Charₚ
+import Data.Char.Properties as Char
 open import Data.Nat.Base using (ℕ)
 open import Data.Nat.Properties using (_≤?_)
 open import Data.Fin.Properties using (inject≤-injective)
 open import Data.Product.Base using (_,_; proj₁)
 open import Data.Vec.Relation.Unary.Unique.Propositional using (Unique)
-import Data.Vec.Relation.Unary.Unique.Propositional.Properties as 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.Core using (True; from-yes; ¬?)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
@@ -22,7 +22,7 @@ open import Function.Base using (_∘_)
 module Data.Digit.Properties where
 
 digitCharsUnique : Unique digitChars
-digitCharsUnique = from-yes (allPairs? (λ x y → ¬? (x Charₚ.≟ y)) digitChars)
+digitCharsUnique = from-yes (allPairs? (λ x y → ¬? (x Char.≟ y)) digitChars)
 
 module _ (base : ℕ) where
   module _ {base≥2 base≥2′ : True (2 ≤? base)} where
@@ -32,4 +32,4 @@ module _ (base : ℕ) where
 
   module _ {base≤16 base≤16′ : True (base ≤? 16)} where
     showDigit-injective : (n m : Digit base) → showDigit {base} {base≤16} n ≡ showDigit {base} {base≤16′} m → n ≡ m
-    showDigit-injective n m = inject≤-injective _ _ n m ∘ Uniqueₚ.lookup-injective digitCharsUnique _ _
+    showDigit-injective n m = inject≤-injective _ _ n m ∘ Unique.lookup-injective digitCharsUnique _ _

src/Data/Fin/Induction.agda

@@ -16,7 +16,7 @@ import Data.Nat.Properties as ℕ
 open import Data.Product.Base using (_,_)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
 open import Data.Vec.Relation.Unary.Linked as Linked using (Linked; [-]; _∷_)
-import Data.Vec.Relation.Unary.Linked.Properties as Linkedₚ
+import Data.Vec.Relation.Unary.Linked.Properties as Linked
 open import Function.Base using (flip; _$_)
 open import Induction
 open import Induction.WellFounded as WF
@@ -124,7 +124,7 @@ module _ {_≈_ : Rel (Fin n) ℓ} where
     pigeon : {xs : Vec (Fin n) n} → Linked (flip _⊏_) (i ∷ xs) → WellFounded _⊏_
     pigeon {xs} i∷xs↑ =
       let (i₁ , i₂ , i₁<i₂ , xs[i₁]≡xs[i₂]) = pigeonhole (n<1+n n) (Vec.lookup (i ∷ xs)) in
-      let xs[i₁]⊏xs[i₂] = Linkedₚ.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
+      let xs[i₁]⊏xs[i₂] = Linked.lookup⁺ (Ord.transitive _⊏_ ⊏.trans) i∷xs↑ i₁<i₂ in
       let xs[i₁]⊏xs[i₁] = ⊏.<-respʳ-≈ (⊏.Eq.reflexive xs[i₁]≡xs[i₂]) xs[i₁]⊏xs[i₂] in
       contradiction xs[i₁]⊏xs[i₁] (⊏.irrefl ⊏.Eq.refl)
 

src/Data/Fin/Substitution/Lemmas.agda

@@ -12,9 +12,9 @@ open import Data.Fin.Substitution
 open import Data.Nat hiding (_⊔_; _/_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)
 open import Data.Vec.Base
-import Data.Vec.Properties as VecProp
+import Data.Vec.Properties as Vec
 open import Function.Base as Fun using (_∘_; _$_; flip)
-open import Relation.Binary.PropositionalEquality.Core as PropEq
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
@@ -68,9 +68,9 @@ record Lemmas₀ (T : Pred ℕ ℓ) : Set ℓ where
   lookup-map-weaken-↑⋆ zero    x           = refl
   lookup-map-weaken-↑⋆ (suc k) zero        = refl
   lookup-map-weaken-↑⋆ (suc k) (suc x) {ρ} = begin
-    lookup (map weaken (map weaken ρ ↑⋆ k)) x        ≡⟨ VecProp.lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
+    lookup (map weaken (map weaken ρ ↑⋆ k)) x        ≡⟨ Vec.lookup-map x weaken (map weaken ρ ↑⋆ k) ⟩
     weaken (lookup (map weaken ρ ↑⋆ k) x)            ≡⟨ cong weaken (lookup-map-weaken-↑⋆ k x) ⟩
-    weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x))      ≡⟨ sym $ VecProp.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
+    weaken (lookup ((ρ ↑) ↑⋆ k) (lift k suc x))      ≡⟨ sym $ Vec.lookup-map (lift k suc x) weaken ((ρ ↑) ↑⋆ k) ⟩
     lookup (map weaken ((ρ ↑) ↑⋆ k)) (lift k suc x)  ∎
 
 record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where
@@ -85,7 +85,7 @@ record Lemmas₁ (T : Pred ℕ ℓ) : Set ℓ where
                       lookup             ρ  x ≡ var      y →
                       lookup (map weaken ρ) x ≡ var (suc y)
   lookup-map-weaken x {y} {ρ} hyp = begin
-    lookup (map weaken ρ) x  ≡⟨ VecProp.lookup-map x weaken ρ ⟩
+    lookup (map weaken ρ) x  ≡⟨ Vec.lookup-map x weaken ρ ⟩
     weaken (lookup ρ x)      ≡⟨ cong weaken hyp ⟩
     weaken (var y)           ≡⟨ weaken-var ⟩
     var (suc y)              ∎
@@ -153,7 +153,7 @@ record Lemmas₂ (T : Pred ℕ ℓ) : Set ℓ where
 
   lookup-⊙ : ∀ x {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
              lookup (ρ₁ ⊙ ρ₂) x ≡ lookup ρ₁ x / ρ₂
-  lookup-⊙ x {ρ₁} {ρ₂} = VecProp.lookup-map x (λ t → t / ρ₂) ρ₁
+  lookup-⊙ x {ρ₁} {ρ₂} = Vec.lookup-map x (λ t → t / ρ₂) ρ₁
 
   lookup-⨀ : ∀ x (ρs : Subs T m n) →
              lookup (⨀ ρs) x ≡ var x /✶ ρs
@@ -239,8 +239,8 @@ record Lemmas₃ (T : Pred ℕ ℓ) : Set ℓ where
 
   ⊙-id : {ρ : Sub T m n} → ρ ⊙ id ≡ ρ
   ⊙-id {ρ = ρ} = begin
-    map (λ t → t / id) ρ  ≡⟨ VecProp.map-cong id-vanishes ρ ⟩
-    map Fun.id         ρ  ≡⟨ VecProp.map-id ρ ⟩
+    map (λ t → t / id) ρ  ≡⟨ Vec.map-cong id-vanishes ρ ⟩
+    map Fun.id         ρ  ≡⟨ Vec.map-id ρ ⟩
     ρ                     ∎
 
   open Lemmas₂ lemmas₂ public hiding (wk-⊙-sub′)
@@ -264,13 +264,13 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
       ρ₁ ↑ ⊙ ρ₂ ↑                             ∎
       where
       lemma = begin
-        map weaken (map (λ t → t / ρ₂) ρ₁)    ≡⟨ sym (VecProp.map-∘ _ _ _) ⟩
-        map (λ t → weaken (t / ρ₂)) ρ₁        ≡⟨ VecProp.map-cong (λ t → begin
+        map weaken (map (λ t → t / ρ₂) ρ₁)    ≡⟨ sym (Vec.map-∘ _ _ _) ⟩
+        map (λ t → weaken (t / ρ₂)) ρ₁        ≡⟨ Vec.map-cong (λ t → begin
                                                    weaken (t / ρ₂)  ≡⟨ sym /-wk ⟩
                                                    t / ρ₂ / wk      ≡⟨ hyp t ⟩
                                                    t / wk / ρ₂ ↑    ≡⟨ cong₂ _/_ /-wk refl ⟩
                                                    weaken t / ρ₂ ↑  ∎) ρ₁ ⟩
-        map (λ t → weaken t / ρ₂ ↑) ρ₁        ≡⟨ VecProp.map-∘ _ _ _ ⟩
+        map (λ t → weaken t / ρ₂ ↑) ρ₁        ≡⟨ Vec.map-∘ _ _ _ ⟩
         map (λ t → t / ρ₂ ↑) (map weaken ρ₁)  ∎
 
     ↑⋆-distrib′ : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} →
@@ -284,7 +284,7 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
 
   map-weaken : {ρ : Sub T m n} → map weaken ρ ≡ ρ ⊙ wk
   map-weaken {ρ = ρ} = begin
-    map weaken ρ          ≡⟨ VecProp.map-cong (λ _ → sym /-wk) ρ ⟩
+    map weaken ρ          ≡⟨ Vec.map-cong (λ _ → sym /-wk) ρ ⟩
     map (λ t → t / wk) ρ  ≡⟨ refl ⟩
     ρ ⊙ wk                ∎
 
@@ -324,8 +324,8 @@ record Lemmas₄ (T : Pred ℕ ℓ) : Set ℓ where
   ⊙-assoc : {ρ₁ : Sub T m n} {ρ₂ : Sub T n o} {ρ₃ : Sub T o p} →
             ρ₁ ⊙ (ρ₂ ⊙ ρ₃) ≡ (ρ₁ ⊙ ρ₂) ⊙ ρ₃
   ⊙-assoc {ρ₁ = ρ₁} {ρ₂} {ρ₃} = begin
-    map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁                  ≡⟨ VecProp.map-cong /-⊙ ρ₁ ⟩
-    map (λ t → t / ρ₂ / ρ₃) ρ₁                  ≡⟨ VecProp.map-∘ _ _ _ ⟩
+    map (λ t → t / ρ₂ ⊙ ρ₃) ρ₁                  ≡⟨ Vec.map-cong /-⊙ ρ₁ ⟩
+    map (λ t → t / ρ₂ / ρ₃) ρ₁                  ≡⟨ Vec.map-∘ _ _ _ ⟩
     map (λ t → t / ρ₃) (map (λ t → t / ρ₂) ρ₁)  ∎
 
   map-weaken-⊙-sub : ∀ {ρ : Sub T m n} {t} → map weaken ρ ⊙ sub t ≡ ρ
@@ -560,7 +560,7 @@ record TermLemmas (T : ℕ → Set) : Set₁ where
              (∀ x → lookup ρ₂ x ≡ T.var (f x)) →
              map T.var ρ₁ ≡ ρ₂
   map-var≡ {ρ₁ = ρ₁} {ρ₂ = ρ₂} {f = f} hyp₁ hyp₂ = extensionality λ x →
-    lookup (map T.var ρ₁) x  ≡⟨ VecProp.lookup-map x _ ρ₁ ⟩
+    lookup (map T.var ρ₁) x  ≡⟨ Vec.lookup-map x _ ρ₁ ⟩
     T.var (lookup ρ₁ x)      ≡⟨ cong T.var $ hyp₁ x ⟩
     T.var (f x)              ≡⟨ sym $ hyp₂ x ⟩
     lookup ρ₂ x              ∎
@@ -577,15 +577,15 @@ record TermLemmas (T : ℕ → Set) : Set₁ where
   ↑≡↑ : {ρ : Sub Fin m n} → map T.var (ρ VarSubst.↑) ≡ map T.var ρ T.↑
   ↑≡↑ {ρ = ρ} = map-var≡
     (VarLemmas.lookup-↑⋆ (lookup ρ) (λ _ → refl) 1)
-    (lookup-↑⋆ (lookup ρ) (λ _ → VecProp.lookup-map _ _ ρ) 1)
+    (lookup-↑⋆ (lookup ρ) (λ _ → Vec.lookup-map _ _ ρ) 1)
 
   /Var≡/ : ∀ {ρ : Sub Fin m n} {t} → t /Var ρ ≡ t T./ map T.var ρ
   /Var≡/ {ρ = ρ} {t = t} =
     /✶-↑✶ (ε ▻ ρ) (ε ▻ map T.var ρ)
       (λ k x →
          T.var x /Var ρ VarSubst.↑⋆ k        ≡⟨ app-var ⟩
          T.var (lookup (ρ VarSubst.↑⋆ k) x)  ≡⟨ cong T.var $ VarLemmas.lookup-↑⋆ _ (λ _ → refl) k _ ⟩
-         T.var (lift k (VarSubst._/ ρ) x)    ≡⟨ sym $ lookup-↑⋆ _ (λ _ → VecProp.lookup-map _ _ ρ) k _ ⟩
+         T.var (lift k (VarSubst._/ ρ) x)    ≡⟨ sym $ lookup-↑⋆ _ (λ _ → Vec.lookup-map _ _ ρ) k _ ⟩
          lookup (map T.var ρ T.↑⋆ k) x       ≡⟨ sym app-var ⟩
          T.var x T./ map T.var ρ T.↑⋆ k      ∎)
       zero t

src/Data/Integer/Properties.agda

@@ -24,7 +24,7 @@ open import Data.Nat.Solver
 open import Data.Product.Base using (proj₁; proj₂; _,_; _×_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sign as Sign using (Sign) renaming (_*_ to _𝕊*_)
-import Data.Sign.Properties as 𝕊ₚ
+import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
@@ -1597,7 +1597,7 @@ abs-* i j = abs-◃ _ _
 *-cancelʳ-≡ : ∀ i j k .{{_ : NonZero k}} → i * k ≡ j * k → i ≡ j
 *-cancelʳ-≡ i j k eq with sign-cong′ eq
 ... | inj₁ s[ik]≡s[jk] = ◃-cong
-  (𝕊ₚ.*-cancelʳ-≡ (sign k) (sign i) (sign j) s[ik]≡s[jk])
+  (Sign.*-cancelʳ-≡ (sign k) (sign i) (sign j) s[ik]≡s[jk])
   (ℕ.*-cancelʳ-≡ ∣ i ∣ ∣ j ∣ _ (abs-cong eq))
 ... | inj₂ (∣ik∣≡0 , ∣jk∣≡0) = trans
   (∣i∣≡0⇒i≡0 (ℕ.m*n≡0⇒m≡0 _ _ ∣ik∣≡0))
@@ -1709,7 +1709,7 @@ neg-distribʳ-* i j = begin
 ◃-distrib-* s t zero    (suc n) = refl
 ◃-distrib-* s t (suc m) zero    =
   trans
-    (cong₂ _◃_ (𝕊ₚ.*-comm s t) (ℕ.*-comm m 0))
+    (cong₂ _◃_ (Sign.*-comm s t) (ℕ.*-comm m 0))
     (*-comm (t ◃ zero) (s ◃ suc m))
 ◃-distrib-* s t (suc m) (suc n) =
   sym (cong₂ _◃_

src/Data/List/Countdown.agda

@@ -29,10 +29,10 @@ open import Data.Sum.Properties
 open import Relation.Nullary.Reflects using (invert)
 open import Relation.Nullary
 open import Relation.Nullary.Decidable using (dec-true; dec-false)
-open import Relation.Binary.PropositionalEquality.Core as PropEq
+open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; _≢_; refl; cong)
-import Relation.Binary.PropositionalEquality.Properties as PropEq
-open PropEq.≡-Reasoning
+import Relation.Binary.PropositionalEquality.Properties as ≡
+open ≡.≡-Reasoning
 
 private
   open module D = DecSetoid D
@@ -124,12 +124,12 @@ record _⊕_ (counted : List Elem) (n : ℕ) : Set where
 
 -- A countdown can be initialised by proving that Elem is finite.
 
-empty : ∀ {n} → Injection D.setoid (PropEq.setoid (Fin n)) → [] ⊕ n
+empty : ∀ {n} → Injection D.setoid (≡.setoid (Fin n)) → [] ⊕ n
 empty inj =
   record { kind      = inj₂ ∘ to
          ; injective = λ {x} {y} {i} eq₁ eq₂ → injective (begin
              to x ≡⟨ inj₂-injective eq₁ ⟩
-             i    ≡⟨ PropEq.sym $ inj₂-injective eq₂ ⟩
+             i    ≡⟨ ≡.sym $ inj₂-injective eq₂ ⟩
              to y ∎)
          }
   where open Injection inj
@@ -199,7 +199,7 @@ insert {counted} {n} counted⊕1+n x x∉counted =
   inj eq₁ eq₂ | no  _ | no  _ | inj₂ i         | inj₂ _ | inj₂ _ | _ | _ | hlp =
     hlp _ refl refl $
       punchOut-injective {i = i} _ _ $
-        (PropEq.trans (inj₂-injective eq₁) (PropEq.sym (inj₂-injective eq₂)))
+        (≡.trans (inj₂-injective eq₁) (≡.sym (inj₂-injective eq₂)))
 
 -- Counts an element if it has not already been counted.