A Syntax for Strictly Associative and Unital $\infty$-Categories

Eric Finster, Alex Rice, Jamie Vicary

We present the first definition of strictly associative and unital $\infty$-category. Our proposal takes the form of a type theory whose terms describe the operations of such struc…