2026-07-20T15:07:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26814 2026-07-09T11:31:09Z ddc:004 open_access

Eliminating Reversals from Cubical Type Theories Cavallo, Evan Sattler, Christian Dependent type theory univalence cubical type theory 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Evan Cavallo and Christian Sattler 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.27 urn:nbn:de:0030-drops-268148 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.27 eng https://creativecommons.org/licenses/by/4.0/legalcode