diff --git a/src/Algebra/Construct/LexProduct.agda b/src/Algebra/Construct/LexProduct.agda
index e2f5825824..65a6b80ba1 100644
--- a/src/Algebra/Construct/LexProduct.agda
+++ b/src/Algebra/Construct/LexProduct.agda
@@ -6,16 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
-open import Data.Bool using (true; false)
+open import Algebra.Bundles using (Magma)
+open import Algebra.Definitions
+open import Data.Bool.Base using (true; false)
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Pointwise.NonDependent using (Pointwise)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_∘_)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Decidable)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Negation using (contradiction; contradiction₂)
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction; contradiction₂)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 module Algebra.Construct.LexProduct
diff --git a/src/Algebra/Properties/Monoid/Sum.agda b/src/Algebra/Properties/Monoid/Sum.agda
index ae64a5f4dc..78a8d3b205 100644
--- a/src/Algebra/Properties/Monoid/Sum.agda
+++ b/src/Algebra/Properties/Monoid/Sum.agda
@@ -7,16 +7,17 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Algebra.Bundles using (Monoid)
+
+module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
+
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero)
-open import Data.Vec.Functional as Vector
+open import Data.Vec.Functional as Vector using (Vector; replicate; init;
+  last; head; tail)
 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.Core as ≡ using (_≗_; _≡_)
 
-module Algebra.Properties.Monoid.Sum {a ℓ} (M : Monoid a ℓ) where
-
 open Monoid M
   renaming
   ( _∙_       to _+_
diff --git a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
index 35cfcc5ea6..eefb5f40ab 100644
--- a/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
+++ b/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
@@ -8,7 +8,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (IdempotentCommutativeMonoid)
 
 open import Data.Bool as Bool using (Bool; true; false; if_then_else_; _∨_)
 open import Data.Fin.Base using (Fin; zero; suc)
diff --git a/src/Codata/Sized/Conat/Literals.agda b/src/Codata/Sized/Conat/Literals.agda
index 7f0cccb26b..932fd4ab88 100644
--- a/src/Codata/Sized/Conat/Literals.agda
+++ b/src/Codata/Sized/Conat/Literals.agda
@@ -8,9 +8,9 @@
 
 module Codata.Sized.Conat.Literals where
 
-open import Agda.Builtin.FromNat
-open import Data.Unit
-open import Codata.Sized.Conat
+open import Agda.Builtin.FromNat using (Number)
+open import Data.Unit.Base using (⊤)
+open import Codata.Sized.Conat using (Conat; fromℕ)
 
 number : ∀ {i} → Number (Conat i)
 number = record
diff --git a/src/Codata/Sized/Delay/Properties.agda b/src/Codata/Sized/Delay/Properties.agda
index de2b3c95b4..2936660718 100644
--- a/src/Codata/Sized/Delay/Properties.agda
+++ b/src/Codata/Sized/Delay/Properties.agda
@@ -10,7 +10,7 @@ module Codata.Sized.Delay.Properties where
 
 open import Size
 import Data.Sum.Base as Sum
-import Data.Nat as ℕ
+import Data.Nat.Base as ℕ
 open import Codata.Sized.Thunk using (Thunk; force)
 open import Codata.Sized.Conat
 open import Codata.Sized.Conat.Bisimilarity as Coℕ using (zero ; suc)
diff --git a/src/Data/Container/Fixpoints/Sized.agda b/src/Data/Container/Fixpoints/Sized.agda
index abfb877e00..47655af29a 100644
--- a/src/Data/Container/Fixpoints/Sized.agda
+++ b/src/Data/Container/Fixpoints/Sized.agda
@@ -8,10 +8,10 @@
 
 module Data.Container.Fixpoints.Sized where
 
-open import Level
-open import Size
-open import Codata.Sized.M
-open import Data.W.Sized
+open import Level using (Level; _⊔_)
+open import Size using (Size)
+open import Codata.Sized.M using (M)
+open import Data.W.Sized using (W)
 open import Data.Container hiding (μ) public
 
 private
diff --git a/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda
index 58e6966154..a1fc21f44e 100644
--- a/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda
+++ b/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda
@@ -11,7 +11,7 @@ module Data.Container.Indexed.Relation.Binary.Pointwise.Properties where
 open import Axiom.Extensionality.Propositional
 open import Data.Container.Indexed.Core
 open import Data.Container.Indexed.Relation.Binary.Pointwise
-open import Data.Product using (_,_; Σ-syntax; -,_)
+open import Data.Product.Base using (_,_; Σ-syntax; -,_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary
 open import Relation.Binary.PropositionalEquality as P
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 97412c094d..3fa0ebf92f 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -8,7 +8,7 @@
 
 module Data.Fin.Permutation where
 
-open import Data.Bool using (true; false)
+open import Data.Bool.Base using (true; false)
 open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index ff9239359c..e58797ecd1 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -22,7 +22,7 @@ open import Data.Nat.Base as ℕ
   using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; s<s⁻¹; _∸_; _^_)
 import Data.Nat.Properties as ℕ
 open import Data.Nat.Solver
-open import Data.Unit using (⊤; tt)
+open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base as Product
   using (∃; ∃₂; _×_; _,_; map; proj₁; proj₂; uncurry; <_,_>)
 open import Data.Product.Properties using (,-injective)
diff --git a/src/Data/Fin/Substitution/Lemmas.agda b/src/Data/Fin/Substitution/Lemmas.agda
index 05e177acf7..9dedec0ebb 100644
--- a/src/Data/Fin/Substitution/Lemmas.agda
+++ b/src/Data/Fin/Substitution/Lemmas.agda
@@ -9,11 +9,12 @@
 module Data.Fin.Substitution.Lemmas where
 
 open import Data.Fin.Substitution
-open import Data.Nat hiding (_⊔_; _/_)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
 open import Data.Fin.Base using (Fin; zero; suc; lift)
-open import Data.Vec.Base
+open import Data.Vec.Base using (lookup; []; _∷_; map)
 import Data.Vec.Properties as Vec
 open import Function.Base as Fun using (_∘_; _$_; flip)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality.Core as ≡
   using (_≡_; refl; sym; cong; cong₂)
 open import Relation.Binary.PropositionalEquality.Properties
@@ -21,7 +22,6 @@ open import Relation.Binary.PropositionalEquality.Properties
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
   using (Star; ε; _◅_; _▻_)
 open ≡-Reasoning
-open import Level using (Level; _⊔_)
 open import Relation.Unary using (Pred)
 
 private
diff --git a/src/Data/Integer.agda b/src/Data/Integer.agda
index 66c8100242..6e4976f3df 100644
--- a/src/Data/Integer.agda
+++ b/src/Data/Integer.agda
@@ -31,7 +31,7 @@ open import Data.Integer.Properties public
 -- Show
 
 import Data.Nat.Show as ℕ using (show)
-open import Data.Sign as Sign using (Sign)
+open import Data.Sign.Base as Sign using (Sign)
 open import Data.String.Base using (String; _++_)
 
 show : ℤ → String
diff --git a/src/Data/Integer/DivMod.agda b/src/Data/Integer/DivMod.agda
index 687570ba1b..28d15d05fd 100644
--- a/src/Data/Integer/DivMod.agda
+++ b/src/Data/Integer/DivMod.agda
@@ -13,7 +13,6 @@ open import Data.Integer.Properties
 open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s; z<s; s<s)
 import Data.Nat.Properties as ℕ
 import Data.Nat.DivMod as ℕ
