Data structures for quasistrict higher categories

Understand

We present new data structures for quasistrict higher categories, in which associativity and unit laws hold strictly.

• Our approach has low axiomatic complexity compared to traditional algebraic definitions of higher categories, and we use it to give a practical definition of quasistrict 4-category.
• It is also amenable to computer implementation, and we exploit this to give a new machine-verified algebraic proof that every adjunction of 1-cells in a quasistrict 4-category can be promoted to a coherent adjunction satisfying the butterfly equations.