A Syntax for Strictly Associative and Unital $\infty$-Categories

TL;DR

This paper introduces a novel type-theoretic framework for strictly associative and unital at-infinity structures, featuring a new insertion rule that simplifies syntax and enables decision procedures for equality.

Contribution

It provides the first formal definition of strictly associative and unital at-infinity categories using a type theory with a novel insertion rule for coherence.

Findings

Defines a new insertion rule for coherence in at-infinity

Develops a decision procedure for equality in the theory

Implements an OCaml tool for verifying higher categorical statements

Abstract

We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions. The key technical device is a new computation rule in the definitional equality of the theory, which we call insertion, defined in terms of a universal property. On terms for which it is defined, this operation "inserts" one of the arguments of a substituted coherence into the coherence itself, appropriately modifying the pasting diagram and result type, and simplifying the syntax in the process. We generate an equational theory from this reduction relation and we study its properties in detail, showing that it yields a decision procedure for equality. Expressed as a type theory, our model is well-adapted for generating and verifying efficient proofs of higher categorical statements. We illustrate this via an OCaml implementation, and give a number of examples, including a short encoding of the syllepsis, a 5-dimensional homotopy that plays an important role in the homotopy groups of spheres.