-import Data.Sign as S
 open import Function.Base using (_∘′_)
 open import Relation.Nullary.Decidable
 open import Relation.Binary.PropositionalEquality
diff --git a/src/Data/Integer/Divisibility/Signed.agda b/src/Data/Integer/Divisibility/Signed.agda
index 18df0c8a91..f88f3ba859 100644
--- a/src/Data/Integer/Divisibility/Signed.agda
+++ b/src/Data/Integer/Divisibility/Signed.agda
@@ -16,7 +16,7 @@ import Data.Nat.Base as ℕ
 import Data.Nat.Divisibility as ℕ
 import Data.Nat.Coprimality as ℕ
 import Data.Nat.Properties as ℕ
-import Data.Sign as Sign
+import Data.Sign.Base as Sign
 import Data.Sign.Properties as Sign
 open import Level
 open import Relation.Binary.Core using (_⇒_; _Preserves_⟶_)
diff --git a/src/Data/Integer/Literals.agda b/src/Data/Integer/Literals.agda
index 5794f1ceef..d06be38eea 100644
--- a/src/Data/Integer/Literals.agda
+++ b/src/Data/Integer/Literals.agda
@@ -8,9 +8,9 @@
 
 module Data.Integer.Literals where
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.FromNeg
-open import Data.Unit using (⊤)
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.FromNeg using (Negative)
+open import Data.Unit.Base using (⊤)
 open import Data.Integer.Base using (ℤ; -_; +_)
 
 number : Number ℤ
diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda
index d5706b5d53..842058f62e 100644
--- a/src/Data/Integer/Properties.agda
+++ b/src/Data/Integer/Properties.agda
@@ -23,7 +23,7 @@ import Data.Nat.Properties as ℕ
 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)
+open import Data.Sign.Base as Sign using (Sign)
 import Data.Sign.Properties as Sign
 open import Function.Base using (_∘_; _$_; id)
 open import Level using (0ℓ)
diff --git a/src/Data/Integer/Tactic/RingSolver.agda b/src/Data/Integer/Tactic/RingSolver.agda
index affe9ecd2e..d4e1a43536 100644
--- a/src/Data/Integer/Tactic/RingSolver.agda
+++ b/src/Data/Integer/Tactic/RingSolver.agda
@@ -16,7 +16,7 @@ open import Data.Maybe.Base using (just; nothing)
 open import Data.Integer.Base
 open import Data.Integer.Properties
 open import Level using (0ℓ)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Relation.Binary.PropositionalEquality
 import Tactic.RingSolver as Solver
 import Tactic.RingSolver.Core.AlmostCommutativeRing as ACR
diff --git a/src/Data/List/Fresh/Properties.agda b/src/Data/List/Fresh/Properties.agda
index 6619fbb18d..49452e08ee 100644
--- a/src/Data/List/Fresh/Properties.agda
+++ b/src/Data/List/Fresh/Properties.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Fresh.Properties where
 
-open import Level using (Level; _⊔_; Lift)
+open import Level using (Level; _⊔_)
 open import Data.Product.Base using (_,_)
 open import Relation.Nullary
 open import Relation.Unary as U using (Pred)
diff --git a/src/Data/List/Literals.agda b/src/Data/List/Literals.agda
index 6307fe4dc5..80d57901d1 100644
--- a/src/Data/List/Literals.agda
+++ b/src/Data/List/Literals.agda
@@ -8,10 +8,10 @@
 
 module Data.List.Literals where
 
-open import Agda.Builtin.FromString
-open import Data.Unit
-open import Agda.Builtin.Char
-open import Agda.Builtin.List
+open import Agda.Builtin.FromString using (IsString)
+open import Data.Unit.Base using (⊤)
+open import Agda.Builtin.Char using (Char)
+open import Agda.Builtin.List using (List)
 open import Data.String.Base using (toList)
 
 isString : IsString (List Char)
diff --git a/src/Data/List/NonEmpty/Properties.agda b/src/Data/List/NonEmpty/Properties.agda
index 45b27f46c3..68e9bfcf0e 100644
--- a/src/Data/List/NonEmpty/Properties.agda
+++ b/src/Data/List/NonEmpty/Properties.agda
@@ -12,7 +12,7 @@ open import Effect.Monad
 open import Data.Nat
 open import Data.Nat.Properties
 open import Data.Maybe.Properties using (just-injective)
-open import Data.Bool using (Bool; true; false)
+open import Data.Bool.Base using (Bool; true; false)
 open import Data.List.Base as List using (List; []; _∷_; _++_)
 open import Data.List.Effectful using () renaming (monad to listMonad)
 open import Data.List.NonEmpty.Effectful using () renaming (monad to list⁺Monad)
diff --git a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
index 3af753e826..57c9100e02 100644
--- a/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
@@ -30,7 +30,7 @@ import Data.List.Relation.Unary.Unique.Setoid as Unique
 import Data.List.Membership.Setoid as Membership
 open import Data.List.Membership.Setoid.Properties using (∈-∃++; ∈-insert)
 import Data.List.Properties as Lₚ
-open import Data.Nat hiding (_⊔_)
+open import Data.Nat.Base using (ℕ; suc; _<_; z<s; _+_)
 open import Data.Nat.Induction
 open import Data.Nat.Properties
 open import Data.Product.Base using (_,_; _×_; ∃; ∃₂; proj₁; proj₂)
diff --git a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
index 3e91679bb2..f4556c6760 100644
--- a/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
+++ b/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
@@ -25,7 +25,7 @@ import Data.List.Relation.Binary.Subset.Setoid.Properties as Subset
 open import Data.List.Relation.Binary.Subset.Propositional
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Permutation
-open import Data.Nat using (ℕ; _≤_)
+open import Data.Nat.Base using (ℕ; _≤_)
 import Data.Product.Base as Product
 import Data.Sum.Base as Sum
 open import Effect.Monad
