diff --git a/CHANGELOG.md b/CHANGELOG.md
index a55dcb0f79..78dea52440 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1547,6 +1547,8 @@ Other minor changes
   combine-surjective : ∀ i → ∃₂ λ j k → combine j k ≡ i
   combine-monoˡ-<    : i < j → combine i k < combine j l
 
+  ℕ-ℕ≡toℕ‿ℕ-         : n ℕ-ℕ i ≡ toℕ (n ℕ- i)
+
   lower₁-injective   : lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
   pinch-injective    : suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
 
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index ce93b67b01..06c4581337 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -11,6 +11,7 @@
 
 module Data.Fin.Base where
 
+open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
@@ -18,6 +19,7 @@ open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
 open import Level using (0ℓ)
 open import Relation.Nullary using (yes; no)
+open import Relation.Nullary.Negation using (contradiction)
 open import Relation.Nullary.Decidable.Core using (True; toWitness)
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≢_; refl; cong)
@@ -122,7 +124,7 @@ inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
 lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
 lower₁ {suc n} zero    _  = zero
-lower₁ {suc n} (suc i) ne = suc (lower₁ i λ x → ne (cong suc x))
+lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
 -- A strengthening injection into the minimal Fin fibre.
 strengthen : ∀ (i : Fin n) → Fin′ (suc i)
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 13d106be57..8a23d5049e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -790,6 +790,10 @@ toℕ‿ℕ- (suc n) (suc i)  = toℕ‿ℕ- n i
 -- _ℕ-ℕ_
 ------------------------------------------------------------------------
 
+ℕ-ℕ≡toℕ‿ℕ- : ∀ n i → n ℕ-ℕ i ≡ toℕ (n ℕ- i)
+ℕ-ℕ≡toℕ‿ℕ- n       zero    = sym (toℕ-fromℕ n)
+ℕ-ℕ≡toℕ‿ℕ- (suc n) (suc i) = ℕ-ℕ≡toℕ‿ℕ- n i
+
 nℕ-ℕi≤n : ∀ n i → n ℕ-ℕ i ℕ.≤ n
 nℕ-ℕi≤n n       zero     = ℕₚ.≤-refl
 nℕ-ℕi≤n (suc n) (suc i)  = begin
diff --git a/src/Data/List/Membership/Setoid.agda b/src/Data/List/Membership/Setoid.agda
index 3896a9004d..e8476d9a44 100644
--- a/src/Data/List/Membership/Setoid.agda
+++ b/src/Data/List/Membership/Setoid.agda
@@ -11,7 +11,6 @@ open import Relation.Binary
 module Data.List.Membership.Setoid {c ℓ} (S : Setoid c ℓ) where
 
 open import Function.Base using (_∘_; id; flip)
-open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; _∷_; length; lookup)
 open import Data.List.Relation.Unary.Any
   using (Any; index; map; here; there)
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 9ec496f421..3a600acb4b 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -15,7 +15,7 @@ open import Algebra.Bundles
 open import Algebra.Definitions as AlgebraicDefinitions using (Involutive)
 import Algebra.Structures as AlgebraicStructures
 open import Data.Bool.Base using (Bool; false; true; not; if_then_else_)
-open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ; inject₁)
+open import Data.Fin.Base using (Fin; zero; suc; cast; toℕ)
 open import Data.List.Base as List
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
diff --git a/src/Data/List/Relation/Binary/Equality/Setoid.agda b/src/Data/List/Relation/Binary/Equality/Setoid.agda
index cd1a6d86d1..feaa48e6dc 100644
--- a/src/Data/List/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/List/Relation/Binary/Equality/Setoid.agda
@@ -11,7 +11,7 @@ open import Relation.Binary using (Setoid)
 
 module Data.List.Relation.Binary.Equality.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Pointwise as PW using (Pointwise)
 open import Data.List.Relation.Unary.Unique.Setoid S using (Unique)
