diff --git a/src/foundation/universal-property-cartesian-product-types.lagda.md b/src/foundation/universal-property-cartesian-product-types.lagda.md
index 398f26853a..362ce03044 100644
--- a/src/foundation/universal-property-cartesian-product-types.lagda.md
+++ b/src/foundation/universal-property-cartesian-product-types.lagda.md
@@ -108,9 +108,9 @@ Cartesian products are a special case of pullbacks.
   is-retraction-inv-gap-product (pair a b) = refl
 
   abstract
-    is-pullback-product :
+    is-pullback-cartesian-product :
       is-pullback (terminal-map A) (terminal-map B) cone-product
-    is-pullback-product =
+    is-pullback-cartesian-product =
       is-equiv-is-invertible
         inv-gap-product
         is-section-inv-gap-product
@@ -131,5 +131,5 @@ We conclude that cartesian products satisfy the universal property of pullbacks.
         ( terminal-map A)
         ( terminal-map B)
         ( cone-product)
-        ( is-pullback-product)
+        ( is-pullback-cartesian-product)
 ```
diff --git a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
index f10cf0df03..98f0df2cb7 100644
--- a/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/acyclic-maps.lagda.md
@@ -494,7 +494,7 @@ module _
           ( terminal-map A)
           ( terminal-map B)
           ( cone-product A B)
-          ( is-pullback-product A B)
+          ( is-pullback-cartesian-product A B)
           ( is-acyclic-map-terminal-map-is-acyclic A ac-A)))
 ```
 
diff --git a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
index 74b92b82ab..7c38195588 100644
--- a/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
+++ b/src/synthetic-homotopy-theory/truncated-acyclic-maps.lagda.md
@@ -470,7 +470,7 @@ module _
           ( terminal-map A)
           ( terminal-map B)
           ( cone-product A B)
-          ( is-pullback-product A B)
+          ( is-pullback-cartesian-product A B)
           ( is-truncated-acyclic-map-terminal-map-is-truncated-acyclic A ac-A)))
 ```