diff --git a/src/Data/List/Relation/Unary/Any/Properties.agda b/src/Data/List/Relation/Unary/Any/Properties.agda
index 6383f15a7e..c91a784ff7 100644
--- a/src/Data/List/Relation/Unary/Any/Properties.agda
+++ b/src/Data/List/Relation/Unary/Any/Properties.agda
@@ -20,20 +20,19 @@ open import Data.List.Membership.Propositional.Properties.Core
   using (Any↔; find∘map; map∘find; lose∘find)
 open import Data.List.Relation.Binary.Pointwise
   using (Pointwise; []; _∷_)
-open import Data.Nat using (zero; suc; _<_; z<s; s<s; s≤s)
+open import Data.Nat.Base using (zero; suc; _<_; z<s; s<s; s≤s)
 open import Data.Nat.Properties using (_≟_; ≤∧≢⇒<; ≤-refl; m<n⇒m<1+n)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Maybe.Relation.Unary.Any as MAny using (just)
 open import Data.Product.Base as Product
   using (_×_; _,_; ∃; ∃₂; proj₁; proj₂; uncurry′)
-open import Data.Product.Properties
 open import Data.Product.Function.NonDependent.Propositional
   using (_×-cong_)
 import Data.Product.Function.Dependent.Propositional as Σ
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Effect.Monad
-open import Function.Base
+open import Effect.Monad using (RawMonad)
+open import Function.Base using (_$_; _∘_; flip; const; id; _∘′_)
 open import Function.Bundles
 import Function.Properties.Inverse as Inverse
 open import Function.Related.Propositional as Related using (Kind; Related)
diff --git a/src/Data/List/Relation/Unary/Grouped/Properties.agda b/src/Data/List/Relation/Unary/Grouped/Properties.agda
index 2907b9a665..b0e4e42a4d 100644
--- a/src/Data/List/Relation/Unary/Grouped/Properties.agda
+++ b/src/Data/List/Relation/Unary/Grouped/Properties.agda
@@ -8,7 +8,7 @@
 
 module Data.List.Relation.Unary.Grouped.Properties where
 
-open import Data.Bool using (true; false)
+open import Data.Bool.Base using (true; false)
 open import Data.List.Base using ([]; [_]; _∷_; map; derun)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 import Data.List.Relation.Unary.All.Properties as All
@@ -16,12 +16,12 @@ open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs; []; _
 open import Data.List.Relation.Unary.Grouped
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_; _on_)
+open import Level using (Level)
 open import Relation.Binary.Definitions as B
 open import Relation.Binary.Core using (_⇔_; REL; Rel)
 open import Relation.Unary as U using (Pred)
-open import Relation.Nullary using (¬_; does; yes; no)
-open import Relation.Nullary.Negation using (contradiction)
-open import Level
+open import Relation.Nullary.Decidable.Core using (does; yes; no)
+open import Relation.Nullary.Negation.Core using (¬_; contradiction)
 
 private
   variable
diff --git a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
index 4184647ae2..44039ab152 100644
--- a/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
+++ b/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
@@ -6,17 +6,17 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.List
-import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid
-open import Data.List.Relation.Unary.All.Properties using (all-filter)
-open import Level
 open import Relation.Binary.Definitions using (DecidableEquality)
-open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 module Data.List.Relation.Unary.Unique.DecPropositional.Properties
   {a} {A : Set a} (_≟_ : DecidableEquality A) where
 
+open import Data.List.Base using (deduplicate)
+open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.DecPropositional _≟_
+import Data.List.Relation.Unary.Unique.DecSetoid.Properties as Setoid
+open import Level
+open import Relation.Binary.PropositionalEquality.Properties using (decSetoid)
 
 ------------------------------------------------------------------------
 -- Re-export propositional properties
diff --git a/src/Data/List/Sort/MergeSort.agda b/src/Data/List/Sort/MergeSort.agda
index f476d83b96..529d8623d3 100644
--- a/src/Data/List/Sort/MergeSort.agda
+++ b/src/Data/List/Sort/MergeSort.agda
@@ -10,8 +10,13 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Data.Bool using (true; false)
+open import Relation.Binary.Bundles using (DecTotalOrder)
+
+module Data.List.Sort.MergeSort
+  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
+open import Data.Bool.Base using (true; false)
 open import Data.List.Base
+  using (List; []; _∷_; merge; length; map; [_]; concat; _++_)
 open import Data.List.Properties using (length-partition; ++-assoc; concat-[-])
 open import Data.List.Relation.Unary.Linked using ([]; [-])
 import Data.List.Relation.Unary.Sorted.TotalOrder.Properties as Sorted
@@ -20,17 +25,13 @@ import Data.List.Relation.Unary.All.Properties as All
 open import Data.List.Relation.Binary.Permutation.Propositional
 import Data.List.Relation.Binary.Permutation.Propositional.Properties as Perm
 open import Data.Maybe.Base using (just)
-open import Relation.Nullary.Decidable using (does)
 open import Data.Nat.Base using (_<_; _>_; z<s; s<s)
 open import Data.Nat.Induction
 open import Data.Nat.Properties using (m<n⇒m<1+n)
 open import Data.Product.Base as Product using (_,_)
 open import Function.Base using (_∘_)
-open import Relation.Binary.Bundles using (DecTotalOrder)
-open import Relation.Nullary.Negation using (¬_)
-
-module Data.List.Sort.MergeSort
-  {a ℓ₁ ℓ₂} (O : DecTotalOrder a ℓ₁ ℓ₂) where
+open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open DecTotalOrder O renaming (Carrier to A)
 
diff --git a/src/Data/Maybe.agda b/src/Data/Maybe.agda
index f39d35d2ff..d3f78a7d78 100644
--- a/src/Data/Maybe.agda
+++ b/src/Data/Maybe.agda
@@ -9,10 +9,10 @@
 module Data.Maybe where
 
 open import Data.Empty using (⊥)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Data.Bool.Base using (T)
-open import Data.Maybe.Relation.Unary.All
-open import Data.Maybe.Relation.Unary.Any
+open import Data.Maybe.Relation.Unary.All using (All)
+open import Data.Maybe.Relation.Unary.Any using (Any; just)
 open import Level using (Level)
 
 private
diff --git a/src/Data/Nat/Combinatorics/Specification.agda b/src/Data/Nat/Combinatorics/Specification.agda
index b217ea4143..ac1c6ca1b4 100644
--- a/src/Data/Nat/Combinatorics/Specification.agda
+++ b/src/Data/Nat/Combinatorics/Specification.agda
@@ -10,7 +10,7 @@
 
 module Data.Nat.Combinatorics.Specification where
 