@@ -129,13 +129,14 @@ concat⁺ = PW.concat⁺
 ------------------------------------------------------------------------
 -- tabulate
 
-tabulate⁺ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
-            (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
-tabulate⁺ = PW.tabulate⁺
+module _ {n} {f g : Fin n → A}
+  where
+
+  tabulate⁺ : (∀ i → f i ≈ g i) → tabulate f ≋ tabulate g
+  tabulate⁺ = PW.tabulate⁺
 
-tabulate⁻ : ∀ {n} {f : Fin n → A} {g : Fin n → A} →
-            tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
-tabulate⁻ = PW.tabulate⁻
+  tabulate⁻ : tabulate f ≋ tabulate g → (∀ i → f i ≈ g i)
+  tabulate⁻ = PW.tabulate⁻
 
 ------------------------------------------------------------------------
 -- filter
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 08f1b35dc2..335894a701 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -14,7 +14,6 @@ module Data.List.Relation.Binary.Permutation.Setoid.Properties
 
 open import Algebra
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base as List hiding (head; tail)
 open import Data.List.Relation.Binary.Pointwise as Pointwise
   using (Pointwise; head; tail)
diff --git a/src/Data/List/Relation/Unary/Any.agda b/src/Data/List/Relation/Unary/Any.agda
index 40398a3b8e..02f7219229 100644
--- a/src/Data/List/Relation/Unary/Any.agda
+++ b/src/Data/List/Relation/Unary/Any.agda
@@ -9,7 +9,7 @@
 module Data.List.Relation.Unary.Any where
 
 open import Data.Empty
-open import Data.Fin.Base
+open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List; []; [_]; _∷_)
 open import Data.Product as Prod using (∃; _,_)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
diff --git a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
index 2435b34168..7494b55795 100644
--- a/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
@@ -6,7 +6,6 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.Fin hiding (_≟_)
 open import Data.List.Base
 open import Data.List.Membership.Setoid.Properties as Membership
 open import Data.List.Relation.Unary.Any using (index)
@@ -85,5 +84,5 @@ module _ (S? : DecSetoid a ℓ₁) where
 module _ (S : Setoid a ℓ₁) where
 
   lookup-surjective : ∀ {xs} → IsEnumeration S xs →
-                      Surjective {A = Fin (length xs)} _≡_ (_≈_ S) (lookup xs)
+                      Surjective _≡_ (_≈_ S) (lookup xs)
   lookup-surjective _∈xs y = index (y ∈xs) , sym S (lookup-index (y ∈xs))
diff --git a/src/Data/List/Relation/Unary/Linked/Properties.agda b/src/Data/List/Relation/Unary/Linked/Properties.agda
index 4bb2d4bf92..d00b76a329 100644
--- a/src/Data/List/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/List/Relation/Unary/Linked/Properties.agda
@@ -16,8 +16,6 @@ import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
 open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
-open import Data.Fin.Base using (Fin)
-open import Data.Fin.Properties using (suc-injective)
 open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s)
 open import Data.Nat.Properties using (≤-refl; ≤-pred; ≤-step)
 open import Data.Maybe.Relation.Binary.Connected
diff --git a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
index ea113da0da..c9ac3bff73 100644
--- a/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
@@ -8,14 +8,14 @@
 
 module Data.List.Relation.Unary.Unique.Propositional.Properties where
 
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Relation.Binary.Disjoint.Propositional
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.List.Relation.Unary.Unique.Propositional
 import Data.List.Relation.Unary.Unique.Setoid.Properties as Setoid
-open import Data.Nat.Base
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (_<_)
 open import Data.Nat.Properties using (<⇒≢)
 open import Data.Product using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (≡⇒≡×≡)
diff --git a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
index 1cdde539df..e182b43363 100644
--- a/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
@@ -8,7 +8,6 @@
 
 module Data.List.Relation.Unary.Unique.Setoid.Properties where
 
