Naive cubical type theory

TL;DR

This paper introduces a naive cubical approach to type theory, providing an informal framework that supports fundamental properties like function extensionality and path induction, serving as a foundational step towards cubical type theories.

Contribution

It presents an informal, cubical style of reasoning in type theory based on a cartesian cubical framework, highlighting elementary results and foundational properties.

Findings

Establishes function extensionality within the naive cubical type theory.

Derives weak connections and path induction principles.

Shows the groupoid structure of types and Eckmann-Hilton duality.

Abstract

This paper proposes a way of doing type theory informally, assuming a cubical style of reasoning. It can thus be viewed as a first step toward a cubical alternative to the program of informalization of type theory carried out in the homotopy type theory book for dependent type theory augmented with axioms for univalence and higher inductive types. We adopt a cartesian cubical type theory proposed by Angiuli, Brunerie, Coquand, Favonia, Harper, and Licata as the implicit foundation, confining our presentation to elementary results such as function extensionality, the derivation of weak connections and path induction, the groupoid structure of types, and the Eckmman-Hilton duality.