Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generating Higher Identity Proofs in Homotopy Type Theory

Thibaut Benjamin

TL;DR

This work develops a formal bridge between CaTT, the dependent type theory for weak $ oldsymbol{igomega}$-categories, and Martin-Löf type theory’s HoTT fragment by a translation that treats CaTT higher cells as higher identity proofs in HoTT. It proves correctness of the translation, and provides an OCaml/Coq-based implementation (CaTT plugin) that generates HoTT terms from CaTT files, enabling mechanised reasoning about identity types through CaTT’s automation. The Eckmann–Hilton cell serves as a concrete demonstration: a CaTT construction yields a substantially shorter, more modular term than a directly written HoTT term, highlighting practical benefits for higher-categorical proofs. The work thereby establishes HoTT as a syntactic model of CaTT and shows how CaTT’s automation can reduce the proof effort required for complex higher-dimensional identities, with potential impact on formalised higher-category theory in proof assistants.

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.

Generating Higher Identity Proofs in Homotopy Type Theory

TL;DR

This work develops a formal bridge between CaTT, the dependent type theory for weak -categories, and Martin-Löf type theory’s HoTT fragment by a translation that treats CaTT higher cells as higher identity proofs in HoTT. It proves correctness of the translation, and provides an OCaml/Coq-based implementation (CaTT plugin) that generates HoTT terms from CaTT files, enabling mechanised reasoning about identity types through CaTT’s automation. The Eckmann–Hilton cell serves as a concrete demonstration: a CaTT construction yields a substantially shorter, more modular term than a directly written HoTT term, highlighting practical benefits for higher-categorical proofs. The work thereby establishes HoTT as a syntactic model of CaTT and shows how CaTT’s automation can reduce the proof effort required for complex higher-dimensional identities, with potential impact on formalised higher-category theory in proof assistants.

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.

Paper Structure

This paper contains 25 sections, 14 theorems, 33 equations, 3 figures.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Related works.
  4. Overview of the paper.
  5. Acknowledgements.
  6. Overview of Martin-Löf type theory
  7. Notations for type theories
  8. Martin-Löf type theory
  9. The dependent type theory CaTT
  10. The type theory GSeTT
  11. Intuition on the semantics.
  12. The type theory CaTT
  13. Ps-contexts and their source and target.
  14. Term constructors.
  15. Implementation and intuition on the semantics
  16. ...and 10 more sections

Key Result

Lemma 1

For every $n\in \mathbb{N}$, the following rules are admissible in HoTT:

Figures (3)

  • Figure 1: Translation from GSeTT terms to HoTT
  • Figure 2: Intuitive illustration of the Eckmann-Hilton cell
  • Figure 3: Definition of the Eckmann-Hilton cell in CaTT

Theorems & Definitions (28)

  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • Remark 1
  • Lemma 3
  • proof
  • Proposition 4
  • proof
  • ...and 18 more