-open import Data.Bool using (T; true; false)
+open import Data.Bool.Base using (T; true; false)
 open import Data.Nat.Base
 open import Data.Nat.DivMod
 open import Data.Nat.Divisibility
diff --git a/src/Data/Nat/Literals.agda b/src/Data/Nat/Literals.agda
index 2c18dc185c..22a53dedeb 100644
--- a/src/Data/Nat/Literals.agda
+++ b/src/Data/Nat/Literals.agda
@@ -8,9 +8,9 @@
 
 module Data.Nat.Literals where
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.Nat
-open import Data.Unit
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.Nat using (Nat)
+open import Data.Unit.Base using (⊤)
 
 number : Number Nat
 number = record
diff --git a/src/Data/Nat/Logarithm.agda b/src/Data/Nat/Logarithm.agda
index 49cdc0f362..48155f1427 100644
--- a/src/Data/Nat/Logarithm.agda
+++ b/src/Data/Nat/Logarithm.agda
@@ -8,7 +8,7 @@
 
 module Data.Nat.Logarithm where
 
-open import Data.Nat
+open import Data.Nat.Base
 open import Data.Nat.Induction using (<-wellFounded)
 open import Data.Nat.Logarithm.Core
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda
index b09b46db7d..e58385f587 100644
--- a/src/Data/Nat/Properties.agda
+++ b/src/Data/Nat/Properties.agda
@@ -24,7 +24,7 @@ open import Data.Bool.Properties using (T?)
 open import Data.Nat.Base
 open import Data.Product.Base using (∃; _×_; _,_)
 open import Data.Sum.Base as Sum
-open import Data.Unit using (tt)
+open import Data.Unit.Base using (tt)
 open import Function.Base
 open import Function.Bundles using (_↣_)
 open import Function.Metric.Nat
diff --git a/src/Data/Nat/PseudoRandom/LCG/Unsafe.agda b/src/Data/Nat/PseudoRandom/LCG/Unsafe.agda
index de8427b6d4..545c30c85f 100644
--- a/src/Data/Nat/PseudoRandom/LCG/Unsafe.agda
+++ b/src/Data/Nat/PseudoRandom/LCG/Unsafe.agda
@@ -9,8 +9,8 @@
 {-# OPTIONS --cubical-compatible --sized-types #-}
 
 open import Codata.Sized.Stream using (Stream; unfold)
-open import Data.Nat.PseudoRandom.LCG
-open import Data.Nat using (ℕ)
+open import Data.Nat.PseudoRandom.LCG using (Generator; step)
+open import Data.Nat.Base using (ℕ)
 open import Data.Product.Base using (<_,_>)
 open import Function.Base using (id)
 
diff --git a/src/Data/Nat/Tactic/RingSolver.agda b/src/Data/Nat/Tactic/RingSolver.agda
index af327ce06c..e55bf6c963 100644
--- a/src/Data/Nat/Tactic/RingSolver.agda
+++ b/src/Data/Nat/Tactic/RingSolver.agda
@@ -16,7 +16,7 @@ open import Data.Maybe.Base using (just; nothing)
 open import Data.Nat.Base using (zero; suc)
 open import Data.Nat.Properties
 open import Level using (0ℓ)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 open import Relation.Binary.PropositionalEquality
 
 import Tactic.RingSolver as Solver
diff --git a/src/Data/Product/Nary/NonDependent.agda b/src/Data/Product/Nary/NonDependent.agda
index 29bb483964..6a04492a5d 100644
--- a/src/Data/Product/Nary/NonDependent.agda
+++ b/src/Data/Product/Nary/NonDependent.agda
@@ -14,7 +14,7 @@ module Data.Product.Nary.NonDependent where
 -- behind the design decisions.
 ------------------------------------------------------------------------
 
-open import Level as L using (Level; _⊔_; Lift; 0ℓ)
+open import Level using (Level)
 open import Agda.Builtin.Unit
 open import Data.Product.Base as Prod
 import Data.Product.Properties as Prodₚ
diff --git a/src/Data/Rational/Literals.agda b/src/Data/Rational/Literals.agda
index 089ed20db0..4162468058 100644
--- a/src/Data/Rational/Literals.agda
+++ b/src/Data/Rational/Literals.agda
@@ -8,9 +8,9 @@
 
 module Data.Rational.Literals where
 
-open import Agda.Builtin.FromNat
-open import Agda.Builtin.FromNeg
-open import Data.Unit using (⊤)
+open import Agda.Builtin.FromNat using (Number)
+open import Agda.Builtin.FromNeg using (Negative)
+open import Data.Unit.Base using (⊤)
 open import Data.Nat.Base using (ℕ; zero)
 open import Data.Nat.Coprimality using (sym; 1-coprimeTo)
 open import Data.Integer.Base using (ℤ; ∣_∣; +_; -_)
diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda
index 6ff6a8bc6d..43088288e2 100644
--- a/src/Data/Rational/Properties.agda
+++ b/src/Data/Rational/Properties.agda
@@ -44,8 +44,7 @@ open import Data.Rational.Unnormalised.Base as ℚᵘ
   )
 import Data.Rational.Unnormalised.Properties as ℚᵘ
 open import Data.Sum.Base as Sum
-open import Data.Unit using (tt)
-import Data.Sign as S
+import Data.Sign.Base as S
 open import Function.Base using (_∘_; _∘′_; _∘₂_; _$_; flip)
 open import Function.Definitions using (Injective)
 open import Level using (0ℓ)
diff --git a/src/Data/Star/BoundedVec.agda b/src/Data/Star/BoundedVec.agda
index 5664cf847d..11f2585e40 100644
--- a/src/Data/Star/BoundedVec.agda
+++ b/src/Data/Star/BoundedVec.agda
@@ -11,15 +11,17 @@
 module Data.Star.BoundedVec where
 
 import Data.Maybe.Base as Maybe
-open import Data.Star.Nat
-open import Data.Star.Decoration
+open import Data.Star.Nat using (ℕ; suc; length)
+open import Data.Star.Decoration using (decoration)
 open import Data.Star.Pointer
+  using (Any; this; that; Pointer; step; done; init)
 open import Data.Star.List using (List)
-open import Data.Unit
+open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (const)
 open import Relation.Binary.Core using (_=[_]⇒_)
-open import Relation.Binary.Consequences
+open import Relation.Binary.Consequences using (map-NonEmpty)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
+  using (gmap; ε; _◅_)
 
 ------------------------------------------------------------------------
 -- The type
diff --git a/src/Data/Star/Decoration.agda b/src/Data/Star/Decoration.agda
index d4e968388b..ce3ef5f7cd 100644
--- a/src/Data/Star/Decoration.agda
+++ b/src/Data/Star/Decoration.agda
@@ -8,9 +8,9 @@
 
 module Data.Star.Decoration where
 
