The equivalence between type-theoretic and Grothendieck–Maltsiniotis c9-categories

Let $\mathcal{S}_{\mathrm{cat}}$ be the category of type-theoretic models described in the paper, and let $\mathcal{T}$ be the canonical coherator for Grothendieck–Maltsiniotis $\omega$-categories. An $\omega$-category in the Grothendieck–Maltsiniotis sense is a functor $C:\mathcal{T}^{\operatorname{op}}\to\operatorname{Set}$ such that $C^{\operatorname{op}}$ preserves globular sums. Equivalence conjecture. The category $\mathcal{S}_{\mathrm{cat}}$ is equivalent to $\mathcal{T}$. This would identify the type-theoretic definition with the canonical coherator underlying the Grothendieck–Maltsiniotis definition; the paper leaves the detailed comparison for future work.