A type-theoretic approach to semistrict higher categories

Weak ∞-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 ∞-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 Catt, a type theory whose models correspond to globular weak ∞-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 Catt extended with an equality relation generated by an arbitrary set of equality rules R, which we name CattR. We study this framework in detail, formalising much of its metatheory in the proof assistant Agda, and studying how certain operations of Catt behave in the presence of definitional equality.

The main contribution of this thesis is to introduce two type theories, Cattsu and Cattsua, which are instances of this general framework. Cattsu, short for Catt with strict units, is a variant of Catt where the unitor isomorphisms trivialise to identities. It is primarily generated by a reduction we call pruning, which removes identities from composites, simplifying their structure. Cattsua, which stands for Catt with strict units and associators, trivialises both the associativity and unitality operations of Catt, and is generated by a generalisation of pruning called insertion. Insertion merges multiple composites into a single operation, flattening the structure of terms in the theory.

Further, we provide reduction systems that generate the equality of both Cattsu and Cattsua respectively, and prove that these reductions systems are strongly terminating and confluent. 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.