-open import Data.Unit
+open import Data.Unit.Base using (⊤; tt)
 open import Function.Base using (flip)
-open import Level
+open import Level using (Level; suc; _⊔_)
 open import Relation.Binary.Core using (Rel; _=[_]⇒_; _⇒_)
 open import Relation.Binary.Definitions using (NonEmpty; nonEmpty)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
@@ -20,7 +20,6 @@ open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 EdgePred : {ℓ r : Level} (p : Level) {I : Set ℓ} → Rel I r → Set (suc p ⊔ ℓ ⊔ r)
 EdgePred p T = ∀ {i j} → T i j → Set p
 
-
 data NonEmptyEdgePred {ℓ r p : Level} {I : Set ℓ} (T : Rel I r)
                       (P : EdgePred p T) : Set (ℓ ⊔ r ⊔ p) where
   nonEmptyEdgePred : ∀ {i j} {x : T i j}
diff --git a/src/Data/Star/Environment.agda b/src/Data/Star/Environment.agda
index c7ccb18ef4..6d30db7c3c 100644
--- a/src/Data/Star/Environment.agda
+++ b/src/Data/Star/Environment.agda
@@ -8,12 +8,12 @@
 
 module Data.Star.Environment {ℓ} (Ty : Set ℓ) where
 
-open import Level
-open import Data.Star.List
-open import Data.Star.Decoration
-open import Data.Star.Pointer as Pointer hiding (lookup)
-open import Data.Unit
-open import Function.Base hiding (_∋_)
+open import Level using (_⊔_)
+open import Data.Star.List using (List)
+open import Data.Star.Decoration using (All)
+open import Data.Star.Pointer as Pointer using (Any; this; that; result)
+open import Data.Unit.Polymorphic using (⊤)
+open import Function.Base using (const)
 open import Relation.Binary.PropositionalEquality
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
 
@@ -27,7 +27,7 @@ Ctxt = List Ty
 infix 4 _∋_
 
 _∋_ : Ctxt → Ty → Set ℓ
-Γ ∋ σ = Any (const (Lift ℓ ⊤)) (σ ≡_) Γ
+Γ ∋ σ = Any (const (⊤ {ℓ})) (σ ≡_) Γ
 
 vz : ∀ {Γ σ} → Γ ▻ σ ∋ σ
 vz = this refl
diff --git a/src/Data/Star/Fin.agda b/src/Data/Star/Fin.agda
index 9ed437f95f..ded64da4bb 100644
--- a/src/Data/Star/Fin.agda
+++ b/src/Data/Star/Fin.agda
@@ -9,8 +9,8 @@
 module Data.Star.Fin where
 
 open import Data.Star.Nat as ℕ using (ℕ)
-open import Data.Star.Pointer
-open import Data.Unit
+open import Data.Star.Pointer using (Any; this; that)
+open import Data.Unit.Base using (⊤; tt)
 
 -- Finite sets are undecorated pointers into natural numbers.
 
diff --git a/src/Data/Star/List.agda b/src/Data/Star/List.agda
index 358ea7281e..bcc9870375 100644
--- a/src/Data/Star/List.agda
+++ b/src/Data/Star/List.agda
@@ -8,11 +8,12 @@
 
 module Data.Star.List where
 
-open import Data.Star.Nat
-open import Data.Unit
+open import Data.Star.Nat using (ℕ; _+_; zero)
+open import Data.Unit.Base using (tt)
 open import Relation.Binary.Construct.Always using (Always)
 open import Relation.Binary.Construct.Constant using (Const)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
+  using (Star; ε; _◅_; fold)
 
 -- Lists.
 
diff --git a/src/Data/Star/Nat.agda b/src/Data/Star/Nat.agda
index aa1eb9a55b..960537c593 100644
--- a/src/Data/Star/Nat.agda
+++ b/src/Data/Star/Nat.agda
@@ -8,7 +8,7 @@
 
 module Data.Star.Nat where
 
-open import Data.Unit
+open import Data.Unit.Base using (tt)
 open import Function.Base using (const)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
diff --git a/src/Data/Star/Vec.agda b/src/Data/Star/Vec.agda
index 108fbe7399..3677db147b 100644
--- a/src/Data/Star/Vec.agda
+++ b/src/Data/Star/Vec.agda
@@ -8,15 +8,16 @@
 
 module Data.Star.Vec where
 
-open import Data.Star.Nat
+open import Data.Star.Nat using (ℕ; zero; suc; 1#; _+_; length)
 open import Data.Star.Fin using (Fin)
-open import Data.Star.Decoration
-open import Data.Star.Pointer as Pointer hiding (lookup)
+open import Data.Star.Decoration using (All; ↦; _◅◅◅_; decoration)
+open import Data.Star.Pointer as Pointer using (result)
 open import Data.Star.List using (List)
 open import Level using (Level)
 open import Relation.Binary.Construct.Closure.ReflexiveTransitive
-open import Function.Base
-open import Data.Unit
+  using (ε; _◅_; gmap)
+open import Function.Base using (const)
+open import Data.Unit.Base using (tt)
 
 private
   variable
diff --git a/src/Data/String.agda b/src/Data/String.agda
index e92054a673..98b01b3b5f 100644
--- a/src/Data/String.agda
+++ b/src/Data/String.agda
@@ -9,7 +9,7 @@
 module Data.String where
 
 open import Data.Bool.Base using (if_then_else_)
-open import Data.Char as Char using (Char)
+open import Data.Char.Base as Char using (Char)
 open import Function.Base using (_∘_; _$_)
 open import Data.Nat.Base as ℕ using (ℕ)
 import Data.Nat.Properties as ℕ
diff --git a/src/Data/String/Literals.agda b/src/Data/String/Literals.agda
index 9995ceb133..f376958da9 100644
--- a/src/Data/String/Literals.agda
+++ b/src/Data/String/Literals.agda
@@ -8,9 +8,9 @@
 
 module Data.String.Literals where
 
-open import Agda.Builtin.FromString
-open import Data.Unit
-open import Agda.Builtin.String
+open import Agda.Builtin.FromString using (IsString)
+open import Data.Unit.Base using (⊤)
+open import Agda.Builtin.String using (String)
 
 isString : IsString String
 isString = record
diff --git a/src/Data/Tree/AVL/Key.agda b/src/Data/Tree/AVL/Key.agda
index 6fd5a1b021..1c32ef88d7 100644
--- a/src/Data/Tree/AVL/Key.agda
+++ b/src/Data/Tree/AVL/Key.agda
@@ -9,18 +9,16 @@
 
 open import Relation.Binary.Bundles
   using (StrictTotalOrder; StrictPartialOrder)
-open import Relation.Binary.Definitions using (Reflexive)
 
 module Data.Tree.AVL.Key
   {a ℓ₁ ℓ₂} (sto : StrictTotalOrder a ℓ₁ ℓ₂)
   where
 
-open import Level
-open import Data.Empty
-open import Data.Unit
+open import Level using (Level; _⊔_)
 open import Data.Product.Base using (_×_; _,_)
+open import Relation.Binary.Definitions using (Reflexive)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_ ; refl)
-open import Relation.Nullary.Negation using (¬_)
+open import Relation.Nullary.Negation.Core using (¬_)
 open import Relation.Nullary.Construct.Add.Extrema
   as AddExtremaToSet using (_±)
 import Relation.Binary.Construct.Add.Extrema.Equality
