diff --git a/doc/README/Effect/Monad/Partiality.agda b/doc/README/Effect/Monad/Partiality.agda
new file mode 100644
index 0000000000..7b96749cd5
--- /dev/null
+++ b/doc/README/Effect/Monad/Partiality.agda
@@ -0,0 +1,27 @@
+-----------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Example showing the use of the partiality Monad
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe --guardedness #-}
+
+module README.Effect.Monad.Partiality where
+
+open import Codata.Musical.Notation using (♯_)
+open import Data.Bool.Base using (false; true)
+open import Data.Nat using (ℕ; _+_; _∸_; _≤?_)
+open import Effect.Monad.Partiality
+open import Relation.Nullary.Decidable using (does)
+
+open Workaround
+
+-- McCarthy's f91:
+
+f91′ : ℕ → ℕ ⊥P
+f91′ n with does (n ≤? 100)
+... | true  = later (♯ (f91′ (11 + n) >>= f91′))
+... | false = now (n ∸ 10)
+
+f91 : ℕ → ℕ ⊥
+f91 n = ⟦ f91′ n ⟧P
diff --git a/src/Algebra/Module/Construct/Idealization.agda b/src/Algebra/Module/Construct/Idealization.agda
index 0526f059fd..4a393ea879 100644
--- a/src/Algebra/Module/Construct/Idealization.agda
+++ b/src/Algebra/Module/Construct/Idealization.agda
@@ -43,9 +43,11 @@ import Algebra.Definitions as Definitions
 import Algebra.Module.Construct.DirectProduct as DirectProduct
 import Algebra.Module.Construct.TensorUnit as TensorUnit
 open import Algebra.Structures using (IsAbelianGroup; IsRing)
-open import Data.Product using (_,_; ∃-syntax)
+open import Data.Product.Base using (_,_; ∃-syntax)
 open import Level using (Level; _⊔_)
-open import Relation.Binary using (Rel; Setoid; IsEquivalence)
+open import Relation.Binary.Bundles using  (Setoid)
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Structures using (IsEquivalence)
 import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
 
 ------------------------------------------------------------------------
diff --git a/src/Algebra/Properties/CommutativeMonoid.agda b/src/Algebra/Properties/CommutativeMonoid.agda
index e83be61ac7..cef85545a1 100644
--- a/src/Algebra/Properties/CommutativeMonoid.agda
+++ b/src/Algebra/Properties/CommutativeMonoid.agda
@@ -6,9 +6,9 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra.Bundles
-open import Algebra.Definitions
-open import Data.Product using (_,_; proj₂)
+open import Algebra.Bundles using (CommutativeMonoid)
+open import Algebra.Definitions using (LeftInvertible; RightInvertible; Invertible)
+open import Data.Product.Base using (_,_; proj₂)
 
 module Algebra.Properties.CommutativeMonoid
   {g₁ g₂} (M : CommutativeMonoid g₁ g₂) where
diff --git a/src/Data/Container/Core.agda b/src/Data/Container/Core.agda
index 006f433d2e..07afabe2eb 100644
--- a/src/Data/Container/Core.agda
+++ b/src/Data/Container/Core.agda
@@ -8,10 +8,10 @@
 
 module Data.Container.Core where
 
-open import Level
+open import Level using (Level; _⊔_; suc)
 open import Data.Product.Base as Product using (Σ-syntax)
-open import Function.Base
-open import Function using (Inverse; _↔_)
+open import Function.Base using (_∘_; _∘′_)
+open import Function.Bundles using (Inverse; _↔_)
 open import Relation.Unary using (Pred; _⊆_)
 
 -- Definition of Containers
diff --git a/src/Data/Container/Indexed.agda b/src/Data/Container/Indexed.agda
index b34657a4be..f99fef80dc 100644
--- a/src/Data/Container/Indexed.agda
+++ b/src/Data/Container/Indexed.agda
@@ -11,14 +11,14 @@
 
 module Data.Container.Indexed where
 
-open import Level
+open import Level using (Level; zero; _⊔_)
 open import Data.Product.Base as Prod hiding (map)
-open import Data.W.Indexed
+open import Data.W.Indexed using (W)
 open import Function.Base renaming (id to ⟨id⟩; _∘_ to _⟨∘⟩_)
-open import Function using (_↔_; Inverse)
+open import Function.Bundles using (_↔_; Inverse)
 open import Relation.Unary using (Pred; _⊆_)
 open import Relation.Binary.Core using (Rel; REL)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; refl; trans; subst)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; _≗_; refl; trans; subst)
 
 ------------------------------------------------------------------------
 
