diff --git a/extra/denotational/Adequacy.lagda b/src/plfa/Adequacy.lagda
similarity index 99%
rename from extra/denotational/Adequacy.lagda
rename to src/plfa/Adequacy.lagda
index 2926bcf1..b47f2214 100644
--- a/extra/denotational/Adequacy.lagda
+++ b/src/plfa/Adequacy.lagda
@@ -7,7 +7,7 @@ next      : /ContextualEquivalence/
 ---
 
 \begin{code}
-module denotational.Adequacy where
+module plfa.Adequacy where
 \end{code}
 
 ## Imports
@@ -16,18 +16,18 @@ module denotational.Adequacy where
 open import plfa.Untyped
   using (Context; _⊢_; ★; _∋_; ∅; _,_; Z; S_; `_; ƛ_; _·_;
          rename; subst; ext; exts; _[_]; subst-zero)
-open import denotational.LambdaReduction
+open import plfa.LambdaReduction
   using (_—↠_; _—→⟨_⟩_; _[]; _—→_; ξ₁; ξ₂; β; ζ)
-open import denotational.CallByName
+open import plfa.CallByName
   using (Clos; clos; ClosEnv; ∅'; _,'_; _⊢_⇓_; ⇓-var; ⇓-lam; ⇓-app; ⇓-determ;
          cbn→reduce)
-open import denotational.Denotational
+open import plfa.Denotational
   using (Value; Env; `∅; _`,_; _↦_; _⊑_; _⊢_↓_; ⊥; Funs∈; _⊔_; ∈→⊑;
          var; ↦-elim; ↦-intro; ⊔-intro; ⊥-intro; sub; ℰ; _≃_; _iff_;
          Trans⊑; ConjR1⊑; ConjR2⊑; ConjL⊑; Refl⊑; Fun⊑; Bot⊑; Dist⊑;
          sub-inv-fun)
-open import denotational.Soundness using (soundness)
-open import denotational.Substitution using (ids; sub-id)
+open import plfa.Soundness using (soundness)
+open import plfa.Substitution using (ids; sub-id)
 
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; _≢_; refl; trans; sym; cong; cong₂; cong-app)
diff --git a/extra/denotational/CallByName.lagda b/src/plfa/CallByName.lagda
similarity index 99%
rename from extra/denotational/CallByName.lagda
rename to src/plfa/CallByName.lagda
index e586a9e8..bb8dd76e 100644
--- a/extra/denotational/CallByName.lagda
+++ b/src/plfa/CallByName.lagda
@@ -7,7 +7,7 @@ next      : /Denotational/
 ---
 
 \begin{code}
-module denotational.CallByName where
+module plfa.CallByName where
 \end{code}
 
 ## Imports
@@ -16,9 +16,9 @@ module denotational.CallByName where
 open import plfa.Untyped
   using (Context; _⊢_; _∋_; ★; ∅; _,_; Z; S_; `_; ƛ_; _·_; subst; subst-zero;
          exts; rename)
-open import denotational.LambdaReduction
+open import plfa.LambdaReduction
   using (β; ξ₁; ξ₂; ζ; _—→_; _—↠_; _—→⟨_⟩_; _[]; —↠-trans; appL-cong)
-open import denotational.Substitution
+open import plfa.Substitution
   using (Subst; ⟪_⟫; _•_; _⨟_; ids; sub-id; sub-sub; subst-zero-exts-cons)
 import Relation.Binary.PropositionalEquality as Eq
 open Eq using (_≡_; refl; trans; sym)
diff --git a/extra/denotational/Compositional.lagda b/src/plfa/Compositional.lagda
similarity index 99%
rename from extra/denotational/Compositional.lagda
rename to src/plfa/Compositional.lagda
index 03974baa..4fdda37c 100644
--- a/extra/denotational/Compositional.lagda
+++ b/src/plfa/Compositional.lagda
@@ -7,7 +7,7 @@ next      : /Soundness/
 ---
 
 \begin{code}
