diff --git a/extra/extra/Lambda-new.lagda b/extra/extra/Lambda-new.lagda
index 3d5c98ab..9a9e0770 100644
--- a/extra/extra/Lambda-new.lagda
+++ b/extra/extra/Lambda-new.lagda
@@ -38,7 +38,7 @@ progress and preservation.  Following chapters will look at a number
 of variants of lambda calculus.
 
 Be aware that the approach we take here is _not_ our recommended
-approach to formalisation.  Using De Bruijn indices and
+approach to formalisation.  Using de Bruijn indices and
 inherently-typed terms, as we will do in
 Chapter [DeBruijn]({{ site.baseurl }}{% link out/plta/DeBruijn.md %}),
 leads to a more compact formulation.  Nonetheless, we begin with named
diff --git a/src/plfa/Denotational.lagda b/src/plfa/Denotational.lagda
index aa1ff205..13eeca46 100644
--- a/src/plfa/Denotational.lagda
+++ b/src/plfa/Denotational.lagda
@@ -251,7 +251,7 @@ init-last {Γ} γ = extensionality lemma
   lemma (S x)  =  refl
 \end{code}
 
-The nth function takes a De Bruijn index and finds the corresponding
+The nth function takes a de Bruijn index and finds the corresponding
 value in the environment.
 
 \begin{code}