diff --git a/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda b/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda
index afaba23f09..4afafefbb9 100644
--- a/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda
+++ b/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda
@@ -8,11 +8,11 @@
 
 module Data.Container.Indexed.Relation.Binary.Pointwise where
 
-open import Data.Product using (_,_; Σ-syntax)
-open import Function
+open import Data.Product.Base using (_,_; Σ-syntax)
+open import Function.Base using (_∘_)
 open import Level using (Level; _⊔_)
 open import Relation.Binary using (REL; _⇒_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 open import Data.Container.Indexed.Core using (Container; Subtrees; ⟦_⟧)
 
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 0cda410424..2d3c9e20e0 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -23,7 +23,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
 open import Data.Nat.Base
-open import Data.Nat.Divisibility
+open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product.Base as Product
   using (_×_; _,_; uncurry; uncurry′; proj₁; proj₂; <_,_>)
diff --git a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
index fca4f2793d..b4d2a97d90 100644
--- a/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
+++ b/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
@@ -13,10 +13,10 @@ module Data.List.Relation.Ternary.Appending.Setoid.Properties
   where
 
 open import Data.List.Base as List using (List; [])
-import Data.List.Properties as Listₚ
+import Data.List.Properties as List
 open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise; [])
 import Data.List.Relation.Ternary.Appending.Properties as Appendingₚ
-open import Data.Product using (∃-syntax; _×_; _,_)
+open import Data.Product.Base using (∃-syntax; _×_; _,_)
 open import Function.Base using (id)
 open import Relation.Binary.Core using (_⇒_)
 open import Relation.Binary.PropositionalEquality.Core using (refl)
@@ -45,7 +45,7 @@ open Appendingₚ public
 ++[]⁻¹ : Appending as [] cs → Pointwise _≈_ as cs
 ++[]⁻¹ {as} {cs} ls with break ls
 ... | cs₁ , cs₂ , refl , pw , []
-  rewrite Listₚ.++-identityʳ cs₁
+  rewrite List.++-identityʳ cs₁
   = pw
 
 respʳ-≋ : ∀ {cs′} → Appending as bs cs → Pointwise _≈_ cs cs′ →
diff --git a/src/Data/List/Relation/Unary/First/Properties.agda b/src/Data/List/Relation/Unary/First/Properties.agda
index d598f14469..0f70a7659c 100644
--- a/src/Data/List/Relation/Unary/First/Properties.agda
+++ b/src/Data/List/Relation/Unary/First/Properties.agda
@@ -8,7 +8,6 @@
 
 module Data.List.Relation.Unary.First.Properties where
 
-open import Data.Empty
 open import Data.Fin.Base using (suc)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -16,9 +15,9 @@ open import Data.List.Relation.Unary.Any as Any using (here; there)
 open import Data.List.Relation.Unary.First
 import Data.Sum as Sum
 open import Function.Base using (_∘′_; _$_; _∘_; id)
-open import Relation.Binary.PropositionalEquality as ≡ using (_≡_; refl; _≗_)
-open import Relation.Unary
-open import Relation.Nullary.Negation
+open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
+open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
+open import Relation.Nullary.Negation using (contradiction)
 
 ------------------------------------------------------------------------
 -- map
@@ -52,7 +51,7 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   All⇒¬First : P ⊆ ∁ Q → All P ⊆ ∁ (First P Q)
-  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = ⊥-elim (p⇒¬q px qx)
+  All⇒¬First p⇒¬q (px ∷ pxs) [ qx ]   = contradiction qx (p⇒¬q px)
   All⇒¬First p⇒¬q (_ ∷ pxs)  (_ ∷ hf) = All⇒¬First p⇒¬q pxs hf
 
   First⇒¬All : Q ⊆ ∁ P → First P Q ⊆ ∁ (All P)
@@ -64,16 +63,16 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
 
   unique-index : ∀ {xs} → P ⊆ ∁ Q → (f₁ f₂ : First P Q xs) → index f₁ ≡ index f₂
   unique-index p⇒¬q [ _ ]    [ _ ]    = refl