-module denotational.Compositional where
+module plfa.Compositional where
 \end{code}
 
 ## Imports
@@ -15,12 +15,12 @@ module denotational.Compositional where
 \begin{code}
 open import plfa.Untyped
   using (Context; _,_; ★; _∋_; _⊢_; `_; ƛ_; _·_)
-open import denotational.Denotational
+open import plfa.Denotational
   using (Value; _↦_; _`,_; _⊔_; ⊥; _⊑_; _⊢_↓_; nth;
          Bot⊑; Fun⊑; ConjL⊑; ConjR1⊑; ConjR2⊑; Dist⊑; Refl⊑; Trans⊑; Dist⊔↦⊔;
          var; ↦-intro; ↦-elim; ⊔-intro; ⊥-intro; sub;
          up-env; ℰ; _≃_; ≃-sym; Denotation; Env)
-open denotational.Denotational.≃-Reasoning
+open plfa.Denotational.≃-Reasoning
 
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
diff --git a/extra/denotational/Confluence.lagda b/src/plfa/Confluence.lagda
similarity index 99%
rename from extra/denotational/Confluence.lagda
rename to src/plfa/Confluence.lagda
index e9cc9d81..04c2c15a 100644
--- a/extra/denotational/Confluence.lagda
+++ b/src/plfa/Confluence.lagda
@@ -13,12 +13,11 @@ module plfa.Confluence where
 ## Imports
 
 \begin{code}
-open import plfa.Substitution using (subst-commute; rename-subst-commute)
+open import plfa.Substitution
+   using (subst-commute; rename-subst-commute; Rename; Subst)
 open import plfa.LambdaReduction
     using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _[];
            abs-cong; appL-cong; appR-cong; —↠-trans)