-open import Data.Fin.Base using (Fin)
 open import Data.List.Base
 open import Data.List.Membership.Setoid.Properties
 open import Data.List.Relation.Binary.Disjoint.Setoid
@@ -20,7 +19,8 @@ open import Data.List.Relation.Unary.Unique.Setoid
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (_×ₛ_)
 import Data.List.Relation.Unary.AllPairs.Properties as AllPairs
-open import Data.Nat.Base
+open import Data.Fin.Base using (Fin)
+open import Data.Nat.Base using (_<_)
 open import Function.Base using (_∘_; id)
 open import Level using (Level)
 open import Relation.Binary using (Rel; Setoid)
@@ -40,8 +40,8 @@ private
 
 module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
 
-  open Setoid S renaming (Carrier to A; _≈_ to _≈₁_)
-  open Setoid R renaming (Carrier to B; _≈_ to _≈₂_)
+  open Setoid S renaming (_≈_ to _≈₁_)
+  open Setoid R renaming (_≈_ to _≈₂_)
 
   map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
          ∀ {xs} → Unique S xs → Unique R (map f xs)
@@ -153,7 +153,5 @@ module _ (S : Setoid a ℓ) where
 
 module _ (S : Setoid a ℓ) {P : Pred _ p} (P? : Decidable P) where
 
-  open Setoid S renaming (Carrier to A)
-
   filter⁺ : ∀ {xs} → Unique S xs → Unique S (filter P? xs)
   filter⁺ = AllPairs.filter⁺ P?
diff --git a/src/Data/Nat/DivMod/WithK.agda b/src/Data/Nat/DivMod/WithK.agda
index 3fc45ec291..458a7eef33 100644
--- a/src/Data/Nat/DivMod/WithK.agda
+++ b/src/Data/Nat/DivMod/WithK.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.DivMod.WithK where
 
-open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_; zero; suc)
+open import Data.Nat using (ℕ; NonZero; _+_; _*_; _≟_)
 open import Data.Nat.DivMod hiding (_mod_; _divMod_)
 open import Data.Nat.Properties using (≤⇒≤″)
 open import Data.Nat.WithK
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 06a19bf92b..1696e6b482 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -17,7 +17,7 @@ module Data.Vec.Functional where
 
 open import Data.Fin.Base
 open import Data.List.Base as L using (List)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
 open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Base as V using (Vec)
diff --git a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
index f248ac57d1..ccc8e3c00c 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
@@ -6,8 +6,7 @@
 
 {-# OPTIONS --without-K --safe #-}
 
-open import Data.Fin.Base
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Functional as VF hiding (map)
 open import Data.Vec.Functional.Relation.Binary.Pointwise
   using (Pointwise)
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda
index 360dc46540..645dafadec 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda
@@ -8,8 +8,6 @@
 
 module Data.Vec.Functional.Relation.Binary.Pointwise where
 
-open import Data.Fin.Base
-open import Data.Nat.Base
 open import Data.Vec.Functional as VF hiding (map)
 open import Level using (Level)
 open import Relation.Binary
diff --git a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
index 75edf115fd..7be16938dd 100644
--- a/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
@@ -8,9 +8,9 @@
 
 module Data.Vec.Functional.Relation.Binary.Pointwise.Properties where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
+open import Data.Fin.Properties using (all?; splitAt-↑ˡ; splitAt-↑ʳ)
+open import Data.Nat.Base using (ℕ; zero; suc)
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent
   using () renaming (Pointwise to ×-Pointwise)
diff --git a/src/Data/Vec/Functional/Relation/Unary/All.agda b/src/Data/Vec/Functional/Relation/Unary/All.agda
index 7c6e418a6d..7a1d0412be 100644
--- a/src/Data/Vec/Functional/Relation/Unary/All.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/All.agda
@@ -8,9 +8,7 @@
 
 module Data.Vec.Functional.Relation.Unary.All where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Properties using (all?)
 open import Data.Product using (_,_)
 open import Data.Vec.Functional as VF hiding (map)
 open import Level using (Level)
diff --git a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
index 5ce23f962a..d9b288a4d3 100644
--- a/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
@@ -8,9 +8,8 @@
 
 module Data.Vec.Functional.Relation.Unary.All.Properties where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
-open import Data.Nat.Base
+open import Data.Fin.Base using (zero; suc; _↑ˡ_; _↑ʳ_; splitAt)
+open import Data.Fin.Properties using (splitAt-↑ˡ; splitAt-↑ʳ)
 open import Data.Product as Σ using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_])
 open import Data.Vec.Functional as VF hiding (map)