-  unique-index p⇒¬q [ qx ]   (px ∷ _) = ⊥-elim (p⇒¬q px qx)
-  unique-index p⇒¬q (px ∷ _) [ qx ]   = ⊥-elim (p⇒¬q px qx)
+  unique-index p⇒¬q [ qx ]   (px ∷ _) = contradiction qx (p⇒¬q px)
+  unique-index p⇒¬q (px ∷ _) [ qx ]   = contradiction qx (p⇒¬q px)
   unique-index p⇒¬q (_ ∷ f₁) (_ ∷ f₂) = ≡.cong suc (unique-index p⇒¬q f₁ f₂)
 
   irrelevant : P ⊆ ∁ Q → Irrelevant P → Irrelevant Q → Irrelevant (First P Q)
-  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    [ qx₂ ]    = ≡.cong [_] (q-irr qx₁ qx₂)
-  irrelevant p⇒¬q p-irr q-irr [ qx₁ ]    (px₂ ∷ f₂) = ⊥-elim (p⇒¬q px₂ qx₁)
-  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) [ qx₂ ]    = ⊥-elim (p⇒¬q px₁ qx₂)
-  irrelevant p⇒¬q p-irr q-irr (px₁ ∷ f₁) (px₂ ∷ f₂) =
-    ≡.cong₂ _∷_ (p-irr px₁ px₂) (irrelevant p⇒¬q p-irr q-irr f₁ f₂)
+  irrelevant p⇒¬q p-irr q-irr [ px ]    [ qx ]    = ≡.cong [_] (q-irr px qx)
+  irrelevant p⇒¬q p-irr q-irr [ qx ]    (px ∷ _)  = contradiction qx (p⇒¬q px)
+  irrelevant p⇒¬q p-irr q-irr (px ∷ _)  [ qx ]    = contradiction qx (p⇒¬q px)
+  irrelevant p⇒¬q p-irr q-irr (px ∷ f)  (qx ∷ g) =
+    ≡.cong₂ _∷_ (p-irr px qx) (irrelevant p⇒¬q p-irr q-irr f g)
 
 ------------------------------------------------------------------------
 -- Decidability
diff --git a/src/Data/Nat/Primality/Factorisation.agda b/src/Data/Nat/Primality/Factorisation.agda
index 6dda6bac9d..66e75dd4df 100644
--- a/src/Data/Nat/Primality/Factorisation.agda
+++ b/src/Data/Nat/Primality/Factorisation.agda
@@ -8,13 +8,16 @@
 
 module Data.Nat.Primality.Factorisation where
 
-open import Data.Empty using (⊥-elim)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility
+  using (_∣?_; quotient; quotient>1; quotient-<; quotient-∣; m∣n⇒n≡m*quotient; _∣_; ∣1⇒≡1;
+        divides)
 open import Data.Nat.Properties
 open import Data.Nat.Induction using (<-Rec; <-rec; <-recBuilder)
 open import Data.Nat.Primality
-open import Data.Product as Π using (∃-syntax; _×_; _,_; proj₁; proj₂)
+  using (Prime; _Rough_; rough∧square>⇒prime; ∤⇒rough-suc; rough∧∣⇒rough; rough∧∣⇒prime;
+         2-rough; euclidsLemma; prime⇒irreducible; ¬prime[1]; productOfPrimes≥1; prime⇒nonZero)
+open import Data.Product.Base using (∃-syntax; _×_; _,_; proj₁; proj₂)
 open import Data.List.Base using (List; []; _∷_; _++_; product)
 open import Data.List.Membership.Propositional using (_∈_)
 open import Data.List.Membership.Propositional.Properties using (∈-∃++)
@@ -22,14 +25,16 @@ open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (here; there)
 open import Data.List.Relation.Binary.Permutation.Propositional
   using (_↭_; prep; swap; ↭-reflexive; ↭-refl; ↭-trans; refl; module PermutationReasoning)
-open import Data.List.Relation.Binary.Permutation.Propositional.Properties using (product-↭; All-resp-↭; shift)
+open import Data.List.Relation.Binary.Permutation.Propositional.Properties
+  using (product-↭; All-resp-↭; shift)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Function.Base using (_$_; _∘_; _|>_; flip)
 open import Induction using (build)
 open import Induction.Lexicographic using (_⊗_; [_⊗_])
 open import Relation.Nullary.Decidable using (yes; no)
 open import Relation.Nullary.Negation using (contradiction)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
+open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; sym; trans; cong; module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
index 6c8004b559..1cba24520a 100644
--- a/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
+++ b/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
@@ -9,13 +9,16 @@
 module Data.Product.Relation.Binary.Pointwise.NonDependent where
 
 open import Data.Product.Base as Product