-open import plfa.Denotational using (Rename)
-open import plfa.Soundness using (Subst)
 open import plfa.Untyped
     using (_⊢_; _∋_; `_; _,_; ★; ƛ_; _·_; _[_];
            rename; ext; exts; Z; S_; subst; subst-zero)
diff --git a/extra/denotational/ContextualEquivalence.lagda b/src/plfa/ContextualEquivalence.lagda
similarity index 89%
rename from extra/denotational/ContextualEquivalence.lagda
rename to src/plfa/ContextualEquivalence.lagda
index c1c5f370..ec0d88de 100644
--- a/extra/denotational/ContextualEquivalence.lagda
+++ b/src/plfa/ContextualEquivalence.lagda
@@ -7,19 +7,19 @@ next      : /Acknowledgements/
 ---
 
 \begin{code}
-module denotational.ContextualEquivalence where
+module plfa.ContextualEquivalence where
 \end{code}
 
 ## Imports
 
 \begin{code}
 open import plfa.Untyped using (_⊢_; ★; ∅; _,_; ƛ_)
-open import denotational.LambdaReduction using (_—↠_)
-open import denotational.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
-open import denotational.Compositional using (Ctx; plug; compositionality)
-open import denotational.Soundness using (soundness)
-open import denotational.Adequacy using (adequacy)
-open import denotational.CallByName using (_⊢_⇓_; cbn→reduce)
+open import plfa.LambdaReduction using (_—↠_)
+open import plfa.Denotational using (ℰ; _≃_; ≃-sym; ≃-trans; _iff_)
+open import plfa.Compositional using (Ctx; plug; compositionality)
+open import plfa.Soundness using (soundness)
+open import plfa.Adequacy using (adequacy)
+open import plfa.CallByName using (_⊢_⇓_; cbn→reduce)
 
 open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; proj₂)
   renaming (_,_ to ⟨_,_⟩)
diff --git a/extra/denotational/Denotational.lagda b/src/plfa/Denotational.lagda
similarity index 99%
rename from extra/denotational/Denotational.lagda
rename to src/plfa/Denotational.lagda
index 060e8d78..bacc5a44 100644
--- a/extra/denotational/Denotational.lagda
+++ b/src/plfa/Denotational.lagda
@@ -7,7 +7,7 @@ next      : /Compositional/
 ---
 
 \begin{code}
-module denotational.Denotational where
+module plfa.Denotational where
 \end{code}
 
 The lambda calculus is a language about _functions_, that is, mappings
@@ -63,7 +63,7 @@ open import Agda.Primitive using (lzero)
 open import plfa.Untyped
     using (Context; ★; _∋_; ∅; _,_; Z; S_; _⊢_; `_; _·_; ƛ_;
            #_; twoᶜ; ext; rename; exts; subst; subst-zero; _[_])
-open import denotational.Substitution using (Rename; extensionality; rename-id)
+open import plfa.Substitution using (Rename; extensionality; rename-id)
 open import Relation.Nullary using (¬_)
 open import Relation.Nullary.Negation using (contradiction)
 open import Data.Empty using (⊥-elim)
diff --git a/extra/denotational/LambdaReduction.lagda b/src/plfa/LambdaReduction.lagda
similarity index 98%
rename from extra/denotational/LambdaReduction.lagda
rename to src/plfa/LambdaReduction.lagda
index 5e4bde51..915ecba3 100644
--- a/extra/denotational/LambdaReduction.lagda
+++ b/src/plfa/LambdaReduction.lagda
@@ -7,7 +7,7 @@ next      : /Confluence/
 ---
 
 \begin{code}
-module denotational.LambdaReduction where
+module plfa.LambdaReduction where
 \end{code}
 
 ## Imports
diff --git a/extra/denotational/Soundness.lagda b/src/plfa/Soundness.lagda
similarity index 99%
rename from extra/denotational/Soundness.lagda
rename to src/plfa/Soundness.lagda
index 52e19766..249521f6 100644
--- a/extra/denotational/Soundness.lagda
+++ b/src/plfa/Soundness.lagda
@@ -7,7 +7,7 @@ next      : /Adequacy/
 ---
 
 \begin{code}
-module denotational.Soundness where
+module plfa.Soundness where
 \end{code}
 
 ## Imports
@@ -16,15 +16,15 @@ module denotational.Soundness where
 open import plfa.Untyped
   using (Context; _,_; _∋_; _⊢_; ★; Z; S_; `_; ƛ_; _·_;
          subst; _[_]; subst-zero; ext; rename; exts)
-open import denotational.LambdaReduction
+open import plfa.LambdaReduction
   using (_—→_; ξ₁; ξ₂; β; ζ; _—↠_; _—→⟨_⟩_; _[])
-open import denotational.Substitution using (Rename; Subst; ids)  
-open import denotational.Denotational
+open import plfa.Substitution using (Rename; Subst; ids)  
+open import plfa.Denotational
   using (Value; ⊥; Env; _⊢_↓_; _`,_; _⊑_; _`⊑_; `⊥; _`⊔_; init; last; init-last;
          Refl⊑; Trans⊑; `Refl⊑; Env⊑; EnvConjR1⊑; EnvConjR2⊑; up-env;
          var; ↦-elim; ↦-intro; ⊥-intro; ⊔-intro; sub;
          rename-pres; ℰ; _≃_; ≃-trans)
-open import denotational.Compositional using (lambda-inversion; var-inv)
+open import plfa.Compositional using (lambda-inversion; var-inv)
 
 open import Relation.Binary.PropositionalEquality
   using (_≡_; _≢_; refl; sym; cong; cong₂; cong-app)
diff --git a/extra/denotational/Substitution.lagda b/src/plfa/Substitution.lagda
similarity index 99%
rename from extra/denotational/Substitution.lagda
rename to src/plfa/Substitution.lagda
index eba252ef..09384e68 100644
--- a/extra/denotational/Substitution.lagda
+++ b/src/plfa/Substitution.lagda
@@ -8,7 +8,7 @@ next      : /LambdaReduction/
 
 
 \begin{code}
-module denotational.Substitution where
+module plfa.Substitution where
 \end{code}
 
 ## Imports