diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda
index c0820fafb7..e64fc4f30b 100644
--- a/src/Algebra/Definitions.agda
+++ b/src/Algebra/Definitions.agda
@@ -109,7 +109,7 @@ _DistributesOver_ : Op₂ A → Op₂ A → Set _
 * DistributesOver + = (* DistributesOverˡ +) × (* DistributesOverʳ +)
 
 _MiddleFourExchange_ : Op₂ A → Op₂ A → Set _
-_*_ MiddleFourExchange _+_ = 
+_*_ MiddleFourExchange _+_ =
   ∀ w x y z → ((w + x) * (y + z)) ≈ ((w + y) * (x + z))
 
 _IdempotentOn_ : Op₂ A → A → Set _
diff --git a/src/Data/Nat/Show.agda b/src/Data/Nat/Show.agda
index 454bc95b76..9f0fdf2bb5 100644
--- a/src/Data/Nat/Show.agda
+++ b/src/Data/Nat/Show.agda
@@ -17,7 +17,7 @@ open import Data.Maybe.Base as Maybe using (Maybe; nothing; _<∣>_; when)
 import Data.Maybe.Effectful as Maybe
 open import Data.Nat
 open import Data.Product using (proj₁)
-open import Data.String as String using (String)
+open import Data.String.Base using (toList; fromList; String)
 open import Function.Base
 open import Relation.Nullary.Decidable using (True)
 
@@ -28,7 +28,7 @@ readMaybe : ∀ base {base≤16 : True (base ≤? 16)} → String → Maybe ℕ
 readMaybe _ "" = nothing
 readMaybe base = Maybe.map convert
               ∘′ TraversableA.mapA Maybe.applicative readDigit
-              ∘′ String.toList
+              ∘′ toList
 
   where
 
@@ -62,7 +62,7 @@ toDecimalChars : ℕ → List Char
 toDecimalChars = List.map toDigitChar ∘′ toNatDigits 10
 
 show : ℕ → String
-show = String.fromList ∘ toDecimalChars
+show = fromList ∘ toDecimalChars
 
 -- Arbitrary base betwen 2 & 16.
 -- Warning: when compiled the time complexity of `showInBase b n` is
@@ -81,5 +81,5 @@ showInBase : (base : ℕ)
              {base≥2 : True (2 ≤? base)}
              {base≤16 : True (base ≤? 16)} →
              ℕ → String
-showInBase base {base≥2} {base≤16} = String.fromList
+showInBase base {base≥2} {base≤16} = fromList
                                    ∘ charsInBase base {base≥2} {base≤16}