A Syntax for Strictly Associative and Unital โ-Categories
A Syntax for Strictly Associative and Unital โ-Categories
We present the first definition of strictly associative and unital โ-category.Our proposal takes the form of a type theory whose terms describe the operations of such structures, and whose definitional equality relation enforces desired strictness conditions.The key technical device is a new computation rule in the definitional equality of the โฆ