diff --git a/hs/config.txt b/hs/config.txt
index 3b445750..b7d0b5ee 100644
--- a/hs/config.txt
+++ b/hs/config.txt
@@ -14,7 +14,7 @@ Decidable
 Lambda
 Properties
 DeBruijn
-Extensions
+More
 Inference
 Untyped
 --
diff --git a/src/plta/Extensions.lagda b/src/plta/More.lagda
similarity index 99%
rename from src/plta/Extensions.lagda
rename to src/plta/More.lagda
index 9d979e96..930501ba 100644
--- a/src/plta/Extensions.lagda
+++ b/src/plta/More.lagda
@@ -1,11 +1,11 @@
 ---
-title     : "Extensions: Extensions to simply-typed lambda calculus"
+title     : "More: More constructs of simply-typed lambda calculus"
 layout    : page
-permalink : /Extensions/
+permalink : /More/
 ---
 
 \begin{code}
-module plta.Extensions where
+module plta.More where
 \end{code}
 
 
diff --git a/src/plta/Statistics.lagda b/src/plta/Statistics.lagda
index 6ba3b802..f783701f 100644
--- a/src/plta/Statistics.lagda
+++ b/src/plta/Statistics.lagda
@@ -29,7 +29,7 @@ Total number of lines and number of lines of Agda code in each chapter
     Lambda                      1300     386
     Properties                  1533     724
     DeBruijn                    1363     627
-    Extensions                   603     524
+    More                         603     524
     Inference                    431     350
     Untyped                      362     281