-open import Data.Product.Properties using (≡-dec)
-open import Data.Sum.Base
-open import Data.Unit.Base using (⊤)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Level using (Level; _⊔_; 0ℓ)
-open import Function
+open import Function.Base using (_on_; id)
+open import Function.Bundles using (Inverse)
 open import Relation.Nullary.Decidable using (_×-dec_)
-open import Relation.Binary
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Bundles
+  using (Setoid; DecSetoid; Preorder; Poset; StrictPartialOrder)
+open import Relation.Binary.Definitions
+open import Relation.Binary.Structures
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
 
diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda
index c9fcb8d54d..41c236062c 100644
--- a/src/Data/Rational/Unnormalised/Base.agda
+++ b/src/Data/Rational/Unnormalised/Base.agda
@@ -9,6 +9,7 @@
 module Data.Rational.Unnormalised.Base where
 
 open import Algebra.Bundles.Raw
+  using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)
diff --git a/src/Data/Sum/Algebra.agda b/src/Data/Sum/Algebra.agda
index f128af8075..ab51bece88 100644
--- a/src/Data/Sum/Algebra.agda
+++ b/src/Data/Sum/Algebra.agda
@@ -8,12 +8,16 @@
 
 module Data.Sum.Algebra where
 
-open import Algebra
+open import Algebra.Bundles
+  using (Magma; Semigroup; Monoid; CommutativeMonoid)
+open import Algebra.Definitions
+open import Algebra.Structures
+  using (IsMagma; IsSemigroup; IsMonoid; IsCommutativeMonoid)
 open import Data.Empty.Polymorphic using (⊥)
 open import Data.Product.Base using (_,_)
-open import Data.Sum.Base
-open import Data.Sum.Properties
-open import Data.Unit.Polymorphic using (⊤; tt)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂; map; [_,_]; swap; assocʳ; assocˡ)
+open import Data.Sum.Properties using (swap-involutive)
+open import Data.Unit.Polymorphic.Base using (⊤; tt)
 open import Function.Base using (id; _∘_)
 open import Function.Properties.Inverse using (↔-isEquivalence)
 open import Function.Bundles using (_↔_; Inverse; mk↔ₛ′)
diff --git a/src/Data/Sum/Function/Propositional.agda b/src/Data/Sum/Function/Propositional.agda
index b7830bc895..25bb1a0907 100644
--- a/src/Data/Sum/Function/Propositional.agda
+++ b/src/Data/Sum/Function/Propositional.agda
@@ -8,15 +8,18 @@
 
 module Data.Sum.Function.Propositional where
 
-open import Data.Sum.Base
+open import Data.Sum.Base using (_⊎_)
 open import Data.Sum.Function.Setoid
 open import Data.Sum.Relation.Binary.Pointwise using (Pointwise-≡↔≡; _⊎ₛ_)
 open import Function.Construct.Composition as Compose
 open import Function.Related.Propositional
-open import Function
+open import Function.Base using (id)
+open import Function.Bundles
+  using (Inverse; _⟶_; _⇔_; _↣_; _↠_; _↩_; _↪_; _⤖_; _↔_)
 open import Function.Properties.Inverse as Inv
 open import Level using (Level; _⊔_)
-open import Relation.Binary using (REL; Setoid)
+open import Relation.Binary.Core using (REL)
+open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.PropositionalEquality using (setoid)
 
 private
diff --git a/src/Data/Unit/Polymorphic/Properties.agda b/src/Data/Unit/Polymorphic/Properties.agda
index 87519aa9ee..ad2ccc3a05 100644
--- a/src/Data/Unit/Polymorphic/Properties.agda
+++ b/src/Data/Unit/Polymorphic/Properties.agda
@@ -23,6 +23,7 @@ open import Relation.Binary.Structures
 open import Relation.Binary.Definitions
   using (Decidable; Antisymmetric; Total)
 open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; trans; decSetoid; setoid; isEquivalence)
 
 private
   variable
diff --git a/src/Effect/Monad/Partiality.agda b/src/Effect/Monad/Partiality.agda
index c0723f1370..3143d0d7ad 100644
--- a/src/Effect/Monad/Partiality.agda
+++ b/src/Effect/Monad/Partiality.agda
@@ -8,15 +8,15 @@
 
 module Effect.Monad.Partiality where
 
-open import Codata.Musical.Notation
-open import Effect.Functor
-open import Effect.Applicative
-open import Effect.Monad
+open import Codata.Musical.Notation using (∞; ♯_; ♭)
+open import Effect.Functor using (RawFunctor)
+open import Effect.Applicative using (RawApplicative)
+open import Effect.Monad using (RawMonad; module Join)
 open import Data.Bool.Base using (Bool; false; true)
