Strict Omega Categories

January 14, 2023

Abstract

This theory formalises a definition of strict $\omega$-categories and the strict $\omega$-category of pasting diagrams. It is the first step towards a formalisation of weak infinity categories à la Batanin–Leinster.