agda · Taneb · Mar 20, 2026 · Mar 21, 2026 · jamesmckinna · Mar 25, 2026
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -6,6 +6,8 @@ The library has been tested using Agda 2.8.0.
 Highlights
 ----------
 
+* Modules that previously used `--cubical-compatible` once again use `--without-K`.
+
 Bug-fixes
 ---------
 

diff --git a/GenerateEverything.hs b/GenerateEverything.hs
@@ -255,9 +255,9 @@ classify fp hd ls
   -- We start with sanity checks
   | isUnsafe && safe          = throwError $ fp ++ contradiction "unsafe" "safe"
   | not (isUnsafe || safe)    = throwError $ fp ++ uncategorized "unsafe" "safe"
-  | isWithK && cubicalC       = throwError $ fp ++ contradiction "as relying on K" "cubical-compatible"
+  | isWithK && withoutK       = throwError $ fp ++ contradiction "as relying on K" "without-K"
   | isWithK && not withK      = throwError $ fp ++ missingWithK
-  | not (isWithK || cubicalC) = throwError $ fp ++ uncategorized "as relying on K" "cubical-compatible"
+  | not (isWithK || withoutK) = throwError $ fp ++ uncategorized "as relying on K" "without-K"
   -- And then perform the actual classification
   | otherwise = do
       let safety = if | safe -> Safe
@@ -273,9 +273,9 @@ classify fp hd ls
     isUnsafe = isUnsafeModule fp
 
     -- based on detected OPTIONS
-    safe        = option "--safe"
-    withK       = option "--with-K"
-    cubicalC    = option "--cubical-compatible"
+    safe     = option "--safe"
+    withK    = option "--with-K"
+    withoutK = option "--without-K"
 
     -- based on detected comment in header
     deprecated  = let detect = List.isSubsequenceOf "This module is DEPRECATED."

diff --git a/HACKING.md b/HACKING.md
@@ -21,7 +21,7 @@ What is an acceptable contribution?
   for purely computational contributions this will involve adding tests.
 
 - It should use the minimal set of Agda features, i.e. it should normally use
-  the Agda option pragmas `--cubical-compatible` and `--safe`, with the occasional use of
+  the Agda option pragmas `--without-K` and `--safe`, with the occasional use of
   `--with-K`, `--sized`, `--guardedness` in certain situations.
 
 In general, if something is in a general undergraduate Computer Science or Mathematics
