A type-theoretic approach to semistrict higher categories

Abstract

Weak $\infty$-categories are known to be more expressive than their strict counterparts, but are more difficult to work with, as constructions in such a category involve the manipulation of explicit coherence data. This motivates the search for definitions of semistrict $\infty$-categories, where some, but not all, of the operations have been strictified. We introduce a general framework for adding definitional equality to the type theory $\mathsf{Catt}$, a type theory whose models correspond to globular weak $\infty$-categories, which was introduced by Finster and Mimram. Adding equality to this theory causes the models to exhibit semistrict behaviour, trivialising some operations while leaving others weak. The framework consists of a generalisation of $\mathsf{Catt}$ extended with an equality relation generated by an arbitrary set of equality rules $\mathcal{R}$, which we name $\mathsf{Catt}_{\mathcal{R}}$. We study this framework in detail, formalising much of its metatheory in the proof assistant Agda, and studying how certain operations of $\mathsf{Catt}$ behave in the presence of definitional equality. We use this framework to introduce two type theories, $\mathsf{Catt}_{\mathsf{su}}$ and $\mathsf{Catt}_{\mathsf{sua}}$, which are instances of this general framework. Further, we provide terminating and confluent reduction systems that generate the equality of both systems. We therefore prove that the equality, and hence typechecking, of both theories is decidable. This is used to give an implementation of these type theories, which uses an approach inspired by normalisation by evaluation to efficiently find normal forms for terms. We further introduce a bidirectional typechecking algorithm used by the implementation which allows for terms to be defined in a convenient syntax where many arguments can be left implicit.