diff --git a/src/Data/Tree/AVL/NonEmpty.agda b/src/Data/Tree/AVL/NonEmpty.agda
index 79fd4eb842..ac013e65a7 100644
--- a/src/Data/Tree/AVL/NonEmpty.agda
+++ b/src/Data/Tree/AVL/NonEmpty.agda
@@ -17,15 +17,13 @@ module Data.Tree.AVL.NonEmpty
   {a ℓ₁ ℓ₂} (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) where
 
 open import Data.Bool.Base using (Bool)
-open import Data.Empty
 open import Data.List.NonEmpty as List⁺ using (List⁺; _∷_; _++⁺_)
 open import Data.Maybe.Base hiding (map)
 open import Data.Nat.Base hiding (_<_; _⊔_; compare)
 open import Data.Product.Base hiding (map)
-open import Data.Unit
 open import Function.Base using (_$_; _∘′_)
-open import Level using (_⊔_; Lift; lift)
-open import Relation.Unary
+open import Level using (_⊔_)
+open import Relation.Unary using (IUniversal; _⇒_)
 
 open StrictTotalOrder strictTotalOrder renaming (Carrier to Key)
 open import Data.Tree.AVL.Value Eq.setoid
diff --git a/src/Data/Tree/Binary/Zipper.agda b/src/Data/Tree/Binary/Zipper.agda
index 5786ca7672..3024b125ca 100644
--- a/src/Data/Tree/Binary/Zipper.agda
+++ b/src/Data/Tree/Binary/Zipper.agda
@@ -11,7 +11,7 @@ module Data.Tree.Binary.Zipper where
 open import Level using (Level; _⊔_)
 open import Data.Tree.Binary as BT using (Tree; node; leaf)
 open import Data.List.Base as List using (List; []; _∷_; sum; _++_; [_])
-open import Data.Maybe using (Maybe; nothing; just)
+open import Data.Maybe.Base using (Maybe; nothing; just)
 open import Data.Nat.Base using (ℕ; suc; _+_)
 open import Function.Base using (_$_; _∘_)
 
diff --git a/src/Data/Vec/Bounded.agda b/src/Data/Vec/Bounded.agda
index 881e3b86e1..410e3bebcc 100644
--- a/src/Data/Vec/Bounded.agda
+++ b/src/Data/Vec/Bounded.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Bounded where
 
 open import Level using (Level)
-open import Data.Nat.Base
+open import Data.Nat.Base using (_≤_)
 open import Data.Vec.Base using (Vec)
 import Data.Vec as Vec using (filter; takeWhile; dropWhile)
 open import Function.Base using (id)
diff --git a/src/Data/Vec/Functional/Properties.agda b/src/Data/Vec/Functional/Properties.agda
index 39d9e25abb..addfc32678 100644
--- a/src/Data/Vec/Functional/Properties.agda
+++ b/src/Data/Vec/Functional/Properties.agda
@@ -10,7 +10,7 @@ module Data.Vec.Functional.Properties where
 
 open import Data.Empty using (⊥-elim)
 open import Data.Fin.Base
-open import Data.Nat as ℕ
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product.Base as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.List.Base as List using (List)
diff --git a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
index 28f022454b..f0cefce5c7 100644
--- a/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
+++ b/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
@@ -6,21 +6,20 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (REL)
 open import Relation.Binary.Bundles using (Setoid)
-open import Relation.Binary.Structures using (IsEquivalence)
-open import Relation.Binary.Definitions using (Reflexive; Sym; Trans)
 
 module Data.Vec.Relation.Binary.Equality.Setoid
   {a ℓ} (S : Setoid a ℓ) where
 
 open import Data.Nat.Base using (ℕ; zero; suc; _+_)
-open import Data.Fin using (zero; suc)
+open import Data.Fin.Base using (zero; suc)
 open import Data.Vec.Base
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as PW
   using (Pointwise)
-open import Function.Base
 open import Level using (_⊔_)
+open import Relation.Binary.Core using (REL)
+open import Relation.Binary.Structures using (IsEquivalence)
+open import Relation.Binary.Definitions using (Reflexive; Sym; Trans)
 
 open Setoid S renaming (Carrier to A)
 
diff --git a/src/Data/Vec/Relation/Binary/Lex/Core.agda b/src/Data/Vec/Relation/Binary/Lex/Core.agda
index ed23c7cf6a..92237d4f18 100644
--- a/src/Data/Vec/Relation/Binary/Lex/Core.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/Core.agda
@@ -9,7 +9,7 @@
 module Data.Vec.Relation.Binary.Lex.Core {a} {A : Set a} where
 
 open import Data.Empty
-open import Data.Nat using (ℕ; suc)
+open import Data.Nat.Base using (ℕ; suc)
 import Data.Nat.Properties as ℕ
 open import Data.Product.Base using (_×_; _,_; proj₁; proj₂; uncurry)
 open import Data.Vec.Base using (Vec; []; _∷_)
@@ -136,7 +136,7 @@ module _ {P : Set} {_≈_ : Rel A ℓ₁} {_≺_ : Rel A ℓ₂} where
   module _ (P? : Dec P) (_≈?_ : Decidable _≈_) (_≺?_ : Decidable _≺_) where
 
     decidable : ∀ {m n} → Decidable (_<ₗₑₓ_ {m} {n})
-    decidable {m} {n} xs ys with m Data.Nat.≟ n
+    decidable {m} {n} xs ys with m ℕ.≟ n
     decidable {_} {_} []       []       | yes refl = Dec.map P⇔[]<[] P?
     decidable {_} {_} (x ∷ xs) (y ∷ ys) | yes refl = Dec.map ∷<∷-⇔ ((x ≺? y) ⊎-dec (x ≈? y) ×-dec (decidable xs ys))
     decidable {_} {_} _        _        | no  m≢n    = no (λ xs<ys → contradiction (length-equal xs<ys) m≢n)
