Higher Structures in Homotopy Type Theory

TL;DR

This paper explores the challenges of constructing higher homotopy types within Homotopy Type Theory, focusing on infinite coherence data and the development of the meta-theory in Univalent Foundations.

Contribution

It analyzes the limitations of current type formers for higher structures and discusses potential solutions for complex coherence and meta-theoretical issues.

Findings

Current type formers are insufficient for some higher structures

Problems with infinite coherence data like semi-simplicial types

Proposed solutions for developing the meta-theory

Abstract

The intended model of the homotopy type theories used in Univalent Foundations is the infinity-category of homotopy types, also known as infinity-groupoids. The problem of higher structures is that of constructing the homotopy types needed for mathematics, especially those that aren't sets. The current repertoire of constructions, including the usual type formers and higher inductive types, suffice for many but not all of these. We discuss the problematic cases, typically those involving an infinite hierarchy of coherence data such as semi-simplicial types, as well as the problem of developing the meta-theory of homotopy type theories in Univalent Foundations. We also discuss some proposed solutions.