diff --git a/Cubical/HITs/James/Stable.agda b/Cubical/HITs/James/Stable.agda
index 7c9915f49..48e6af5b7 100644
--- a/Cubical/HITs/James/Stable.agda
+++ b/Cubical/HITs/James/Stable.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
 
 {-
   The stable version of the James splitting:
diff --git a/Cubical/HITs/Susp/SuspProduct.agda b/Cubical/HITs/Susp/SuspProduct.agda
index d847ff614..6f00c0d62 100644
--- a/Cubical/HITs/Susp/SuspProduct.agda
+++ b/Cubical/HITs/Susp/SuspProduct.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical #-}
+{-# OPTIONS --safe #-}
 
 {-
   The suspension of a Cartesian product is given by a triple wedge sum
diff --git a/Cubical/Homotopy/HiltonMilnor.agda b/Cubical/Homotopy/HiltonMilnor.agda
index c8f967ac0..425a5e797 100644
--- a/Cubical/Homotopy/HiltonMilnor.agda
+++ b/Cubical/Homotopy/HiltonMilnor.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical --lossy-unification #-}
+{-# OPTIONS --safe --lossy-unification #-}
 
 {-
   The finitary Hilton–Milnor splitting