diff --git a/src/Data/Integer/Base.agda b/src/Data/Integer/Base.agda
index 338656956b..9d7e689db0 100644
--- a/src/Data/Integer/Base.agda
+++ b/src/Data/Integer/Base.agda
@@ -14,7 +14,7 @@ module Data.Integer.Base where
 open import Algebra.Bundles.Raw
   using (RawMagma; RawMonoid; RawGroup; RawNearSemiring; RawSemiring; RawRing)
 open import Data.Bool.Base using (Bool; T; true; false)
-open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s)
+open import Data.Nat.Base as ℕ using (ℕ; z≤n; s≤s) hiding (module ℕ)
 open import Data.Sign.Base as Sign using (Sign)
 open import Level using (0ℓ)
 open import Relation.Binary.Core using (Rel)
@@ -140,6 +140,9 @@ record Negative (i : ℤ) : Set where
 
 -- Instances
 
+open ℕ public
+  using (nonZero)
+
 instance
   pos : ∀ {n} → Positive +[1+ n ]
   pos = _
diff --git a/src/Data/Rational/Base.agda b/src/Data/Rational/Base.agda
index 5f5a35e6f9..ebb5ad0ac9 100644
--- a/src/Data/Rational/Base.agda
+++ b/src/Data/Rational/Base.agda
@@ -10,7 +10,9 @@ module Data.Rational.Base where
 
 open import Algebra.Bundles.Raw
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
-open import Data.Integer.Base as ℤ using (ℤ; +_; +0; +[1+_]; -[1+_])
+open import Data.Integer.Base as ℤ
+  using (ℤ; +_; +0; +[1+_]; -[1+_])
+  hiding (module ℤ)
 open import Data.Nat.GCD
 open import Data.Nat.Coprimality as C
   using (Coprime; Bézout-coprime; coprime-/gcd; coprime?; ¬0-coprimeTo-2+)
@@ -176,6 +178,11 @@ NonPositive p = ℚᵘ.NonPositive (toℚᵘ p)
 NonNegative : Pred ℚ 0ℓ
 NonNegative p = ℚᵘ.NonNegative (toℚᵘ p)
 
+-- Instances
+
+open ℤ public
+  using (nonZero; pos; nonNeg; nonPos0; nonPos; neg)
+
 -- Constructors
 
 ≢-nonZero : ∀ {p} → p ≢ 0ℚ → NonZero p
diff --git a/src/Data/Rational/Unnormalised/Base.agda b/src/Data/Rational/Unnormalised/Base.agda
index dc5bd144dc..c9fcb8d54d 100644
--- a/src/Data/Rational/Unnormalised/Base.agda
+++ b/src/Data/Rational/Unnormalised/Base.agda
@@ -12,6 +12,7 @@ open import Algebra.Bundles.Raw
 open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Integer.Base as ℤ
   using (ℤ; +_; +0; +[1+_]; -[1+_]; +<+; +≤+)
+  hiding (module ℤ)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc)
 open import Level using (0ℓ)
 open import Relation.Nullary.Negation.Core using (¬_; contradiction)
@@ -149,6 +150,11 @@ NonPositive p = ℤ.NonPositive (↥ p)
 NonNegative : Pred ℚᵘ 0ℓ
 NonNegative p = ℤ.NonNegative (↥ p)
 
+-- Instances
+
+open ℤ public
+  using (nonZero; pos; nonNeg; nonPos0; nonPos; neg)
+
 -- Constructors and destructors
 
 -- Note: these could be proved more elegantly using the constructors