diff --git a/proofs/agda/AntiEcho.agda b/proofs/agda/AntiEcho.agda
index 7760d95..15c5859 100644
--- a/proofs/agda/AntiEcho.agda
+++ b/proofs/agda/AntiEcho.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/AntiEchoTropical.agda b/proofs/agda/AntiEchoTropical.agda
index 1fd0102..b6f5af9 100644
--- a/proofs/agda/AntiEchoTropical.agda
+++ b/proofs/agda/AntiEchoTropical.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/AntiEchoTropicalGeneric.agda b/proofs/agda/AntiEchoTropicalGeneric.agda
index 6037945..08e3fb1 100644
--- a/proofs/agda/AntiEchoTropicalGeneric.agda
+++ b/proofs/agda/AntiEchoTropicalGeneric.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Dyadic.agda b/proofs/agda/Dyadic.agda
index 20363e1..8f7f61a 100644
--- a/proofs/agda/Dyadic.agda
+++ b/proofs/agda/Dyadic.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/DyadicEchoBridge.agda b/proofs/agda/DyadicEchoBridge.agda
index 49ee41f..3b5ed2f 100644
--- a/proofs/agda/DyadicEchoBridge.agda
+++ b/proofs/agda/DyadicEchoBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo.agda b/proofs/agda/Echo.agda
index 86745cd..1ce9cfc 100644
--- a/proofs/agda/Echo.agda
+++ b/proofs/agda/Echo.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Index/ThinPoset.agda b/proofs/agda/Echo/Index/ThinPoset.agda
index 805eb3d..c6c579a 100644
--- a/proofs/agda/Echo/Index/ThinPoset.agda
+++ b/proofs/agda/Echo/Index/ThinPoset.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Measure/Examples.agda b/proofs/agda/Echo/Measure/Examples.agda
index 5065d80..e169a02 100644
--- a/proofs/agda/Echo/Measure/Examples.agda
+++ b/proofs/agda/Echo/Measure/Examples.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Measure/Interface.agda b/proofs/agda/Echo/Measure/Interface.agda
index 04e8dc3..e965bbb 100644
--- a/proofs/agda/Echo/Measure/Interface.agda
+++ b/proofs/agda/Echo/Measure/Interface.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Modality/Core.agda b/proofs/agda/Echo/Modality/Core.agda
index 60b6932..d55f678 100644
--- a/proofs/agda/Echo/Modality/Core.agda
+++ b/proofs/agda/Echo/Modality/Core.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Modality/Interface.agda b/proofs/agda/Echo/Modality/Interface.agda
index 9777157..2d66ad7 100644
--- a/proofs/agda/Echo/Modality/Interface.agda
+++ b/proofs/agda/Echo/Modality/Interface.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Echo/Separation/NotResourceInstance.agda b/proofs/agda/Echo/Separation/NotResourceInstance.agda
index 8b0334c..1f056df 100644
--- a/proofs/agda/Echo/Separation/NotResourceInstance.agda
+++ b/proofs/agda/Echo/Separation/NotResourceInstance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoAbstractionBarrier.agda b/proofs/agda/EchoAbstractionBarrier.agda
index a33f52d..038c673 100644
--- a/proofs/agda/EchoAbstractionBarrier.agda
+++ b/proofs/agda/EchoAbstractionBarrier.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoAccess.agda b/proofs/agda/EchoAccess.agda
index e0e9820..5f680ad 100644
--- a/proofs/agda/EchoAccess.agda
+++ b/proofs/agda/EchoAccess.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoAggregation.agda b/proofs/agda/EchoAggregation.agda
index 0b545a3..8dca672 100644
--- a/proofs/agda/EchoAggregation.agda
+++ b/proofs/agda/EchoAggregation.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoApprox.agda b/proofs/agda/EchoApprox.agda
index 3a863f8..3ca4fe2 100644
--- a/proofs/agda/EchoApprox.agda
+++ b/proofs/agda/EchoApprox.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoApproxInstance.agda b/proofs/agda/EchoApproxInstance.agda
index 3ec3b30..c40f05d 100644
--- a/proofs/agda/EchoApproxInstance.agda
+++ b/proofs/agda/EchoApproxInstance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoBitNarrowingNumeric.agda b/proofs/agda/EchoBitNarrowingNumeric.agda
index c193149..619991d 100644
--- a/proofs/agda/EchoBitNarrowingNumeric.agda
+++ b/proofs/agda/EchoBitNarrowingNumeric.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Numeric specification for the typed-wasm-echo receipt. This proves the
diff --git a/proofs/agda/EchoCanonicalIdentitySuite.agda b/proofs/agda/EchoCanonicalIdentitySuite.agda
index 4f51b3b..7b7570a 100644
--- a/proofs/agda/EchoCanonicalIdentitySuite.agda
+++ b/proofs/agda/EchoCanonicalIdentitySuite.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoCategorical.agda b/proofs/agda/EchoCategorical.agda
index 886f4f8..0a538dc 100644
--- a/proofs/agda/EchoCategorical.agda
+++ b/proofs/agda/EchoCategorical.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoCharacteristic.agda b/proofs/agda/EchoCharacteristic.agda
index 7a6ad9d..4f18d64 100644
--- a/proofs/agda/EchoCharacteristic.agda
+++ b/proofs/agda/EchoCharacteristic.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoChoreo.agda b/proofs/agda/EchoChoreo.agda
index 07446cd..4d2c4b1 100644
--- a/proofs/agda/EchoChoreo.agda
+++ b/proofs/agda/EchoChoreo.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoCost.agda b/proofs/agda/EchoCost.agda
index c37c622..ae6adef 100644
--- a/proofs/agda/EchoCost.agda
+++ b/proofs/agda/EchoCost.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoCostInstance.agda b/proofs/agda/EchoCostInstance.agda
index 4a977a1..b6dc882 100644
--- a/proofs/agda/EchoCostInstance.agda
+++ b/proofs/agda/EchoCostInstance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDecidable.agda b/proofs/agda/EchoDecidable.agda
index 9a1e75c..38d06e0 100644
--- a/proofs/agda/EchoDecidable.agda
+++ b/proofs/agda/EchoDecidable.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDecorationBridge.agda b/proofs/agda/EchoDecorationBridge.agda
index 039ba45..ea7eec2 100644
--- a/proofs/agda/EchoDecorationBridge.agda
+++ b/proofs/agda/EchoDecorationBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDecorationStructure.agda b/proofs/agda/EchoDecorationStructure.agda
index 1ec753f..e188f7b 100644
--- a/proofs/agda/EchoDecorationStructure.agda
+++ b/proofs/agda/EchoDecorationStructure.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDeniability.agda b/proofs/agda/EchoDeniability.agda
index 44599b9..55f27d9 100644
--- a/proofs/agda/EchoDeniability.agda
+++ b/proofs/agda/EchoDeniability.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDifferential.agda b/proofs/agda/EchoDifferential.agda
index f7e8833..b2fef3e 100644
--- a/proofs/agda/EchoDifferential.agda
+++ b/proofs/agda/EchoDifferential.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoDisplayed.agda b/proofs/agda/EchoDisplayed.agda
index a47f2c5..2da6ab3 100644
--- a/proofs/agda/EchoDisplayed.agda
+++ b/proofs/agda/EchoDisplayed.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoEntropy.agda b/proofs/agda/EchoEntropy.agda
index fc5d7c1..8e01fc1 100644
--- a/proofs/agda/EchoEntropy.agda
+++ b/proofs/agda/EchoEntropy.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoEphapaxBridge.agda b/proofs/agda/EchoEphapaxBridge.agda
index e61250d..02fab9c 100644
--- a/proofs/agda/EchoEphapaxBridge.agda
+++ b/proofs/agda/EchoEphapaxBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoEpistemic.agda b/proofs/agda/EchoEpistemic.agda
index 09f717c..4a1f9bc 100644
--- a/proofs/agda/EchoEpistemic.agda
+++ b/proofs/agda/EchoEpistemic.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoEpistemicResidue.agda b/proofs/agda/EchoEpistemicResidue.agda
index 245e50c..97e0a3b 100644
--- a/proofs/agda/EchoEpistemicResidue.agda
+++ b/proofs/agda/EchoEpistemicResidue.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleAbsInt.agda b/proofs/agda/EchoExampleAbsInt.agda
index 4ac3174..3f4ab49 100644
--- a/proofs/agda/EchoExampleAbsInt.agda
+++ b/proofs/agda/EchoExampleAbsInt.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleBitNarrowing.agda b/proofs/agda/EchoExampleBitNarrowing.agda
index 334c7cd..d0981e8 100644
--- a/proofs/agda/EchoExampleBitNarrowing.agda
+++ b/proofs/agda/EchoExampleBitNarrowing.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleParser.agda b/proofs/agda/EchoExampleParser.agda
index 95fcc90..f5f9d2d 100644
--- a/proofs/agda/EchoExampleParser.agda
+++ b/proofs/agda/EchoExampleParser.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleProvenance.agda b/proofs/agda/EchoExampleProvenance.agda
index 6484e2f..25a9de8 100644
--- a/proofs/agda/EchoExampleProvenance.agda
+++ b/proofs/agda/EchoExampleProvenance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleSignAnalysis.agda b/proofs/agda/EchoExampleSignAnalysis.agda
index ee0a318..7b52550 100644
--- a/proofs/agda/EchoExampleSignAnalysis.agda
+++ b/proofs/agda/EchoExampleSignAnalysis.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExampleTruncation.agda b/proofs/agda/EchoExampleTruncation.agda
index 82e9407..91f0034 100644
--- a/proofs/agda/EchoExampleTruncation.agda
+++ b/proofs/agda/EchoExampleTruncation.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoExamples.agda b/proofs/agda/EchoExamples.agda
index 6291a16..6c2d6a7 100644
--- a/proofs/agda/EchoExamples.agda
+++ b/proofs/agda/EchoExamples.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoFiberBridge.agda b/proofs/agda/EchoFiberBridge.agda
index 15b2544..83ef2ad 100644
--- a/proofs/agda/EchoFiberBridge.agda
+++ b/proofs/agda/EchoFiberBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoFiberCount.agda b/proofs/agda/EchoFiberCount.agda
index 181a815..a3a2683 100644
--- a/proofs/agda/EchoFiberCount.agda
+++ b/proofs/agda/EchoFiberCount.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoFiberTriangulation.agda b/proofs/agda/EchoFiberTriangulation.agda
index b237d2b..72c7212 100644
--- a/proofs/agda/EchoFiberTriangulation.agda
+++ b/proofs/agda/EchoFiberTriangulation.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoFidelity.agda b/proofs/agda/EchoFidelity.agda
index 04e09ca..3850d73 100644
--- a/proofs/agda/EchoFidelity.agda
+++ b/proofs/agda/EchoFidelity.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 --
 -- STATUS: type-checks under Agda 2.6.3 / agda-stdlib 2.3 (`--safe
diff --git a/proofs/agda/EchoGraded.agda b/proofs/agda/EchoGraded.agda
index 38f4787..b3bd5bf 100644
--- a/proofs/agda/EchoGraded.agda
+++ b/proofs/agda/EchoGraded.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoGradedComonad.agda b/proofs/agda/EchoGradedComonad.agda
index f928545..c6a560f 100644
--- a/proofs/agda/EchoGradedComonad.agda
+++ b/proofs/agda/EchoGradedComonad.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoGradedComonadF1.agda b/proofs/agda/EchoGradedComonadF1.agda
index 30c399f..b69fc00 100644
--- a/proofs/agda/EchoGradedComonadF1.agda
+++ b/proofs/agda/EchoGradedComonadF1.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoGradedComonadInstance1.agda b/proofs/agda/EchoGradedComonadInstance1.agda
index 1aa3791..fe7ad62 100644
--- a/proofs/agda/EchoGradedComonadInstance1.agda
+++ b/proofs/agda/EchoGradedComonadInstance1.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoGradedComonadInstance2.agda b/proofs/agda/EchoGradedComonadInstance2.agda
index 7c4d5bb..815e81f 100644
--- a/proofs/agda/EchoGradedComonadInstance2.agda
+++ b/proofs/agda/EchoGradedComonadInstance2.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoGradedComonadInterface.agda b/proofs/agda/EchoGradedComonadInterface.agda
index f2641c7..90c1903 100644
--- a/proofs/agda/EchoGradedComonadInterface.agda
+++ b/proofs/agda/EchoGradedComonadInterface.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoHaplotypeCollapsing.agda b/proofs/agda/EchoHaplotypeCollapsing.agda
index 225cd1a..a7c90b0 100644
--- a/proofs/agda/EchoHaplotypeCollapsing.agda
+++ b/proofs/agda/EchoHaplotypeCollapsing.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoImageFactorization.agda b/proofs/agda/EchoImageFactorization.agda
index 7536f86..5384e22 100644
--- a/proofs/agda/EchoImageFactorization.agda
+++ b/proofs/agda/EchoImageFactorization.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoImageFactorizationProp.agda b/proofs/agda/EchoImageFactorizationProp.agda
index 1ffb73b..871f2a8 100644
--- a/proofs/agda/EchoImageFactorizationProp.agda
+++ b/proofs/agda/EchoImageFactorizationProp.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoIndexed.agda b/proofs/agda/EchoIndexed.agda
index 67bce2e..e6c83f3 100644
--- a/proofs/agda/EchoIndexed.agda
+++ b/proofs/agda/EchoIndexed.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoIntegration.agda b/proofs/agda/EchoIntegration.agda
index 116d193..18e5a77 100644
--- a/proofs/agda/EchoIntegration.agda
+++ b/proofs/agda/EchoIntegration.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoJanusBridge.agda b/proofs/agda/EchoJanusBridge.agda
index ee7a140..6b04c7f 100644
--- a/proofs/agda/EchoJanusBridge.agda
+++ b/proofs/agda/EchoJanusBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoKernel.agda b/proofs/agda/EchoKernel.agda
index a7ba21a..fc84973 100644
--- a/proofs/agda/EchoKernel.agda
+++ b/proofs/agda/EchoKernel.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoLLEncoding.agda b/proofs/agda/EchoLLEncoding.agda
index 9f9458e..063bd4e 100644
--- a/proofs/agda/EchoLLEncoding.agda
+++ b/proofs/agda/EchoLLEncoding.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoLinear.agda b/proofs/agda/EchoLinear.agda
index c686717..9b260f5 100644
--- a/proofs/agda/EchoLinear.agda
+++ b/proofs/agda/EchoLinear.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoLossTaxonomy.agda b/proofs/agda/EchoLossTaxonomy.agda
index 16c0020..bc117ef 100644
--- a/proofs/agda/EchoLossTaxonomy.agda
+++ b/proofs/agda/EchoLossTaxonomy.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoNoSectionGeneric.agda b/proofs/agda/EchoNoSectionGeneric.agda
index 14c6809..3ac5b58 100644
--- a/proofs/agda/EchoNoSectionGeneric.agda
+++ b/proofs/agda/EchoNoSectionGeneric.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoOFSUnivF5.agda b/proofs/agda/EchoOFSUnivF5.agda
index e3237ad..f18774e 100644
--- a/proofs/agda/EchoOFSUnivF5.agda
+++ b/proofs/agda/EchoOFSUnivF5.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoOFSUnivF5Diag.agda b/proofs/agda/EchoOFSUnivF5Diag.agda
index 5cdae35..f1ec1c7 100644
--- a/proofs/agda/EchoOFSUnivF5Diag.agda
+++ b/proofs/agda/EchoOFSUnivF5Diag.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoOFSUnivF5Iso.agda b/proofs/agda/EchoOFSUnivF5Iso.agda
index 5389858..51430e8 100644
--- a/proofs/agda/EchoOFSUnivF5Iso.agda
+++ b/proofs/agda/EchoOFSUnivF5Iso.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoObservationalEquivalence.agda b/proofs/agda/EchoObservationalEquivalence.agda
index 1accfcd..c42d188 100644
--- a/proofs/agda/EchoObservationalEquivalence.agda
+++ b/proofs/agda/EchoObservationalEquivalence.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoOrdinal.agda b/proofs/agda/EchoOrdinal.agda
index 5b4eaf7..81d3c45 100644
--- a/proofs/agda/EchoOrdinal.agda
+++ b/proofs/agda/EchoOrdinal.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoOrthogonalFactorizationSystem.agda b/proofs/agda/EchoOrthogonalFactorizationSystem.agda
index 7b2ff7b..046d479 100644
--- a/proofs/agda/EchoOrthogonalFactorizationSystem.agda
+++ b/proofs/agda/EchoOrthogonalFactorizationSystem.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoProbabilisticSupport.agda b/proofs/agda/EchoProbabilisticSupport.agda
index 7966b39..0207eb2 100644
--- a/proofs/agda/EchoProbabilisticSupport.agda
+++ b/proofs/agda/EchoProbabilisticSupport.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoProvenance.agda b/proofs/agda/EchoProvenance.agda
index fb2329c..510e888 100644
--- a/proofs/agda/EchoProvenance.agda
+++ b/proofs/agda/EchoProvenance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoPullback.agda b/proofs/agda/EchoPullback.agda
index 4b73d41..14ecc7f 100644
--- a/proofs/agda/EchoPullback.agda
+++ b/proofs/agda/EchoPullback.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoPullbackUnivF4.agda b/proofs/agda/EchoPullbackUnivF4.agda
index 787f7c0..41cc045 100644
--- a/proofs/agda/EchoPullbackUnivF4.agda
+++ b/proofs/agda/EchoPullbackUnivF4.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoRelModel.agda b/proofs/agda/EchoRelModel.agda
index 010027f..b0c2b56 100644
--- a/proofs/agda/EchoRelModel.agda
+++ b/proofs/agda/EchoRelModel.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoRelational.agda b/proofs/agda/EchoRelational.agda
index d19feac..15f5af9 100644
--- a/proofs/agda/EchoRelational.agda
+++ b/proofs/agda/EchoRelational.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoResidue.agda b/proofs/agda/EchoResidue.agda
index 880f05a..e771569 100644
--- a/proofs/agda/EchoResidue.agda
+++ b/proofs/agda/EchoResidue.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoResidueCell.agda b/proofs/agda/EchoResidueCell.agda
index 696903b..d5761b1 100644
--- a/proofs/agda/EchoResidueCell.agda
+++ b/proofs/agda/EchoResidueCell.agda
@@ -26,7 +26,7 @@
 -- `holding` cell before consuming) — that needs the `(1 e)` quantity / an
 -- `@0`-style erasure encoding and remains the documented next slice.
 
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EchoResidueCell where
 
diff --git a/proofs/agda/EchoResidueTaxonomy.agda b/proofs/agda/EchoResidueTaxonomy.agda
index ab3112c..ea2026e 100644
--- a/proofs/agda/EchoResidueTaxonomy.agda
+++ b/proofs/agda/EchoResidueTaxonomy.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoReversibilityBridge.agda b/proofs/agda/EchoReversibilityBridge.agda
index 8f14078..23e45db 100644
--- a/proofs/agda/EchoReversibilityBridge.agda
+++ b/proofs/agda/EchoReversibilityBridge.agda
@@ -25,7 +25,7 @@
 -- under `--safe --without-K` with zero postulates. The Agda here is the
 -- source of truth; 007's Rust checker and Idris2 spec mirror this model.
 
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EchoReversibilityBridge where
 
diff --git a/proofs/agda/EchoScope.agda b/proofs/agda/EchoScope.agda
index 5c36d53..e75876a 100644
--- a/proofs/agda/EchoScope.agda
+++ b/proofs/agda/EchoScope.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSearch.agda b/proofs/agda/EchoSearch.agda
index dbfca39..3b80e0f 100644
--- a/proofs/agda/EchoSearch.agda
+++ b/proofs/agda/EchoSearch.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSearchExample.agda b/proofs/agda/EchoSearchExample.agda
index 9653f22..555814a 100644
--- a/proofs/agda/EchoSearchExample.agda
+++ b/proofs/agda/EchoSearchExample.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSearchInstance.agda b/proofs/agda/EchoSearchInstance.agda
index d1cda76..845a7a9 100644
--- a/proofs/agda/EchoSearchInstance.agda
+++ b/proofs/agda/EchoSearchInstance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSecurity.agda b/proofs/agda/EchoSecurity.agda
index 46d8f1c..a5dd567 100644
--- a/proofs/agda/EchoSecurity.agda
+++ b/proofs/agda/EchoSecurity.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSelectiveProjection.agda b/proofs/agda/EchoSelectiveProjection.agda
index 670c5f5..568d4f3 100644
--- a/proofs/agda/EchoSelectiveProjection.agda
+++ b/proofs/agda/EchoSelectiveProjection.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoSeparating.agda b/proofs/agda/EchoSeparating.agda
index 52f2c95..dac95b1 100644
--- a/proofs/agda/EchoSeparating.agda
+++ b/proofs/agda/EchoSeparating.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoStabilityTests.agda b/proofs/agda/EchoStabilityTests.agda
index 22cc2ef..2ee13f6 100644
--- a/proofs/agda/EchoStabilityTests.agda
+++ b/proofs/agda/EchoStabilityTests.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoStepNDModelF2.agda b/proofs/agda/EchoStepNDModelF2.agda
index c6f7e5a..de424c4 100644
--- a/proofs/agda/EchoStepNDModelF2.agda
+++ b/proofs/agda/EchoStepNDModelF2.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoThermoCollapseImpossible.agda b/proofs/agda/EchoThermoCollapseImpossible.agda
index ca5aeb2..93c433b 100644
--- a/proofs/agda/EchoThermoCollapseImpossible.agda
+++ b/proofs/agda/EchoThermoCollapseImpossible.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoThermodynamics.agda b/proofs/agda/EchoThermodynamics.agda
index 3148ce2..41ca32a 100644
--- a/proofs/agda/EchoThermodynamics.agda
+++ b/proofs/agda/EchoThermodynamics.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoThermodynamicsFinite.agda b/proofs/agda/EchoThermodynamicsFinite.agda
index 5bb3bf2..31a34f3 100644
--- a/proofs/agda/EchoThermodynamicsFinite.agda
+++ b/proofs/agda/EchoThermodynamicsFinite.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoTotalCompletion.agda b/proofs/agda/EchoTotalCompletion.agda
index 59a48f1..dc490ac 100644
--- a/proofs/agda/EchoTotalCompletion.agda
+++ b/proofs/agda/EchoTotalCompletion.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoTransaction.agda b/proofs/agda/EchoTransaction.agda
index c5f1cb6..61aa858 100644
--- a/proofs/agda/EchoTransaction.agda
+++ b/proofs/agda/EchoTransaction.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoTropical.agda b/proofs/agda/EchoTropical.agda
index fd89672..f3aa127 100644
--- a/proofs/agda/EchoTropical.agda
+++ b/proofs/agda/EchoTropical.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoTruncation.agda b/proofs/agda/EchoTruncation.agda
index cc38831..64bc575 100644
--- a/proofs/agda/EchoTruncation.agda
+++ b/proofs/agda/EchoTruncation.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/EchoVariance.agda b/proofs/agda/EchoVariance.agda
index 0779c4d..963fdef 100644
--- a/proofs/agda/EchoVariance.agda
+++ b/proofs/agda/EchoVariance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/MinimalCNO.agda b/proofs/agda/MinimalCNO.agda
index 8a66daf..1993fdd 100644
--- a/proofs/agda/MinimalCNO.agda
+++ b/proofs/agda/MinimalCNO.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/NarrowingSmoke.agda b/proofs/agda/NarrowingSmoke.agda
index a7a2b77..cb62e85 100644
--- a/proofs/agda/NarrowingSmoke.agda
+++ b/proofs/agda/NarrowingSmoke.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Focused entrypoint for the Wasm narrowing model and numeric contract.
diff --git a/proofs/agda/Ordinal/Buchholz/Syntax.agda b/proofs/agda/Ordinal/Buchholz/Syntax.agda
index ea5f908..e3ab590 100644
--- a/proofs/agda/Ordinal/Buchholz/Syntax.agda
+++ b/proofs/agda/Ordinal/Buchholz/Syntax.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/Ordinal/OmegaMarkers.agda b/proofs/agda/Ordinal/OmegaMarkers.agda
index dee20cd..f74e5a4 100644
--- a/proofs/agda/Ordinal/OmegaMarkers.agda
+++ b/proofs/agda/Ordinal/OmegaMarkers.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/SimpleTest.agda b/proofs/agda/SimpleTest.agda
index 7487286..4fd7b66 100644
--- a/proofs/agda/SimpleTest.agda
+++ b/proofs/agda/SimpleTest.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/VecRotation.agda b/proofs/agda/VecRotation.agda
index f591261..8d0d5fd 100644
--- a/proofs/agda/VecRotation.agda
+++ b/proofs/agda/VecRotation.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/WorkingCNO.agda b/proofs/agda/WorkingCNO.agda
index e76c1f3..6ec2133 100644
--- a/proofs/agda/WorkingCNO.agda
+++ b/proofs/agda/WorkingCNO.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/All.agda b/proofs/agda/characteristic/All.agda
index 980b26d..edac45e 100644
--- a/proofs/agda/characteristic/All.agda
+++ b/proofs/agda/characteristic/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/ChoreoInjective.agda b/proofs/agda/characteristic/ChoreoInjective.agda
index 015f9a0..dfd0843 100644
--- a/proofs/agda/characteristic/ChoreoInjective.agda
+++ b/proofs/agda/characteristic/ChoreoInjective.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/IntegrationAudit.agda b/proofs/agda/characteristic/IntegrationAudit.agda
index fe30976..248f672 100644
--- a/proofs/agda/characteristic/IntegrationAudit.agda
+++ b/proofs/agda/characteristic/IntegrationAudit.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/InteractionTest.agda b/proofs/agda/characteristic/InteractionTest.agda
index f4bd3e5..011067b 100644
--- a/proofs/agda/characteristic/InteractionTest.agda
+++ b/proofs/agda/characteristic/InteractionTest.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/ModeGraded.agda b/proofs/agda/characteristic/ModeGraded.agda
index 1c3d093..7d2c856 100644
--- a/proofs/agda/characteristic/ModeGraded.agda
+++ b/proofs/agda/characteristic/ModeGraded.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/N5Falsifier.agda b/proofs/agda/characteristic/N5Falsifier.agda
index 52d8ec3..042df70 100644
--- a/proofs/agda/characteristic/N5Falsifier.agda
+++ b/proofs/agda/characteristic/N5Falsifier.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/NonTruncatable.agda b/proofs/agda/characteristic/NonTruncatable.agda
index 28df91a..dcb496d 100644
--- a/proofs/agda/characteristic/NonTruncatable.agda
+++ b/proofs/agda/characteristic/NonTruncatable.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RecipeNonTriviality.agda b/proofs/agda/characteristic/RecipeNonTriviality.agda
index ce02eb2..dadd32c 100644
--- a/proofs/agda/characteristic/RecipeNonTriviality.agda
+++ b/proofs/agda/characteristic/RecipeNonTriviality.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RecipeSpec.agda b/proofs/agda/characteristic/RecipeSpec.agda
index 41325a5..71c83af 100644
--- a/proofs/agda/characteristic/RecipeSpec.agda
+++ b/proofs/agda/characteristic/RecipeSpec.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RecipeTheorem.agda b/proofs/agda/characteristic/RecipeTheorem.agda
index 94263db..f49e513 100644
--- a/proofs/agda/characteristic/RecipeTheorem.agda
+++ b/proofs/agda/characteristic/RecipeTheorem.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RoleGraded.agda b/proofs/agda/characteristic/RoleGraded.agda
index a5b6c3e..e94490f 100644
--- a/proofs/agda/characteristic/RoleGraded.agda
+++ b/proofs/agda/characteristic/RoleGraded.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RoleMode.agda b/proofs/agda/characteristic/RoleMode.agda
index e99569e..971eae4 100644
--- a/proofs/agda/characteristic/RoleMode.agda
+++ b/proofs/agda/characteristic/RoleMode.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RoleModeGrade.agda b/proofs/agda/characteristic/RoleModeGrade.agda
index 8ff75f6..df2eb2c 100644
--- a/proofs/agda/characteristic/RoleModeGrade.agda
+++ b/proofs/agda/characteristic/RoleModeGrade.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/RoleRole.agda b/proofs/agda/characteristic/RoleRole.agda
index a0fa64d..6531a36 100644
--- a/proofs/agda/characteristic/RoleRole.agda
+++ b/proofs/agda/characteristic/RoleRole.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/characteristic/VisibleConstraintAudit.agda b/proofs/agda/characteristic/VisibleConstraintAudit.agda
index 6356d91..4b913da 100644
--- a/proofs/agda/characteristic/VisibleConstraintAudit.agda
+++ b/proofs/agda/characteristic/VisibleConstraintAudit.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/All.agda b/proofs/agda/examples/All.agda
index b6dcfe2..426cf13 100644
--- a/proofs/agda/examples/All.agda
+++ b/proofs/agda/examples/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/EchoVsSigma.agda b/proofs/agda/examples/EchoVsSigma.agda
index 76aad45..483a9e0 100644
--- a/proofs/agda/examples/EchoVsSigma.agda
+++ b/proofs/agda/examples/EchoVsSigma.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/EpistemicUpdate.agda b/proofs/agda/examples/EpistemicUpdate.agda
index 3df1136..2f92bf6 100644
--- a/proofs/agda/examples/EpistemicUpdate.agda
+++ b/proofs/agda/examples/EpistemicUpdate.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/LinearErasure.agda b/proofs/agda/examples/LinearErasure.agda
index 663c59f..7a1d56c 100644
--- a/proofs/agda/examples/LinearErasure.agda
+++ b/proofs/agda/examples/LinearErasure.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/Transport.agda b/proofs/agda/examples/Transport.agda
index f7c9ebb..93a476f 100644
--- a/proofs/agda/examples/Transport.agda
+++ b/proofs/agda/examples/Transport.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/examples/TropicalArgmin.agda b/proofs/agda/examples/TropicalArgmin.agda
index c99427f..5e8e4db 100644
--- a/proofs/agda/examples/TropicalArgmin.agda
+++ b/proofs/agda/examples/TropicalArgmin.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/proofs/agda/experimental/echo-additive/All.agda b/proofs/agda/experimental/echo-additive/All.agda
index c71a56a..b0b1594 100644
--- a/proofs/agda/experimental/echo-additive/All.agda
+++ b/proofs/agda/experimental/echo-additive/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL aggregate root for CI only.
 --
diff --git a/proofs/agda/experimental/echo-additive/Grade.agda b/proofs/agda/experimental/echo-additive/Grade.agda
index 309258e..d28eca5 100644
--- a/proofs/agda/experimental/echo-additive/Grade.agda
+++ b/proofs/agda/experimental/echo-additive/Grade.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R0 deliverable.
 -- ℕ ∪ {∞} grade semiring for the echo-types additive tower.
diff --git a/proofs/agda/experimental/echo-additive/GradedAdjunction.agda b/proofs/agda/experimental/echo-additive/GradedAdjunction.agda
index 54a6192..6563a88 100644
--- a/proofs/agda/experimental/echo-additive/GradedAdjunction.agda
+++ b/proofs/agda/experimental/echo-additive/GradedAdjunction.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R4 deliverable: the F_r ⊣ U_r ADJUNCTION ATTEMPT on the
 -- CONTENT-FAITHFUL carrier (terminating-condition (ii) discriminator).
diff --git a/proofs/agda/experimental/echo-additive/GradedCarrier.agda b/proofs/agda/experimental/echo-additive/GradedCarrier.agda
index 678c5b8..267502a 100644
--- a/proofs/agda/experimental/echo-additive/GradedCarrier.agda
+++ b/proofs/agda/experimental/echo-additive/GradedCarrier.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R2 deliverable (SHARED CARRIER).
 -- Carrier D : Grade → Set → Set for the echo-additive composition lines,
diff --git a/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda b/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda
index 84f597f..5b45e57 100644
--- a/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda
+++ b/proofs/agda/experimental/echo-additive/GradedCarrierFaithful.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R4 deliverable (CONTENT-FAITHFUL CARRIER).
 -- The variant carrier named in GradedComonad §7: a finite layer carries a
diff --git a/proofs/agda/experimental/echo-additive/GradedComonad.agda b/proofs/agda/experimental/echo-additive/GradedComonad.agda
index deb7eca..1bb2f8b 100644
--- a/proofs/agda/experimental/echo-additive/GradedComonad.agda
+++ b/proofs/agda/experimental/echo-additive/GradedComonad.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R3 SECONDARY LINE (comonadic δ).
 -- Colaxator δ_{r,s} : D (r +g s) A → D r (D s A), the SPLITTING direction,
diff --git a/proofs/agda/experimental/echo-additive/GradedMonad.agda b/proofs/agda/experimental/echo-additive/GradedMonad.agda
index 26791be..1bd411d 100644
--- a/proofs/agda/experimental/echo-additive/GradedMonad.agda
+++ b/proofs/agda/experimental/echo-additive/GradedMonad.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R3 PRIMARY LINE: the graded monad multiplication φ.
 -- AUTHOR-GATED comparative variance protocol (R2/R3). NOT merged to main (W6).
diff --git a/proofs/agda/experimental/echo-additive/VarianceGate.agda b/proofs/agda/experimental/echo-additive/VarianceGate.agda
index ddf31d8..8e45839 100644
--- a/proofs/agda/experimental/echo-additive/VarianceGate.agda
+++ b/proofs/agda/experimental/echo-additive/VarianceGate.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- EXPERIMENTAL — R1 deliverable: variance gate framing.
 -- This file contains NO proven theorems. Every type signature below is
diff --git a/scripts/kernel-guard.sh b/scripts/kernel-guard.sh
index 5050423..319798d 100644
--- a/scripts/kernel-guard.sh
+++ b/scripts/kernel-guard.sh
@@ -75,8 +75,9 @@ for src in "$ECHO_SRC" "$KERNEL_SRC"; do
   head -1 "$src" | grep -q -- '--without-K' \
     || fail "$src: missing --without-K in the OPTIONS pragma"
 
-  # No safety-relaxing flag, anywhere.
-  if grep -nE -- '--(type-in-type|cubical|rewriting|sized-types|guardedness|injective-type-constructors|no-positivity-check|no-termination-check|allow-unsolved-metas)' "$src" >/dev/null; then
+  # No safety-relaxing flag, anywhere.  Whole flags only: `--cubical-compatible`
+  # (which strengthens, not relaxes) must not match `--cubical`.
+  if grep -nE -- '--(type-in-type|cubical|erased-cubical|rewriting|sized-types|guardedness|injective-type-constructors|no-positivity-check|no-termination-check|allow-unsolved-metas)([[:space:]]|#|$)' "$src" >/dev/null; then
     fail "$src: a safety-relaxing OPTIONS flag is present"
   fi
 
diff --git a/tutorial/All.agda b/tutorial/All.agda
index 4fcc206..9de7d9c 100644
--- a/tutorial/All.agda
+++ b/tutorial/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/epistemic_erasure/All.agda b/tutorial/epistemic_erasure/All.agda
index cc2c3c8..c86c82d 100644
--- a/tutorial/epistemic_erasure/All.agda
+++ b/tutorial/epistemic_erasure/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/epistemic_erasure/EpistemicErasure.agda b/tutorial/epistemic_erasure/EpistemicErasure.agda
index f8934a4..f7e99f0 100644
--- a/tutorial/epistemic_erasure/EpistemicErasure.agda
+++ b/tutorial/epistemic_erasure/EpistemicErasure.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/epistemic_erasure/Smoke.agda b/tutorial/epistemic_erasure/Smoke.agda
index 9b06b27..0692fe0 100644
--- a/tutorial/epistemic_erasure/Smoke.agda
+++ b/tutorial/epistemic_erasure/Smoke.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/provenance_debugging/All.agda b/tutorial/provenance_debugging/All.agda
index 38b3474..af23125 100644
--- a/tutorial/provenance_debugging/All.agda
+++ b/tutorial/provenance_debugging/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/provenance_debugging/ProvenanceDebugging.agda b/tutorial/provenance_debugging/ProvenanceDebugging.agda
index 2cd9a50..59bdda2 100644
--- a/tutorial/provenance_debugging/ProvenanceDebugging.agda
+++ b/tutorial/provenance_debugging/ProvenanceDebugging.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/provenance_debugging/Smoke.agda b/tutorial/provenance_debugging/Smoke.agda
index dffd0e1..1d813dd 100644
--- a/tutorial/provenance_debugging/Smoke.agda
+++ b/tutorial/provenance_debugging/Smoke.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/region_exit_audit/All.agda b/tutorial/region_exit_audit/All.agda
index 6dcaba2..3dfd67e 100644
--- a/tutorial/region_exit_audit/All.agda
+++ b/tutorial/region_exit_audit/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/region_exit_audit/RegionExitAudit.agda b/tutorial/region_exit_audit/RegionExitAudit.agda
index 579a67f..7d59728 100644
--- a/tutorial/region_exit_audit/RegionExitAudit.agda
+++ b/tutorial/region_exit_audit/RegionExitAudit.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
diff --git a/tutorial/region_exit_audit/Smoke.agda b/tutorial/region_exit_audit/Smoke.agda
index 1fdd842..fa6b73b 100644
--- a/tutorial/region_exit_audit/Smoke.agda
+++ b/tutorial/region_exit_audit/Smoke.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- SPDX-License-Identifier: MPL-2.0
 -- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>