diff --git a/src/EpistemicTypes/Access.agda b/src/EpistemicTypes/Access.agda
index fde30cd..f2b99a3 100644
--- a/src/EpistemicTypes/Access.agda
+++ b/src/EpistemicTypes/Access.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Access where
 
diff --git a/src/EpistemicTypes/All.agda b/src/EpistemicTypes/All.agda
index 11812c5..b9af38e 100644
--- a/src/EpistemicTypes/All.agda
+++ b/src/EpistemicTypes/All.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.All where
 
diff --git a/src/EpistemicTypes/Applications/IntegerModel.agda b/src/EpistemicTypes/Applications/IntegerModel.agda
index e4b14d9..f4e1ead 100644
--- a/src/EpistemicTypes/Applications/IntegerModel.agda
+++ b/src/EpistemicTypes/Applications/IntegerModel.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / IntegerModel
 --
diff --git a/src/EpistemicTypes/Applications/OrderedGroup.agda b/src/EpistemicTypes/Applications/OrderedGroup.agda
index 374557b..40f4cd3 100644
--- a/src/EpistemicTypes/Applications/OrderedGroup.agda
+++ b/src/EpistemicTypes/Applications/OrderedGroup.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / OrderedGroup
 --
diff --git a/src/EpistemicTypes/Applications/QCriterion.agda b/src/EpistemicTypes/Applications/QCriterion.agda
index 5da05d7..a0addc1 100644
--- a/src/EpistemicTypes/Applications/QCriterion.agda
+++ b/src/EpistemicTypes/Applications/QCriterion.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / QCriterion
 --
diff --git a/src/EpistemicTypes/Applications/RapidNJExamples.agda b/src/EpistemicTypes/Applications/RapidNJExamples.agda
index 3f93b49..45b7dc9 100644
--- a/src/EpistemicTypes/Applications/RapidNJExamples.agda
+++ b/src/EpistemicTypes/Applications/RapidNJExamples.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / RapidNJExamples
 --
diff --git a/src/EpistemicTypes/Applications/RapidNJSkip.agda b/src/EpistemicTypes/Applications/RapidNJSkip.agda
index 17e7921..1e01e59 100644
--- a/src/EpistemicTypes/Applications/RapidNJSkip.agda
+++ b/src/EpistemicTypes/Applications/RapidNJSkip.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / RapidNJSkip
 --
diff --git a/src/EpistemicTypes/Applications/SortedRow.agda b/src/EpistemicTypes/Applications/SortedRow.agda
index d9561f2..645458c 100644
--- a/src/EpistemicTypes/Applications/SortedRow.agda
+++ b/src/EpistemicTypes/Applications/SortedRow.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Applications / SortedRow
 --
diff --git a/src/EpistemicTypes/Base.agda b/src/EpistemicTypes/Base.agda
index afaf445..aed3f87 100644
--- a/src/EpistemicTypes/Base.agda
+++ b/src/EpistemicTypes/Base.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Base where
 
diff --git a/src/EpistemicTypes/ContinuityExamples.agda b/src/EpistemicTypes/ContinuityExamples.agda
index 40ddd01..99ce13d 100644
--- a/src/EpistemicTypes/ContinuityExamples.agda
+++ b/src/EpistemicTypes/ContinuityExamples.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.ContinuityExamples where
 
diff --git a/src/EpistemicTypes/EchoBridge.agda b/src/EpistemicTypes/EchoBridge.agda
index 045369f..4e3f898 100644
--- a/src/EpistemicTypes/EchoBridge.agda
+++ b/src/EpistemicTypes/EchoBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.EchoBridge where
 
diff --git a/src/EpistemicTypes/Examples.agda b/src/EpistemicTypes/Examples.agda
index 2734813..fadff87 100644
--- a/src/EpistemicTypes/Examples.agda
+++ b/src/EpistemicTypes/Examples.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Examples where
 
diff --git a/src/EpistemicTypes/Kripke/Belief.agda b/src/EpistemicTypes/Kripke/Belief.agda
index 8c256e3..dec850d 100644
--- a/src/EpistemicTypes/Kripke/Belief.agda
+++ b/src/EpistemicTypes/Kripke/Belief.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
 --
diff --git a/src/EpistemicTypes/Kripke/Dependence.agda b/src/EpistemicTypes/Kripke/Dependence.agda
index 3ced10e..d158f0f 100644
--- a/src/EpistemicTypes/Kripke/Dependence.agda
+++ b/src/EpistemicTypes/Kripke/Dependence.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
 --