-open import Data.Nat using (ℕ; zero; suc; _+_)
-open import Data.Product as Prod hiding (map)
+open import Data.Nat.Base using (ℕ; zero; suc; _+_)
+open import Data.Product as Prod using (∃; ∄; -,_; ∃₂; _,_; _×_)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
-open import Function.Base
+open import Function.Base using (_∘′_; flip; id; _∘_; _$_; _⟨_⟩_)
 open import Function.Bundles using (_⇔_; mk⇔)
 open import Level using (Level; _⊔_)
 open import Relation.Binary.Core as B hiding (Rel; _⇔_)
@@ -29,9 +29,8 @@ open import Relation.Binary.Bundles
 import Relation.Binary.Properties.Setoid as SetoidProperties
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 import Relation.Binary.PropositionalEquality.Properties as ≡
-open import Relation.Nullary
-open import Relation.Nullary.Decidable hiding (map)
-open import Relation.Nullary.Negation
+open import Relation.Nullary.Decidable using (yes; no; False; Dec; ¬¬-excluded-middle)
+open import Relation.Nullary.Negation using (¬_; ¬¬-Monad)
 
 private
   variable
@@ -934,22 +933,3 @@ idempotent {A = A} B x f = sound (idem x)
                                                      laterˡ (refl (Setoid.refl B))) ⟩
     (♭ x >>= λ y′ →     ♭ x >>= λ y″ → f y′ y″)  ≳⟨ idem (♭ x) ⟩≅
     (♭ x >>= λ y′ → f y′ y′)                     ∎))
-
-------------------------------------------------------------------------
--- Example
-
-private
- module Example where
-
-  open Data.Nat
-  open Workaround
-
-  -- McCarthy's f91:
-
-  f91′ : ℕ → ℕ ⊥P
-  f91′ n with does (n ≤? 100)
-  ... | true  = later (♯ (f91′ (11 + n) >>= f91′))
-  ... | false = now (n ∸ 10)
-
-  f91 : ℕ → ℕ ⊥
-  f91 n = ⟦ f91′ n ⟧P
diff --git a/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda b/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
index 4ea2965f99..05c20b9682 100644
--- a/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
+++ b/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
@@ -8,10 +8,12 @@
 
 module Function.Properties.Inverse.HalfAdjointEquivalence where
 
-open import Function.Base
-open import Function
-open import Level
+open import Function.Base using (id; _∘_)
+open import Function.Bundles using (Inverse; _↔_; mk↔ₛ′)
+open import Level using (Level; _⊔_)
 open import Relation.Binary.PropositionalEquality
+  using (_≡_; refl; cong; sym; trans; trans-reflʳ; cong-≡id; cong-∘; naturality;
+         cong-id; trans-assoc; trans-symˡ; module ≡-Reasoning)
 
 private
   variable
diff --git a/src/Function/Related/TypeIsomorphisms.agda b/src/Function/Related/TypeIsomorphisms.agda
index eafe0b50b6..3386032654 100644
--- a/src/Function/Related/TypeIsomorphisms.agda
+++ b/src/Function/Related/TypeIsomorphisms.agda
@@ -13,15 +13,14 @@ open import Algebra
 open import Algebra.Structures.Biased using (isCommutativeSemiringˡ)
 open import Axiom.Extensionality.Propositional using (Extensionality)
 open import Data.Bool.Base using (true; false)
-open import Data.Empty using (⊥-elim)
-open import Data.Empty.Polymorphic using (⊥) renaming (⊥-elim to ⊥ₚ-elim)
+open import Data.Empty.Polymorphic using (⊥; ⊥-elim)
 open import Data.Product.Base as Product
   using (_×_; Σ; curry; uncurry; _,_; -,_; <_,_>; proj₁; proj₂; ∃₂; ∃)
 open import Data.Product.Function.NonDependent.Propositional
 open import Data.Sum.Base as Sum
 open import Data.Sum.Properties using (swap-involutive)
 open import Data.Sum.Function.Propositional using (_⊎-cong_)
-open import Data.Unit.Polymorphic using (⊤)
+open import Data.Unit.Polymorphic.Base using (⊤)
 open import Level using (Level; Lift; 0ℓ; suc)
 open import Function.Base
 open import Function.Bundles
@@ -32,7 +31,7 @@ open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; cong)
 open import Relation.Binary.PropositionalEquality.Properties
   using (module ≡-Reasoning)
 open import Relation.Nullary.Reflects using (invert)
