Eliminating reversals from cubical type theories

TL;DR

This paper proves that adding a reversal operator to certain cubical type theories is a conservative extension, and constructs models of these theories with reversals in categories of cubical sets.

Contribution

It introduces a twist construction to internalize reversals in cubical type theories and provides the first models linking these theories to topological spaces.

Findings

Reversal extension is conservative for self-dual interval theories.

Constructs models of cubical type theories with reversals in cubical sets.

Establishes a connection between theories with reversals and topological spaces.

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.