@@ -38,7 +37,7 @@ module _ {P : Pred A p} {Q : Pred B q} {f : A → B} where
 ------------------------------------------------------------------------
 -- replicate
 
-module _ {P : Pred A p} {x : A} {n : ℕ} where
+module _ {P : Pred A p} {x : A} {n} where
 
   replicate⁺ : P x → All P (replicate {n = n} x)
   replicate⁺ = const
@@ -87,14 +86,14 @@ tail⁺ P ps = ps ∘ suc
 ------------------------------------------------------------------------
 -- ++
 
-module _ (P : Pred A p) {m n : ℕ} {xs : Vector A m} {ys : Vector A n} where
+module _ (P : Pred A p) {m n} {xs : Vector A m} {ys : Vector A n} where
 
   ++⁺ : All P xs → All P ys → All P (xs ++ ys)
   ++⁺ pxs pys i with splitAt m i
   ... | inj₁ i′ = pxs i′
   ... | inj₂ j′ = pys j′
 
-module _ (P : Pred A p) {m n : ℕ} (xs : Vector A m) {ys : Vector A n} where
+module _ (P : Pred A p) {m n} (xs : Vector A m) {ys : Vector A n} where
 
   ++⁻ˡ : All P (xs ++ ys) → All P xs
   ++⁻ˡ ps i with ps (i ↑ˡ n)
diff --git a/src/Data/Vec/Functional/Relation/Unary/Any.agda b/src/Data/Vec/Functional/Relation/Unary/Any.agda
index e50cb24eee..23bf65afc5 100644
--- a/src/Data/Vec/Functional/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Functional/Relation/Unary/Any.agda
@@ -8,8 +8,8 @@
 
 module Data.Vec.Functional.Relation.Unary.Any where
 
-open import Data.Fin.Base
-open import Data.Fin.Properties
+open import Data.Fin.Base using (zero; suc)
+open import Data.Fin.Properties using (any?)
 open import Data.Nat.Base
 open import Data.Product as Σ using (Σ; ∃; _×_; _,_; proj₁; proj₂)
 open import Data.Vec.Functional as VF hiding (map)
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 739467517e..97d27767cb 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -10,11 +10,11 @@ module Data.Vec.Properties where
 
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
-open import Data.Nat.Properties as ℕₚ
-  using (+-assoc; ≤-step; ≤-refl; ≤-trans)
+open import Data.Nat.Properties
+  using (+-assoc; ≤-step; ≤-refl; ≤-trans; suc-injective)
 open import Data.Product as Prod
   using (_×_; _,_; proj₁; proj₂; <_,_>; uncurry)
 open import Data.Sum.Base using ([_,_]′)
@@ -396,7 +396,7 @@ toList-cast {n = suc _} eq (x ∷ xs) =
 
 cast-is-id : .(eq : m ≡ m) (xs : Vec A m) → cast eq xs ≡ xs
 cast-is-id eq []       = refl
-cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (ℕₚ.suc-injective eq) xs)
+cast-is-id eq (x ∷ xs) = cong (x ∷_) (cast-is-id (suc-injective eq) xs)
 
 subst-is-cast : (eq : m ≡ n) (xs : Vec A m) → subst (Vec A) eq xs ≡ cast eq xs
 subst-is-cast refl xs = sym (cast-is-id refl xs)
