Describing free ω-categories

The notion of pasting diagram is central in the study of strict ω -categories: it encodes a collection of morphisms for which the composition is defined unambiguously. As such, we expect that a pasting diagram itself describes an ω-category which is freely generated by the cells constituting it. In practice, it seems very difficult to characterize this notion in full generality and various definitions have been proposed with the aim of being reasonably easy to compute with, and including common examples (e.g. cubes or orientals). One of the most tractable such structure is parity complexes, which uses sets of cells in order to represent the boundaries of a cell. In this work, we first show that parity complexes do not satisfy the aforementioned freeness property by providing a mechanized proof in Agda. Then, we propose a new formalism that satisfies the freeness property and which can be seen as a corrected version of parity complexes.