-open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ)
+open import Relation.Nullary using (Dec; ¬_; _because_; ofⁿ; contradiction)
 import Relation.Nullary.Indexed as I
 open import Relation.Nullary.Decidable using (True)
 
@@ -68,10 +67,10 @@ private
 -- × has ⊥ has its zero
 
 ×-zeroˡ : ∀ ℓ → LeftZero {ℓ = ℓ} _↔_ ⊥ _×_
-×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥ₚ-elim > (λ _ → refl) (λ { () })
+×-zeroˡ ℓ A = mk↔ₛ′ proj₁ < id , ⊥-elim > (λ _ → refl) (λ { () })
 
 ×-zeroʳ : ∀ ℓ → RightZero {ℓ = ℓ} _↔_ ⊥ _×_
-×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥ₚ-elim , id > (λ _ → refl) (λ { () })
+×-zeroʳ ℓ A = mk↔ₛ′ proj₂ < ⊥-elim , id > (λ _ → refl) (λ { () })
 
 ×-zero : ∀ ℓ → Zero _↔_ ⊥ _×_
 ×-zero ℓ  = ×-zeroˡ ℓ , ×-zeroʳ ℓ
@@ -332,4 +331,4 @@ True↔ : ∀ {p} {P : Set p}
 True↔ ( true because  [p]) irr =
   mk↔ₛ′ (λ _ → invert [p]) (λ _ → _) (irr _) (λ _ → refl)
 True↔ (false because ofⁿ ¬p) _ =
-  mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (⊥-elim ∘ ¬p) (λ ())
+  mk↔ₛ′ (λ()) (invert (ofⁿ ¬p)) (λ x → flip contradiction ¬p x) (λ ())
diff --git a/src/Relation/Binary/Reasoning/Base/Apartness.agda b/src/Relation/Binary/Reasoning/Base/Apartness.agda
index 22eee2d505..d3a850eca7 100644
--- a/src/Relation/Binary/Reasoning/Base/Apartness.agda
+++ b/src/Relation/Binary/Reasoning/Base/Apartness.agda
@@ -8,7 +8,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level using (Level; _⊔_)
-open import Function using (case_of_)
+open import Function.Base using (case_of_)
 open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Structures using (IsEquivalence)
diff --git a/src/Relation/Binary/Reasoning/Base/Double.agda b/src/Relation/Binary/Reasoning/Base/Double.agda
index b5fd9f66e4..0c1ae9b60c 100644
--- a/src/Relation/Binary/Reasoning/Base/Double.agda
+++ b/src/Relation/Binary/Reasoning/Base/Double.agda
@@ -11,7 +11,7 @@
 {-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level using (_⊔_)
-open import Function using (case_of_)
+open import Function.Base using (case_of_)
 open import Relation.Nullary.Decidable.Core using (Dec; yes; no)
 open import Relation.Binary.Core using (Rel; _⇒_)
 open import Relation.Binary.Definitions using (Reflexive; Trans)
diff --git a/src/Relation/Binary/Reasoning/Base/Partial.agda b/src/Relation/Binary/Reasoning/Base/Partial.agda
index 3d24edf501..5da6792f64 100644
--- a/src/Relation/Binary/Reasoning/Base/Partial.agda
+++ b/src/Relation/Binary/Reasoning/Base/Partial.agda
@@ -6,10 +6,10 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Function using (case_of_)
+open import Function.Base using (case_of_)
 open import Level using (_⊔_)
-open import Relation.Binary.Core
-open import Relation.Binary.Definitions
+open import Relation.Binary.Core using (Rel)
+open import Relation.Binary.Definitions using (Transitive; Trans; Reflexive)
 open import Relation.Nullary.Decidable using (Dec; yes; no)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_)
 open import Relation.Binary.Reasoning.Syntax
diff --git a/src/Relation/Binary/Reasoning/Base/Triple.agda b/src/Relation/Binary/Reasoning/Base/Triple.agda
index 6afb937497..3433e58063 100644
--- a/src/Relation/Binary/Reasoning/Base/Triple.agda
+++ b/src/Relation/Binary/Reasoning/Base/Triple.agda
@@ -12,7 +12,7 @@
 
 open import Data.Product.Base using (proj₁; proj₂)
 open import Level using (_⊔_)
-open import Function using (case_of_)
+open import Function.Base using (case_of_)
 open import Relation.Nullary.Decidable.Core
   using (Dec; yes; no)
 open import Relation.Binary.Core using (Rel; _⇒_)