@@ -405,7 +405,7 @@ cast-trans : .(eq₁ : m ≡ n) (eq₂ : n ≡ o) (xs : Vec A m) →
              cast eq₂ (cast eq₁ xs) ≡ cast (trans eq₁ eq₂) xs
 cast-trans {m = zero}  {n = zero}  {o = zero}  eq₁ eq₂ [] = refl
 cast-trans {m = suc _} {n = suc _} {o = suc _} eq₁ eq₂ (x ∷ xs) =
-  cong (x ∷_) (cast-trans (ℕₚ.suc-injective eq₁) (ℕₚ.suc-injective eq₂) xs)
+  cong (x ∷_) (cast-trans (suc-injective eq₁) (suc-injective eq₂) xs)
 
 ------------------------------------------------------------------------
 -- map
@@ -422,7 +422,7 @@ map-cast : (f : A → B) .(eq : m ≡ n) (xs : Vec A m) →
            map f (cast eq xs) ≡ cast eq (map f xs)
 map-cast {n = zero}  f eq []       = refl
 map-cast {n = suc _} f eq (x ∷ xs)
-  = cong (f x ∷_) (map-cast f (ℕₚ.suc-injective eq) xs)
+  = cong (f x ∷_) (map-cast f (suc-injective eq) xs)
 
 map-++ : ∀ (f : A → B) (xs : Vec A m) (ys : Vec A n) →
          map f (xs ++ ys) ≡ map f xs ++ map f ys
@@ -518,19 +518,19 @@ lookup-cast : .(eq : m ≡ n) (xs : Vec A m) (i : Fin m) →
               lookup (cast eq xs) (Fin.cast eq i) ≡ lookup xs i
 lookup-cast {n = suc _} eq (x ∷ _)  zero    = refl
 lookup-cast {n = suc _} eq (_ ∷ xs) (suc i) =
-  lookup-cast (ℕₚ.suc-injective eq) xs i
+  lookup-cast (suc-injective eq) xs i
 
 lookup-cast₁ : .(eq : m ≡ n) (xs : Vec A m) (i : Fin n) →
                lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
 lookup-cast₁ eq (x ∷ _)  zero    = refl
 lookup-cast₁ eq (_ ∷ xs) (suc i) =
-  lookup-cast₁ (ℕₚ.suc-injective eq) xs i
+  lookup-cast₁ (suc-injective eq) xs i
 
 lookup-cast₂ : .(eq : m ≡ n) (xs : Vec A n) (i : Fin m) →
                lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
-lookup-cast₂ {n = suc _} eq (x ∷ _)  zero    = refl
-lookup-cast₂ {n = suc _} eq (_ ∷ xs) (suc i) =
-  lookup-cast₂ (ℕₚ.suc-injective eq) xs i
+lookup-cast₂ eq (x ∷ _)  zero    = refl
+lookup-cast₂ eq (_ ∷ xs) (suc i) =
+  lookup-cast₂ (suc-injective eq) xs i
 
 lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →
                 lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda
index 2178fdf54d..b30089d33c 100644
--- a/src/Data/Vec/Recursive.agda
+++ b/src/Data/Vec/Recursive.agda
@@ -19,7 +19,7 @@ module Data.Vec.Recursive where
 open import Level using (Level; lift)
 open import Function.Bundles using (mk↔′)
 open import Function.Properties.Inverse using (↔-isEquivalence; ↔-refl; ↔-sym; ↔-trans)
-open import Data.Nat.Base as Nat using (ℕ; zero; suc)
+open import Data.Nat.Base as Nat using (ℕ; zero; suc; NonZero; pred)
 open import Data.Nat.Properties using (+-comm; *-comm)
 open import Data.Empty.Polymorphic
 open import Data.Fin.Base as Fin using (Fin; zero; suc)
diff --git a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
index 4d8330590d..8fc0a267db 100644
--- a/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
+++ b/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
@@ -9,7 +9,6 @@
 module Data.Vec.Relation.Binary.Pointwise.Extensional where
 
 open import Data.Fin.Base using (zero; suc)
