# Strict Omega Categories

January 14, 2023

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

### 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.