A Type Theory for Strictly Associative Infinity Categories

TL;DR

This paper introduces Catt$_{sa}$, a new type theory for strictly associative infinity categories, extending Catt with a definitional equality and an insertion operation, enabling decidable equality and improved structural understanding.

Contribution

It presents a novel type theory for strictly associative infinity categories with a decidable equality, based on an insertion operation and geometric interpretation.

Findings

The reduction relation is confluent and terminating.

Decidable typechecking is achieved.

Insertion operation has a clear geometric and combinatorial interpretation.

Abstract

Many definitions of weak and strict $\infty$-categories have been proposed. In this paper we present a definition for $\infty$-categories with strict associators, but which is otherwise fully weak. Our approach is based on the existing type theory Catt, whose models are known to correspond to weak $\infty$-categories. We add a definitional equality relation to this theory which identifies terms with the same associativity structure, yielding a new type theory Catt$_{sa}$, for strictly associative $\infty$-categories. We also provide a reduction relation which generates definitional equality, and show it is confluent and terminating, giving an algorithm for deciding equality of terms, and making typechecking decidable. Our key contribution, on which our reduction is based, is an operation on terms which we call insertion. This has a direct geometrical interpretation, allowing a subterm to be inserted into the head of the term, flatting its syntactic structure. We describe this operation combinatorially in terms of pasting diagrams, and also show can be characterized as a pushout of contexts. This allows reasoning about insertion using just its universal property.