-open import Data.Nat.Base using (zero; suc)
 open import Data.Vec.Base as Vec hiding ([_]; head; tail; map)
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Inductive
   using ([]; _∷_)
@@ -73,8 +72,8 @@ module _ {_∼_ : REL A B ℓ} where
 
   extensional⇒inductive : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
                            Pointwise _∼_ xs ys → IPointwise _∼_ xs ys
-  extensional⇒inductive {zero} {[]}       {[]}      xs∼ys = []
-  extensional⇒inductive {suc n} {x ∷ xs} {y ∷ ys} xs∼ys =
+  extensional⇒inductive {xs = []}       {[]}   xs∼ys = []
+  extensional⇒inductive {xs = x ∷ xs} {y ∷ ys} xs∼ys =
     (head xs∼ys) ∷ extensional⇒inductive (tail xs∼ys)
 
   inductive⇒extensional : ∀ {n} {xs : Vec A n} {ys : Vec B n} →
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index c263276074..b16340ef6b 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -8,8 +8,7 @@
 
 module Data.Vec.Relation.Unary.All where
 
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
 open import Data.Product as Prod using (_×_; _,_; uncurry; <_,_>)
 open import Data.Sum.Base as Sum using (inj₁; inj₂)
 open import Data.Vec.Base as Vec using (Vec; []; _∷_)
diff --git a/src/Data/Vec/Relation/Unary/All/Properties.agda b/src/Data/Vec/Relation/Unary/All/Properties.agda
index ea6a2f521e..b25a860c68 100644
--- a/src/Data/Vec/Relation/Unary/All/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/All/Properties.agda
@@ -37,7 +37,7 @@ private
 ------------------------------------------------------------------------
 -- lookup
 
-lookup⁺ : All P xs → (i : Fin n) → P (Vec.lookup xs i)
+lookup⁺ : All P xs → ∀ i → P (Vec.lookup xs i)
 lookup⁺ (px ∷ _)  zero    = px
 lookup⁺ (_ ∷ pxs) (suc i) = lookup⁺ pxs i
 
@@ -140,8 +140,8 @@ module _ {P : A → Set p} where
 
   tabulate⁻ : ∀ {n} {f : Fin n → A} →
               All P (tabulate f) → (∀ i → P (f i))
-  tabulate⁻ {suc n} (px ∷ _) zero    = px
-  tabulate⁻ {suc n} (_ ∷ pf) (suc i) = tabulate⁻ pf i
+  tabulate⁻ (px ∷ _) zero    = px
+  tabulate⁻ (_ ∷ pf) (suc i) = tabulate⁻ pf i
 
 ------------------------------------------------------------------------
 -- take and drop
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index 5a65a74dd6..a54991976f 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -9,8 +9,8 @@
 module Data.Vec.Relation.Unary.Any {a} {A : Set a} where
 
 open import Data.Empty
-open import Data.Fin.Base
-open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Fin.Base using (Fin; zero; suc)
+open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Vec.Base as Vec using (Vec; []; [_]; _∷_)
 open import Data.Product as Prod using (∃; _,_)
diff --git a/src/Data/Vec/Relation/Unary/Any/Properties.agda b/src/Data/Vec/Relation/Unary/Any/Properties.agda
index a300c44d55..9faa49d464 100644
--- a/src/Data/Vec/Relation/Unary/Any/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Any/Properties.agda
@@ -363,8 +363,8 @@ module _ {P : Pred A p} where
 
   tabulate⁻ : ∀ {n} {f : Fin n → A} →
               Any P (tabulate f) → ∃ λ i → P (f i)
