diff --git a/src/plfa/part2/Inference.lagda.md b/src/plfa/part2/Inference.lagda.md
index bae6e323..654f497b 100644
--- a/src/plfa/part2/Inference.lagda.md
+++ b/src/plfa/part2/Inference.lagda.md
@@ -260,7 +260,7 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
 Once we have a type derivation, it will be easy to construct
 from it the intrinsically-typed representation.  In order that we
 can compare with our previous development, we import
-module `pfla.DeBruijn`:
+module `plfa.part2.DeBruijn`:
 
 ```
 import plfa.part2.DeBruijn as DB
diff --git a/src/plfa/part2/Lambda.lagda.md b/src/plfa/part2/Lambda.lagda.md
index a98d3913..cea0bc0f 100644
--- a/src/plfa/part2/Lambda.lagda.md
+++ b/src/plfa/part2/Lambda.lagda.md
@@ -1178,7 +1178,7 @@ the empty type `⊥`.  If we use C-c C-n to normalise the term
 
 Agda will return an answer warning us that the impossible has occurred:
 
-    ⊥-elim (.plfa.Lambda.impossible "a" "a" refl)
+    ⊥-elim (plfa.part2.Lambda.impossible "a" "a" refl)
 
 While postulating the impossible is a useful technique, it must be
 used with care, since such postulation could allow us to provide