Eliminating reversals from cubical type theories

Evan Cavallo , Christian Sattler

Authors on Pith no claims yet

Pith reviewed 2026-05-15 03:19 UTC · model grok-4.3

classification 💻 cs.LO

keywords typecubicalintervaltheoriestheoryreversalsreversalconstruction

0 comments

The pith

Adding reversals to self-dual cubical interval theories yields a conservative extension via the twist construction, enabling the first models whose homotopy theory matches topological spaces.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Cubical type theories build equalities from paths along an abstract interval with endpoints. A reversal is an operation that flips the interval, swapping the two ends. For interval theories that are already self-dual, the authors prove that freely adding such a reversal does not prove any new statements about the original theory. The proof uses a twist construction: take the product of the interval with a copy of itself flipped, then swap coordinates to define the reversal. This works for opaque theories that do not simplify the filling operations at concrete types. The same construction also produces models of the strict theory with reversals inside ordinary cubical sets that lack reversals, giving the first such model whose paths behave like continuous paths in topology.

Core claim

For cubical type theories with self-dual interval theories, the extension with a reversal that internalizes the duality is a conservative extension. Using the same twist construction, we also construct models of strict cubical type theory with reversals in categories of cubical sets without reversals.

Load-bearing premise

The result applies only to opaque cubical type theories without strict equations reducing the filling operator at concrete type formers or eliminators from higher inductive types at path constructors; if a theory has such equations, the conservativity may fail.

read the original abstract

Cubical type theories are designed around an abstract unit interval from which types of paths, used to represent equalities, are defined. Varying the operations available on this interval yields different type theories. A reversal is an involutive operator on the interval that swaps its two endpoints. We show that for cubical type theories with self-dual interval theories, such as the minimal theory of two endpoints or the theory of a bounded distributive lattice, the extension of the theory with a reversal that internalizes the duality is a conservative extension. The key tool is a "twist construction": the product of an interval and its dual is again an interval with a reversal given by swapping coordinates. Our conservativity result applies to "opaque" cubical type theories, without strict equations reducing the filling operator at concrete type formers or eliminators from higher inductive types at path constructors. Using the same twist construction, we also construct models of strict cubical type theory with reversals in categories of cubical sets without reversals. We thereby give the first model of a theory with reversals whose homotopy theory corresponds to that of topological spaces.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard axioms of category theory and dependent type theory plus the definition of an opaque cubical type theory; no free parameters or invented entities are introduced.

axioms (2)

standard math Standard axioms of dependent type theory and the definition of cubical sets with an interval object
Invoked throughout to define paths, fillings, and conservativity.
domain assumption The interval theory is self-dual (e.g., minimal two-endpoint theory or bounded distributive lattice)
Stated as the precondition for the conservativity result.

pith-pipeline@v0.9.0 · 5490 in / 1331 out tokens · 26767 ms · 2026-05-15T03:19:06.039941+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AlexanderDuality.lean alexander_duality_circle_linking echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

the product of an interval and its dual is again an interval with a reversal given by swapping coordinates

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.