diff --git a/extra/extra/Logic.lagda b/extra/extra/Logic.lagda
index f69db196..aa86e676 100644
--- a/extra/extra/Logic.lagda
+++ b/extra/extra/Logic.lagda
@@ -94,7 +94,7 @@ Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)` and
 
 Given two types `A` and `B`, we refer to `A x B` as the
 *product* of `A` and `B`.  In set theory, it is also sometimes
-called the *cartesian product*, and in computing it corresponds
+called the *Cartesian product*, and in computing it corresponds
 to a *record* type. Among other reasons for
 calling it the product, note that if type `A` has `m`
 distinct members, and type `B` has `n` distinct members,
diff --git a/src/plfa/Connectives.lagda b/src/plfa/Connectives.lagda
index cd7810e5..3a157529 100644
--- a/src/plfa/Connectives.lagda
+++ b/src/plfa/Connectives.lagda
@@ -133,7 +133,7 @@ Thus, `m ≤ n × n ≤ p` parses as `(m ≤ n) × (n ≤ p)`.
 
 Given two types `A` and `B`, we refer to `A x B` as the
 _product_ of `A` and `B`.  In set theory, it is also sometimes
-called the _cartesian product_, and in computing it corresponds
+called the _Cartesian product_, and in computing it corresponds
 to a _record_ type. Among other reasons for
 calling it the product, note that if type `A` has `m`
 distinct members, and type `B` has `n` distinct members,