diff --git a/extra/extra/Confluence.lagda b/extra/extra/Confluence.lagda
index 8f978522..e7879670 100644
--- a/extra/extra/Confluence.lagda
+++ b/extra/extra/Confluence.lagda
@@ -1,13 +1,21 @@
+---
+title     : "Substitution in the untyped lambda calculus"
+layout    : page
+prev      : /Substitution/
+permalink : /Confluence/
+next      : /Denotational/
+---
+
 \begin{code}
-module extra.Confluence where
+module plfa.Confluence where
 \end{code}
 
 ## Imports
 
 \begin{code}
-open import extra.Substitution
+open import plfa.Substitution
     using (subst-commute; rename-subst-commute)
-open import extra.LambdaReduction
+open import plfa.LambdaReduction
     using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _[];
            abs-cong; appL-cong; appR-cong;
            —↠-trans)
diff --git a/src/plfa/Adequacy.lagda b/src/plfa/Adequacy.lagda
index 38b1c6c6..04b3c629 100644
--- a/src/plfa/Adequacy.lagda
+++ b/src/plfa/Adequacy.lagda
@@ -3,7 +3,7 @@ title     : "Adequacy: of denotational semantics with respect to operational sem
 layout    : page
 prev      : /Soundness/
 permalink : /Adequacy/
-next      : /Acknowledgements/
+next      : /CallByName/
 ---
 
 \begin{code}
diff --git a/extra/extra/CallByName.lagda b/src/plfa/CallByName.lagda
similarity index 97%
rename from extra/extra/CallByName.lagda
rename to src/plfa/CallByName.lagda
index aa5bf3ba..fad34173 100644
--- a/extra/extra/CallByName.lagda
+++ b/src/plfa/CallByName.lagda
@@ -1,3 +1,11 @@
+---
+title     : "Call by name reduction of the untyped lambda calculus"
+layout    : page
+prev      : /Adequacy/
+permalink : /CallByName/
+next      : /Acknowledgements/
+---
+
 \begin{code}
 module plfa.CallByName where
 \end{code}
diff --git a/extra/extra/LambdaReduction.lagda b/src/plfa/LambdaReduction.lagda
similarity index 100%
rename from extra/extra/LambdaReduction.lagda
rename to src/plfa/LambdaReduction.lagda
diff --git a/src/plfa/Soundness.lagda b/src/plfa/Soundness.lagda
index 9959d17e..b3ae0a5c 100644
--- a/src/plfa/Soundness.lagda
+++ b/src/plfa/Soundness.lagda
@@ -16,7 +16,7 @@ module plfa.Soundness where
 open import plfa.Untyped
   using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
          subst; _[_]; subst-zero; ext; rename; exts)
-open import extra.LambdaReduction
+open import plfa.LambdaReduction
   using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[])
 open import plfa.Denotational
 open import plfa.Compositional
diff --git a/extra/extra/Substitution.lagda b/src/plfa/Substitution.lagda
similarity index 99%
rename from extra/extra/Substitution.lagda
rename to src/plfa/Substitution.lagda
index 25d0db97..d4230385 100644
--- a/extra/extra/Substitution.lagda
+++ b/src/plfa/Substitution.lagda
@@ -1,3 +1,12 @@
+---
+title     : "Substitution in the untyped lambda calculus"
+layout    : page
+prev      : /Untyped/
+permalink : /Substitution/
+next      : /Confluence/
+---
+
+
 \begin{code}
 module plfa.Substitution where
 \end{code}