@@ -150,11 +150,11 @@ proper header, and a brief description of what the module is for, e.g.
 ```
 
 If possible, each module should use the options `--safe` and
-`--cubical-compatible`. You can achieve this by placing the following
+`--without-K`. You can achieve this by placing the following
 pragma under the header and before any other line of code (including
 the module name):
 ```
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 ```
 
 If a module cannot be made safe or needs the `--with-K` option then it should be

diff --git a/README.md b/README.md
@@ -69,9 +69,9 @@ Most of the library can be type-checked using the `--safe` flag. Please consult
 [GenerateEverything.hs](https://github.com/agda/agda-stdlib/blob/master/GenerateEverything.hs#L32-L82)
 for a full list of modules that use unsafe features.
 
-#### The `--cubical-compatible` flag
+#### The `--without-K` flag
 
-Most of the library can be type-checked using the `--cubical-compatible` flag, which since Agda v2.6.3 supersedes the former `--without-K` flag. Please consult
+Most of the library can be type-checked using the `--without-K` flag. Please consult
 [GenerateEverything.hs](https://github.com/agda/agda-stdlib/blob/master/GenerateEverything.hs#L91-L111)
 for a full list of modules that use axiom K, requiring the `--with-K` flag.
 

diff --git a/doc/README/Case.agda b/doc/README/Case.agda
@@ -5,7 +5,7 @@
 -- pattern-matching lambda abstractions
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Case where
 

diff --git a/doc/README/Data/Container/FreeMonad.agda b/doc/README/Data/Container/FreeMonad.agda
@@ -5,7 +5,7 @@
 -- used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Container.FreeMonad where
 

diff --git a/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda b/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda
@@ -4,7 +4,7 @@
 -- Example of multi-sorted algebras as indexed containers
 ------------------------------------------------------------------------
 
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --safe --without-K #-}
 
 module README.Data.Container.Indexed.MultiSortedAlgebraExample where
 

diff --git a/doc/README/Data/Default.agda b/doc/README/Data/Default.agda
@@ -5,7 +5,7 @@
 -- argument that default to a specified value if none is passed.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Default where
 

diff --git a/doc/README/Data/Fin/Relation/Unary/Top.agda b/doc/README/Data/Fin/Relation/Unary/Top.agda
@@ -12,7 +12,7 @@
 -- together with their corresponding properties in `Data.Fin.Properties`.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Fin.Relation.Unary.Top where
 

diff --git a/doc/README/Data/Fin/Substitution/UntypedLambda.agda b/doc/README/Data/Fin/Substitution/UntypedLambda.agda
@@ -5,7 +5,7 @@
 -- of substitution for the untyped λ-calculus, along with some lemmas
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Fin.Substitution.UntypedLambda where
 

diff --git a/doc/README/Data/Integer.agda b/doc/README/Data/Integer.agda
@@ -5,7 +5,7 @@
 -- operations and properties are defined, and how they can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --without-K #-}
 
 module README.Data.Integer where
 

diff --git a/doc/README/Data/List/Relation/Ternary/Interleaving.agda b/doc/README/Data/List/Relation/Ternary/Interleaving.agda
@@ -4,7 +4,7 @@
 -- Examples showing how the notion of Interleaving can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.List.Relation.Ternary.Interleaving where
 

diff --git a/doc/README/Data/Nat.agda b/doc/README/Data/Nat.agda
@@ -5,7 +5,7 @@
 -- operations and properties are defined, and how they can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --without-K #-}
 
 module README.Data.Nat where
 

diff --git a/doc/README/Data/Rational.agda b/doc/README/Data/Rational.agda
@@ -5,7 +5,7 @@
 -- operations and properties are defined, and how they can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible #-}
+{-# OPTIONS --without-K #-}
 
 module README.Data.Rational where
 

diff --git a/doc/README/Data/Tree/AVL.agda b/doc/README/Data/Tree/AVL.agda
@@ -4,7 +4,7 @@
 -- Some examples showing how the AVL tree module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Tree.AVL where
 

diff --git a/doc/README/Data/Tree/Binary.agda b/doc/README/Data/Tree/Binary.agda
@@ -4,7 +4,7 @@
 -- Some examples showing how the Binary tree module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Tree.Binary where
 

diff --git a/doc/README/Data/Tree/Rose.agda b/doc/README/Data/Tree/Rose.agda
@@ -4,7 +4,7 @@
 -- Some examples showing how the Rose tree module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Tree.Rose where
 

diff --git a/doc/README/Data/Trie/NonDependent.agda b/doc/README/Data/Trie/NonDependent.agda
@@ -4,7 +4,7 @@
 -- Example use case for a trie: a wee generic lexer
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --sized-types #-}
+{-# OPTIONS --without-K --sized-types #-}
 
 module README.Data.Trie.NonDependent where
 

diff --git a/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda b/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
@@ -8,7 +8,7 @@
 -- section.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Vec.Relation.Binary.Equality.Cast where
 

diff --git a/doc/README/Data/Wrap.agda b/doc/README/Data/Wrap.agda
@@ -4,7 +4,7 @@
 -- An example of how to use `Wrap` to help term inference.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Data.Wrap where
 

diff --git a/doc/README/Debug/Trace.agda b/doc/README/Debug/Trace.agda
@@ -4,7 +4,7 @@
 -- An example showing how the Debug.Trace module can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --rewriting --guardedness #-}
+{-# OPTIONS --without-K --rewriting --guardedness #-}
 
 module README.Debug.Trace where
 

diff --git a/doc/README/Design/Decidability.agda b/doc/README/Design/Decidability.agda
@@ -4,7 +4,7 @@
 -- Examples of decision procedures and how to use them
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Design.Decidability where
 

diff --git a/doc/README/Design/Fixity.agda b/doc/README/Design/Fixity.agda
@@ -4,7 +4,7 @@
 -- Documentation describing some of the fixity choices
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 -- There is no actual code in here, just design note.
 

diff --git a/doc/README/Effect/Monad/Partiality.agda b/doc/README/Effect/Monad/Partiality.agda
@@ -4,7 +4,7 @@
 -- Example showing the use of the partiality Monad
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe --guardedness #-}
+{-# OPTIONS --without-K --safe --guardedness #-}
 
 module README.Effect.Monad.Partiality where
 

diff --git a/doc/README/Inspect.agda b/doc/README/Inspect.agda
@@ -5,7 +5,7 @@
 -- it is implemented in the standard library.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Inspect where
 

diff --git a/doc/README/Nary.agda b/doc/README/Nary.agda
@@ -5,7 +5,7 @@
 -- can be used
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Nary where
 

diff --git a/doc/README/Reflection/External.agda b/doc/README/Reflection/External.agda
@@ -8,7 +8,7 @@
 -- section on Reflection in the Agda user manual for more details.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --allow-exec #-}
+{-# OPTIONS --without-K --allow-exec #-}
 
 module README.Reflection.External where
 

diff --git a/doc/README/Relation/Binary/TypeClasses.agda b/doc/README/Relation/Binary/TypeClasses.agda
@@ -4,7 +4,7 @@
 -- Usage examples of typeclasses for binary relations
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Relation.Binary.TypeClasses where
 

diff --git a/doc/README/Tactic/Cong.agda b/doc/README/Tactic/Cong.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module README.Tactic.Cong where
 

diff --git a/doc/README/Text/Printf.agda b/doc/README/Text/Printf.agda
@@ -4,7 +4,7 @@
 -- Examples of format strings and printf
 ------------------------------------------------------------------------
 
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --safe --without-K #-}
 
 module README.Text.Printf where
 

diff --git a/doc/README/Text/Tabular.agda b/doc/README/Text/Tabular.agda
@@ -4,7 +4,7 @@
 -- Examples of printing list and vec-based tables
 ------------------------------------------------------------------------
 
-{-# OPTIONS --safe --cubical-compatible #-}
+{-# OPTIONS --safe --without-K #-}
 
 module README.Text.Tabular where
 

diff --git a/src/Algebra.agda b/src/Algebra.agda
@@ -5,7 +5,7 @@
 -- (packed in records together with sets, operations, etc.)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra where
 

diff --git a/src/Algebra/Apartness.agda b/src/Algebra/Apartness.agda
@@ -4,7 +4,7 @@
 -- Algebraic objects with an apartness relation
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Apartness where
 

diff --git a/src/Algebra/Apartness/Bundles.agda b/src/Algebra/Apartness/Bundles.agda
@@ -4,7 +4,7 @@
 -- Bundles for local algebraic structures
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Apartness.Bundles where
 

diff --git a/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda b/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
@@ -4,7 +4,7 @@
 -- Properties of Heyting Commutative Rings
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Apartness.Bundles using (HeytingCommutativeRing)
 

diff --git a/src/Algebra/Apartness/Structures.agda b/src/Algebra/Apartness/Structures.agda
@@ -4,7 +4,7 @@
 -- Algebraic structures with an apartness relation
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Algebra.Core using (Op₁; Op₂)
 open import Relation.Binary.Core using (Rel)

diff --git a/src/Algebra/Bundles.agda b/src/Algebra/Bundles.agda
@@ -7,7 +7,7 @@
 
 -- The contents of this module should be accessed via `Algebra`.
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Bundles where
 

diff --git a/src/Algebra/Bundles/Raw.agda b/src/Algebra/Bundles/Raw.agda
@@ -4,7 +4,7 @@
 -- Definitions of 'raw' bundles
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Bundles.Raw where
 

diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda
@@ -5,7 +5,7 @@
 -- commutativity) that don't require the equality relation to be a setoid.
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Consequences.Base
   {a} {A : Set a} where

diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda
@@ -5,7 +5,7 @@
 -- commutativity (specialised to propositional equality)
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 module Algebra.Consequences.Propositional
   {a} {A : Set a} where

diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda
@@ -5,7 +5,7 @@
 -- commutativity, when the underlying relation is a setoid
 ------------------------------------------------------------------------
 
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS --without-K --safe #-}
 
 open import Relation.Binary.Bundles using (Setoid)
 open import Relation.Binary.Definitions
-Original file line number
+Diff line change
@@ Expand Up / @@ -6,6 +6,8 @@ The library has been tested using Agda 2.8.0. @@
     Highlights
     ----------
+    * Modules that previously used `--cubical-compatible` once again use `--without-K`.
     Bug-fixes
     ---------
@@ Expand Down @@