-  tabulate⁻ {suc n} (here p)  = zero , p
-  tabulate⁻ {suc n} (there p) = Prod.map suc id (tabulate⁻ p)
+  tabulate⁻ (here p)  = zero , p
+  tabulate⁻ (there p) = Prod.map suc id (tabulate⁻ p)
 
 ------------------------------------------------------------------------
 -- mapWith∈
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index 20806dc5f5..3935a263c4 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -14,10 +14,9 @@ open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 import Data.Vec.Relation.Unary.All.Properties as Allₚ
 open import Data.Vec.Relation.Unary.Linked as Linked
   using (Linked; []; [-]; _∷_)
-open import Data.Fin.Base using (Fin; zero; suc; _<_)
-open import Data.Fin.Properties using (suc-injective)
-open import Data.Nat.Base using (ℕ; zero; suc)
-open import Data.Nat.Properties using (<-pred) -- ≤-refl; ≤-pred; ≤-step)
+open import Data.Fin.Base using (zero; suc; _<_)
+open import Data.Nat.Base using (ℕ; zero; suc; NonZero)
+open import Data.Nat.Properties using (<-pred)
 open import Level using (Level)
 open import Function.Base using (_∘_; flip; _on_)
 open import Relation.Binary using (Rel; Transitive; DecSetoid)
@@ -44,7 +43,7 @@ module _ (trans : Transitive R) where
   Linked⇒All Rvx [-]         = Rvx ∷ []
   Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs
 
-  lookup⁺ : ∀ {i j : Fin n} {xs} →
+  lookup⁺ : ∀ {i j} {xs : Vec _ n} →
            Linked R xs → i < j →
            R (lookup xs i) (lookup xs j)
   lookup⁺ {i = zero}  {j = suc j} (rx ∷ rxs) i<j = Allₚ.lookup⁺ (Linked⇒All rx rxs) j
diff --git a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
index 9a57cff263..acd1b916c8 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
@@ -8,12 +8,12 @@
 
 module Data.Vec.Relation.Unary.Unique.Propositional.Properties where
 
-open import Data.Fin.Base using (Fin)
 open import Data.Vec.Base
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.Vec.Relation.Unary.Unique.Propositional
 import Data.Vec.Relation.Unary.Unique.Setoid.Properties as Setoid
+open import Data.Fin.Base using(Fin)
 open import Data.Nat.Base
 open import Data.Nat.Properties using (<⇒≢)
 open import Data.Product using (_×_; _,_)
diff --git a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
index d1170ee8df..7166a8af45 100644
--- a/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
@@ -15,7 +15,7 @@ import Data.Vec.Relation.Unary.All.Properties as Allₚ
 open import Data.Vec.Relation.Unary.AllPairs as AllPairs using (AllPairs)
 open import Data.Vec.Relation.Unary.Unique.Setoid
 import Data.Vec.Relation.Unary.AllPairs.Properties as AllPairsₚ
-open import Data.Nat.Base
+open import Data.Nat.Base using (ℕ; _+_)
 open import Function.Base using (_∘_; id)
 open import Level using (Level)
 open import Relation.Binary using (Rel; Setoid)
@@ -33,8 +33,8 @@ private
 
 module _ (S : Setoid a ℓ₁) (R : Setoid b ℓ₂) where
 
-  open Setoid S renaming (Carrier to A; _≈_ to _≈₁_)
-  open Setoid R renaming (Carrier to B; _≈_ to _≈₂_)
+  open Setoid S renaming (_≈_ to _≈₁_)
+  open Setoid R renaming (_≈_ to _≈₂_)
 
   map⁺ : ∀ {f} → (∀ {x y} → f x ≈₂ f y → x ≈₁ y) →
          ∀ {n xs} → Unique S {n} xs → Unique R {n} (map f xs)
@@ -67,7 +67,7 @@ module _ (S : Setoid a ℓ) where
 
 module _ (S : Setoid a ℓ) where
 
-  open Setoid S renaming (Carrier to A)
+  open Setoid S
 
   lookup-injective : ∀ {n xs} → Unique S {n} xs → ∀ i j → lookup xs i ≈ lookup xs j → i ≡ j
   lookup-injective (px ∷ pxs) zero zero eq = P.refl