A Type Theory for Strictly Unital $\infty$-Categories

TL;DR

This paper develops a type-theoretic framework for strictly unital atb3gories, providing a decision procedure for equality and showing strict unitality as a property, not extra structure.

Contribution

It introduces a new algebraic theory with definitional equality for strictly unital ategories, extending weak ategory theory with strict units and establishing meta-theoretic properties.

Findings

Decidable equality in strictly unital ategories

Confluence and termination of the reduction relation

Strict unitality as a property, not structure

Abstract

We use type-theoretic techniques to present an algebraic theory of $\infty$-categories with strict units. Starting with a known type-theoretic presentation of fully weak $\infty$-categories, in which terms denote valid operations, we extend the theory with a non-trivial definitional equality. This forces some operations to coincide strictly in any model, yielding the strict unit behaviour. We make a detailed investigation of the meta-theoretic properties of this theory. We give a reduction relation that generates definitional equality, and prove that it is confluent and terminating, thus yielding the first decision procedure for equality in a strictly-unital setting. Moreover, we show that our definitional equality relation identifies all terms in a disc context, providing a point comparison with a previously proposed definition of strictly unital $\infty$-category. We also prove a conservativity result, showing that every operation of the strictly unital theory indeed arises from a valid operation in the fully weak theory. From this, we infer that strict unitality is a property of an $\infty$-category rather than additional structure.