diff --git a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
index b273029052..57f05fa211 100644
--- a/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
+++ b/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
@@ -12,14 +12,15 @@
 module Data.Vec.Relation.Binary.Lex.NonStrict where
 
 open import Data.Empty
-open import Data.Unit using (⊤; tt)
+open import Data.Unit.Base using (⊤; tt)
 open import Data.Product.Base using (proj₁; proj₂)
-open import Data.Nat using (ℕ)
+open import Data.Nat.Base using (ℕ)
 open import Data.Vec.Base using (Vec; []; _∷_)
 import Data.Vec.Relation.Binary.Lex.Strict as Strict
 open import Data.Vec.Relation.Binary.Pointwise.Inductive as Pointwise
   using (Pointwise; []; _∷_; head; tail)
 open import Function.Base using (id)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.Core using (REL; Rel; _⇒_)
 open import Relation.Binary.Bundles
   using (Poset; StrictPartialOrder; DecPoset; DecStrictPartialOrder; DecTotalOrder; StrictTotalOrder; Preorder; TotalOrder)
@@ -29,7 +30,6 @@ open import Relation.Binary.Definitions
   using (Irreflexive; _Respects₂_; Antisymmetric; Asymmetric; Symmetric; Trans; Decidable; Total; Trichotomous)
 import Relation.Binary.Construct.NonStrictToStrict as Conv
 open import Relation.Nullary hiding (Irrelevant)
-open import Level using (Level; _⊔_)
 
 private
   variable
diff --git a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
index b13962b750..32eced4f6e 100644
--- a/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
@@ -8,7 +8,7 @@
 
 module Data.Vec.Relation.Unary.AllPairs.Properties where
 
-open import Data.Vec
+open import Data.Vec.Base using (_∷_; map; _++_; concat; take; drop; tabulate)
 import Data.Vec.Properties as Vec
 open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
 import Data.Vec.Relation.Unary.All.Properties as All
diff --git a/src/Effect/Monad/Reader/Indexed.agda b/src/Effect/Monad/Reader/Indexed.agda
index 6ece55aa68..0c787abcc9 100644
--- a/src/Effect/Monad/Reader/Indexed.agda
+++ b/src/Effect/Monad/Reader/Indexed.agda
@@ -6,16 +6,16 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Level
+open import Level using (Level; _⊔_; suc; Lift; lift)
 
 module Effect.Monad.Reader.Indexed {r} (R : Set r) (a : Level) where
 
 open import Function.Base using (const; flip; _∘_)
 open import Function.Identity.Effectful as Id using (Identity)
 open import Effect.Applicative.Indexed
-open import Effect.Monad.Indexed
-open import Effect.Monad
-open import Data.Unit
+  using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
+open import Effect.Monad.Indexed using (RawIMonad; RawIMonadZero;
+  RawIMonadPlus)
 
 private
   variable
diff --git a/src/Effect/Monad/State/Indexed.agda b/src/Effect/Monad/State/Indexed.agda
index 4150554ac9..e8345c363b 100644
--- a/src/Effect/Monad/State/Indexed.agda
+++ b/src/Effect/Monad/State/Indexed.agda
@@ -9,13 +9,15 @@
 module Effect.Monad.State.Indexed where
 
 open import Effect.Applicative.Indexed
-open import Effect.Monad
+  using (IFun; RawIApplicative; RawIApplicativeZero; RawIAlternative)
+open import Effect.Monad using (RawMonad; RawMonadZero; RawMonadPlus)
 open import Function.Identity.Effectful as Id using (Identity)
-open import Effect.Monad.Indexed
+open import Effect.Monad.Indexed using (RawIMonad; RawIMonadZero;
+  RawIMonadPlus)
 open import Data.Product.Base using (_×_; _,_; uncurry)
-open import Data.Unit
-open import Function.Base
-open import Level
+open import Data.Unit.Polymorphic using (⊤)
+open import Function.Base using (const; _∘_)
+open import Level using (Level; _⊔_; suc)
 
 private
   variable
@@ -86,11 +88,11 @@ record RawIMonadState {I : Set i} (S : I → Set f)
   field
     monad : RawIMonad M
     get   : ∀ {i} → M i i (S i)
-    put   : ∀ {i j} → S j → M i j (Lift f ⊤)
+    put   : ∀ {i j} → S j → M i j ⊤
 
   open RawIMonad monad public
 
-  modify : ∀ {i j} → (S i → S j) → M i j (Lift f ⊤)
+  modify : ∀ {i j} → (S i → S j) → M i j ⊤
   modify f = get >>= put ∘ f
 
 StateTIMonadState : ∀ {i f} {I : Set i} (S : I → Set f) {M} →
diff --git a/src/System/Environment/Primitive.agda b/src/System/Environment/Primitive.agda
index 103afc2ac9..c1f8533e03 100644
--- a/src/System/Environment/Primitive.agda
+++ b/src/System/Environment/Primitive.agda
@@ -18,7 +18,7 @@ open import IO.Primitive using (IO)
 open import Data.List.Base using (List)
 open import Data.Maybe.Base using (Maybe)
 open import Data.String.Base using (String)
-open import Data.Unit using (⊤)
+open import Data.Unit.Base using (⊤)
 
 open import Foreign.Haskell.Pair using (Pair)
 
diff --git a/src/Tactic/MonoidSolver.agda b/src/Tactic/MonoidSolver.agda
index 4e370bea25..33cbf95001 100644
--- a/src/Tactic/MonoidSolver.agda
+++ b/src/Tactic/MonoidSolver.agda
@@ -75,10 +75,10 @@ module Tactic.MonoidSolver where
 open import Algebra
 open import Function.Base using (_⟨_⟩_)
 
-open import Data.Bool         as Bool    using (Bool; _∨_; if_then_else_)
-open import Data.Maybe        as Maybe   using (Maybe; just; nothing; maybe)
+open import Data.Bool.Base    as Bool    using (Bool; _∨_; if_then_else_)
+open import Data.Maybe.Base   as Maybe   using (Maybe; just; nothing; maybe)
 open import Data.List.Base    as List    using (List; _∷_; [])
-open import Data.Nat          as ℕ       using (ℕ; suc; zero)
+open import Data.Nat.Base     as ℕ       using (ℕ; suc; zero)
 open import Data.Product.Base as Product using (_×_; _,_)
 
 open import Reflection.AST
diff --git a/src/Tactic/RingSolver/Core/NatSet.agda b/src/Tactic/RingSolver/Core/NatSet.agda
index e297bedbc9..1f42ef708c 100644
--- a/src/Tactic/RingSolver/Core/NatSet.agda
+++ b/src/Tactic/RingSolver/Core/NatSet.agda
@@ -36,10 +36,10 @@
 
 module Tactic.RingSolver.Core.NatSet where
 
