A type-theoretic approach to semistrict higher categories

TL;DR

This paper introduces a type-theoretic framework for semistrict higher categories by extending a base theory with definitional equality, enabling formal reasoning, decidable typechecking, and efficient implementation of semistrict models.

Contribution

It develops a general framework for adding definitional equality to a type theory modeling weak ∞-categories, leading to new semistrict theories with decidable typechecking and practical implementation.

Findings

Framework formalized in Agda with metatheory proofs

Decidable typechecking for the new theories

Efficient implementation using normalisation by evaluation

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.