From 01fa4208b2110765b2cdf93219756124550eff4d Mon Sep 17 00:00:00 2001 From: Trebor-Huang Date: Thu, 19 Sep 2024 22:16:54 +0800 Subject: [PATCH] safe flags --- Cubical/HITs/James/Stable.agda | 2 +- Cubical/HITs/Susp/SuspProduct.agda | 2 +- Cubical/Homotopy/HiltonMilnor.agda | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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