diff --git a/src/EpistemicTypes/Kripke/Frame.agda b/src/EpistemicTypes/Kripke/Frame.agda
index c407d5b..4a1fd5e 100644
--- a/src/EpistemicTypes/Kripke/Frame.agda
+++ b/src/EpistemicTypes/Kripke/Frame.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
 --
diff --git a/src/EpistemicTypes/Kripke/Indexed.agda b/src/EpistemicTypes/Kripke/Indexed.agda
index ec9d6be..f9d9bcc 100644
--- a/src/EpistemicTypes/Kripke/Indexed.agda
+++ b/src/EpistemicTypes/Kripke/Indexed.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
 --
diff --git a/src/EpistemicTypes/Kripke/Residual.agda b/src/EpistemicTypes/Kripke/Residual.agda
index 78fb4a2..aa218ba 100644
--- a/src/EpistemicTypes/Kripke/Residual.agda
+++ b/src/EpistemicTypes/Kripke/Residual.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
 --
diff --git a/src/EpistemicTypes/ProofTransport.agda b/src/EpistemicTypes/ProofTransport.agda
index 1fc2173..cfcc292 100644
--- a/src/EpistemicTypes/ProofTransport.agda
+++ b/src/EpistemicTypes/ProofTransport.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Proof statuses carry a successful check and entail a caller-supplied meaning.
 -- Soundness is relative to Meaning and the verifier's explicit soundness proof.
diff --git a/src/EpistemicTypes/ProofTransportExample.agda b/src/EpistemicTypes/ProofTransportExample.agda
index d480aad..6d24ecc 100644
--- a/src/EpistemicTypes/ProofTransportExample.agda
+++ b/src/EpistemicTypes/ProofTransportExample.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 -- Executable Boolean certificate checks, semantic soundness, and countercases.
 -- ArtifactIsTrue means a Boolean equality, not that a physical action occurred.
diff --git a/src/EpistemicTypes/ReadConsistency.agda b/src/EpistemicTypes/ReadConsistency.agda
index 0b72914..b86334c 100644
--- a/src/EpistemicTypes/ReadConsistency.agda
+++ b/src/EpistemicTypes/ReadConsistency.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.ReadConsistency where
 
diff --git a/src/EpistemicTypes/SurrealBridge.agda b/src/EpistemicTypes/SurrealBridge.agda
index 66fb4fd..a5807ea 100644
--- a/src/EpistemicTypes/SurrealBridge.agda
+++ b/src/EpistemicTypes/SurrealBridge.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.SurrealBridge where
 
diff --git a/src/EpistemicTypes/Warrant.agda b/src/EpistemicTypes/Warrant.agda
index c69db5e..89e256e 100644
--- a/src/EpistemicTypes/Warrant.agda
+++ b/src/EpistemicTypes/Warrant.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 
 module EpistemicTypes.Warrant where
 
