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.

翻译：立方体类型论围绕一个抽象单位区间设计，由此定义用于表示等式的路径类型。对该区间上可用操作的不同选择会产生不同的类型论。反转是该区间上交换其两个端点的对合算子。我们证明，对于具有自对偶区间理论的立方体类型论（例如两个端点的最小理论或有界分配格理论），通过添加内化对偶性的反转来扩展该理论是一种保守扩展。关键工具是“扭转构造”：一个区间与其对偶的乘积再次成为一个区间，其反转由交换坐标给出。我们的保守性结果适用于“不透明”立方体类型论，其中没有严格等式来约简具体类型形成子上的填充算子或高阶归纳类型路径构造子上的消去子。利用相同的扭转构造，我们还在无反转的立方体集合范畴中构造了带反转的严格立方体类型论的模型。由此，我们首次给出了其同伦论对应于拓扑空间理论的带反转类型论的模型。