Cubical informal type theory: the higher groupoid structure

TL;DR

This paper explores a cubical type theory framework with univalent universes and higher-inductive types, focusing on elementary theorems related to the higher groupoid structure of types, as an alternative to traditional homotopy type theory.

Contribution

It introduces a cubical type theory foundation with univalence and higher-inductive types, and investigates its elementary higher groupoid properties.

Findings

Confirmed the higher groupoid structure of types within the cubical framework

Demonstrated the consistency of univalence in the cubical setting

Established foundational theorems for elementary higher groupoid properties

Abstract

Following a project of developing conventions and notations for informal type theory carried out in the homotopy type theory book for a framework built out of an augmentation of constructive type theory with axioms governing higher-dimensional constructions via Voevodsky's univalance axiom and higher-inductive types, this paper proposes a way of doing informal type theory with a cubical type theory as the underlying foundation instead. To that end, we adopt a cubical type theory recently proposed by Angiuli, Hou (Favonia) and Harper, a framework with a cumulative hierarchy of univalent Kan universes, full univalence and instances of higher-inductive types. In the present paper we confine ourselves to some elementary theorems concerning the higher groupoid structure of types.