diff --git a/tests/check-proofs.sh b/tests/check-proofs.sh
index 55c3fbe..c55b2f3 100644
--- a/tests/check-proofs.sh
+++ b/tests/check-proofs.sh
@@ -9,6 +9,6 @@ mapfile -t modules < <(find src/EpistemicTypes -name '*.agda' | sort)
 [[ ${#modules[@]} -gt 0 ]] || { echo 'FAIL: no proof modules'; exit 1; }
 for module in "${modules[@]}"; do
   agda --no-libraries --safe --without-K --double-check --ignore-interfaces \
-    -W error -i src "$module"
+    -W error -W noUnsupportedIndexedMatch -i src "$module"
 done
 printf 'PASS: %s source modules checked under the required proof discipline\n' "${#modules[@]}"
diff --git a/tests/check-rejections.sh b/tests/check-rejections.sh
index a7b2bbd..c529d89 100644
--- a/tests/check-rejections.sh
+++ b/tests/check-rejections.sh
@@ -12,7 +12,7 @@ actual_files=$(rg --files tests/reject -g '*.agda' | sort)
 [[ "$actual_files" == "$expected_files" ]] || { echo 'FAIL: rejection manifest differs from files'; exit 1; }
 for fixture in "${fixtures[@]}"; do
   status=0
-  diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error \
+  diagnostic=$(agda --no-libraries --safe --without-K --double-check --ignore-interfaces -W error -W noUnsupportedIndexedMatch \
     -i src -i tests/reject "tests/reject/$fixture.agda" 2>&1) || status=$?
   if [[ "$status" -eq 0 ]]; then
     printf 'FAIL: %s unexpectedly type-checked\n' "$fixture"
diff --git a/tests/reject/BeliefIsKnowledge.agda b/tests/reject/BeliefIsKnowledge.agda
index 43d5e17..1247f78 100644
--- a/tests/reject/BeliefIsKnowledge.agda
+++ b/tests/reject/BeliefIsKnowledge.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
 module BeliefIsKnowledge where
diff --git a/tests/reject/FakeFreshness.agda b/tests/reject/FakeFreshness.agda
index 3206ff2..05365f8 100644
--- a/tests/reject/FakeFreshness.agda
+++ b/tests/reject/FakeFreshness.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module FakeFreshness where
 open import Agda.Builtin.Equality
 open import EpistemicTypes.ReadConsistency
diff --git a/tests/reject/ForgedAcceptance.agda b/tests/reject/ForgedAcceptance.agda
index f24f9e0..9e89a56 100644
--- a/tests/reject/ForgedAcceptance.agda
+++ b/tests/reject/ForgedAcceptance.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForgedAcceptance where
 open import Agda.Builtin.Bool using (true; false)
 open import Agda.Builtin.Equality using (refl)
diff --git a/tests/reject/ForgedResidue.agda b/tests/reject/ForgedResidue.agda
index b5612cf..504a5fc 100644
--- a/tests/reject/ForgedResidue.agda
+++ b/tests/reject/ForgedResidue.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForgedResidue where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
diff --git a/tests/reject/ForkedHistory.agda b/tests/reject/ForkedHistory.agda
index a713ea5..dda0cb8 100644
--- a/tests/reject/ForkedHistory.agda
+++ b/tests/reject/ForkedHistory.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ForkedHistory where
 open import EpistemicTypes.ReadConsistency
 import EpistemicTypes.ContinuityExamples as Examples
diff --git a/tests/reject/InventedMigration.agda b/tests/reject/InventedMigration.agda
index 18b9cf8..ed3f927 100644
--- a/tests/reject/InventedMigration.agda
+++ b/tests/reject/InventedMigration.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module InventedMigration where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
diff --git a/tests/reject/LyingVerifier.agda b/tests/reject/LyingVerifier.agda
index 6dc42d1..e5b2c68 100644
--- a/tests/reject/LyingVerifier.agda
+++ b/tests/reject/LyingVerifier.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module LyingVerifier where
 open import Agda.Builtin.Bool using (true; false)
 open import Agda.Builtin.Equality using (refl)
diff --git a/tests/reject/MismatchedSource.agda b/tests/reject/MismatchedSource.agda
index e6b9efe..ca91543 100644
--- a/tests/reject/MismatchedSource.agda
+++ b/tests/reject/MismatchedSource.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module MismatchedSource where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
diff --git a/tests/reject/ReplayedArtifact.agda b/tests/reject/ReplayedArtifact.agda
index cbbe7c0..ea8f68d 100644
--- a/tests/reject/ReplayedArtifact.agda
+++ b/tests/reject/ReplayedArtifact.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ReplayedArtifact where
 open import Agda.Builtin.Bool using (false)
 open import EpistemicTypes.ProofTransportExample using (Agent; Claim; Artifact; Meaning; Payload; Alice; ArtifactIsTrue; aliceProof)
diff --git a/tests/reject/ReplayedHolder.agda b/tests/reject/ReplayedHolder.agda
index e299817..ac63a0a 100644
--- a/tests/reject/ReplayedHolder.agda
+++ b/tests/reject/ReplayedHolder.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module ReplayedHolder where
 open import Agda.Builtin.Bool using (true)
 open import EpistemicTypes.ProofTransportExample using (Bob; ArtifactIsTrue; module HolderBoundary)
diff --git a/tests/reject/StaleSample.agda b/tests/reject/StaleSample.agda
index 6213460..66c01f6 100644
--- a/tests/reject/StaleSample.agda
+++ b/tests/reject/StaleSample.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module StaleSample where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Equality
diff --git a/tests/reject/UncheckedSkip.agda b/tests/reject/UncheckedSkip.agda
index 53897ae..094a7ba 100644
--- a/tests/reject/UncheckedSkip.agda
+++ b/tests/reject/UncheckedSkip.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 -- Rejection control: a skip whose check was not accepted.
 --
 -- The four-taxon scan below is unscannable past its cursor.  With r = 4
diff --git a/tests/reject/UnderstatedBound.agda b/tests/reject/UnderstatedBound.agda
index f3f940a..f1cf084 100644
--- a/tests/reject/UnderstatedBound.agda
+++ b/tests/reject/UnderstatedBound.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --safe --without-K #-}
+{-# OPTIONS --safe --without-K --cubical-compatible --exact-split --no-sized-types --no-guardedness #-}
 module UnderstatedBound where
 open import Agda.Builtin.Bool
 open import Agda.Builtin.Nat