-open import Data.Nat        as ℕ     using (ℕ; suc; zero)
+open import Data.Nat.Base   as ℕ     using (ℕ; suc; zero)
 open import Data.List.Base  as List  using (List; _∷_; [])
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
-open import Data.Bool       as Bool  using (Bool)
+open import Data.Bool.Base  as Bool  using (Bool)
 open import Function.Base            using (const; _∘_)
 open import Relation.Binary.PropositionalEquality
 
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
index e71ad07419..32cbefe63a 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Addition
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Nat            as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
+open import Data.Nat.Base       as ℕ using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties as ℕ using (≤′-trans)
 open import Data.Product.Base        using (_,_; _×_; proj₂)
 open import Data.List.Base           using (_∷_; [])
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
index c879bdef38..36c66422c7 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
@@ -13,19 +13,19 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Lemmas
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Bool                                       using (Bool;true;false)
+open import Data.Bool.Base                                  using (Bool;true;false)
 open import Data.Nat.Base as ℕ                              using (ℕ; suc; zero; compare; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Nat.Properties as ℕ                        using (≤′-trans)
 open import Data.Vec.Base as Vec                            using (Vec; _∷_)
-open import Data.Fin                                        using (Fin; zero; suc)
+open import Data.Fin.Base                                   using (Fin; zero; suc)
 open import Data.List.Base                                  using (_∷_; [])
-open import Data.Unit using (tt)
+open import Data.Unit.Base using (tt)
 open import Data.List.Kleene
 open import Data.Product.Base                               using (_,_; proj₁; proj₂; map₁; _×_)
-open import Data.Maybe                                      using (nothing; just)
+open import Data.Maybe.Base                                 using (nothing; just)
 open import Function.Base                                   using (_⟨_⟩_)
 open import Level                                           using (lift)
-open import Relation.Nullary                                using (Dec; yes; no)
+open import Relation.Nullary.Decidable.Core                 using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 
 open Homomorphism homo hiding (_^_)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
index b2a4486d6a..9f6aac7e58 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
@@ -15,7 +15,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Negation
 
 open import Data.Vec.Base         using (Vec)
 open import Data.Product.Base     using (_,_)
-open import Data.Nat              using (_<′_)
+open import Data.Nat.Base         using (_<′_)
 open import Data.Nat.Induction
 
 open import Function.Base using (_⟨_⟩_; flip)
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
index 9fcaca2f66..553f761768 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
@@ -15,7 +15,7 @@ module Tactic.RingSolver.Core.Polynomial.Homomorphism.Variables
 
 open import Data.Product.Base    using (_,_)
 open import Data.Vec.Base as Vec using (Vec)
-open import Data.Fin             using (Fin)
+open import Data.Fin.Base        using (Fin)
 open import Data.List.Kleene
 
 open Homomorphism homo
diff --git a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
index 4e3e672916..c73a8ac587 100644
--- a/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
+++ b/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
@@ -13,7 +13,7 @@ module Tactic.RingSolver.Core.Polynomial.Semantics
   (homo : Homomorphism r₁ r₂ r₃ r₄)
   where
 
-open import Data.Nat          using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
+open import Data.Nat.Base     using (ℕ; suc; zero; _≤′_; ≤′-step; ≤′-refl)
 open import Data.Vec.Base     using (Vec; []; _∷_; uncons)
 open import Data.List.Base    using ([]; _∷_)
 open import Data.Product.Base using (_,_; _×_)
diff --git a/src/Test/Golden.agda b/src/Test/Golden.agda
index 43bbd3037e..7e592a3ff2 100644
--- a/src/Test/Golden.agda
+++ b/src/Test/Golden.agda
@@ -97,7 +97,7 @@ open import Data.Unit.Base using (⊤)
 
 open import Function.Base using (id; _$_; case_of_)
 
-open import Relation.Nullary.Decidable using (does)
+open import Relation.Nullary.Decidable.Core using (does)
 
 open import Codata.Musical.Notation using (♯_)
 open import IO
diff --git a/src/Text/Format.agda b/src/Text/Format.agda
index b597c419cf..ffa6501b27 100644
--- a/src/Text/Format.agda
+++ b/src/Text/Format.agda
@@ -12,11 +12,11 @@ open import Data.Maybe.Base
 open import Text.Format.Generic
 
 -- Formatted types
-open import Data.Char.Base
-open import Data.Integer.Base
-open import Data.Float
-open import Data.Nat.Base
-open import Data.String.Base
+open import Data.Char.Base using (Char)
+open import Data.Integer.Base using (ℤ)
+open import Data.Float.Base using (Float)
+open import Data.Nat.Base using (ℕ)
+open import Data.String.Base using (String)
 
 ------------------------------------------------------------------------
 -- Basic types
diff --git a/src/Text/Pretty/Core.agda b/src/Text/Pretty/Core.agda
index 39910f4dd5..4a5a210fef 100644
--- a/src/Text/Pretty/Core.agda
+++ b/src/Text/Pretty/Core.agda
@@ -16,13 +16,14 @@ open import Data.Bool.Base using (Bool)
 open import Data.Irrelevant as Irrelevant using (Irrelevant) hiding (module Irrelevant)
 open import Data.List.Base as List   using (List; []; _∷_)
 open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
-open import Data.Nat.Properties
+open import Data.Nat.Properties      using (≤-refl; ≤-trans; +-identityʳ;
+  module ≤-Reasoning; m≤n⊔m; +-monoʳ-≤; m≤m⊔n; +-comm; _≤?_)
 open import Data.Product.Base as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
 import Data.Product.Relation.Unary.All as Allᴾ
 
 open import Data.Tree.Binary as Tree using (Tree; leaf; node; #nodes; mapₙ)
 open import Data.Tree.Binary.Relation.Unary.All as Allᵀ using (leaf; node)
-open import Data.Unit using (⊤; tt)
+open import Data.Unit.Base using (⊤; tt)
 import Data.Tree.Binary.Relation.Unary.All.Properties as Allᵀ
 import Data.Tree.Binary.Properties as Tree
 
diff --git a/src/Text/Printf.agda b/src/Text/Printf.agda
index b7f1330c89..caa59b8a8c 100644
--- a/src/Text/Printf.agda
+++ b/src/Text/Printf.agda
@@ -12,7 +12,7 @@ open import Data.String.Base using (String; fromChar; concat)
 open import Function.Base using (id)
 
 import Data.Integer.Show as ℤ
-import Data.Float        as Float
+import Data.Float.Base   as Float
 import Data.Nat.Show     as ℕ
 
 open import Text.Format as Format hiding (Error)