diff --git a/book/FPLean/TypeClasses/Coercions.lean b/book/FPLean/TypeClasses/Coercions.lean
index 892c8c8..1128f24 100644
--- a/book/FPLean/TypeClasses/Coercions.lean
+++ b/book/FPLean/TypeClasses/Coercions.lean
@@ -32,7 +32,7 @@ tag := "string-path-coercion"
 %%%
 
 In the {ref "handling-input"}[source code to {lit}`feline`], a {moduleName}`String` is converted to a {moduleName}`FilePath` using the anonymous constructor syntax.
-In fact, this was not necessary: Lean defines a coercion from {moduleName}`String` to {moduleName}`FilePath`, so a string can be used in an position where a path is expected.
+In fact, this was not necessary: Lean defines a coercion from {moduleName}`String` to {moduleName}`FilePath`, so a string can be used in a position where a path is expected.
 Even though the function {anchorTerm readFile}`IO.FS.readFile` has type {anchorTerm readFile}`System.FilePath → IO String`, the following code is accepted by Lean:
 
 ```anchor fileDumper