Generating Higher Identity Proofs in Homotopy Type Theory

TL;DR

This paper demonstrates that homotopy type theory can model omega-categories through a translation principle, enabling more efficient proofs about higher identity types and their structures.

Contribution

It introduces a translation principle that interprets omega-category operations within homotopy type theory, bridging the two frameworks.

Findings

Homotopy type theory models weak omega-groupoids as omega-categories.

The translation principle simplifies proofs about higher identity types.

Application to the Eckmann-Hilton cell reduces proof complexity.

Abstract

Finster and Mimram have defined a dependent type theory called CaTT, which describes the structure of omega-categories. Types in homotopy type theory with their higher identity types form weak omega-groupoids, so they are in particular weak omega-categories. In this article, we show that this principle makes homotopy type theory into a model of CaTT, by defining a translation principle that interprets an operation on the cell of an omega-category as an operation on higher identity types. We then illustrate how this translation allows to leverage several mechanisation principles that are available in CaTT, to reduce the proof effort required to derive results about the structure of identity types, such as the existence of an Eckmann-Hilton cell.