In many works on (Higher) Category Theory, in addition to the usual many-sorted notions of $n$-categories and of $\omega$-categories, the single-sorted versions of them are also commonly used.

The aim of this project is to provide a formalization of the latter notions and the proof of their equivalence in Lean 4.