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

A type-theoretic $\omega$-category is a model of the type theory defined in the paper, while a Grothendieck–Maltsiniotis $\omega$-category is a functor $C:\mathcal{T}^{\operatorname{op}}\to\operatorname{Set}$ whose opposite preserves globular sums, where $\mathcal{T}$ is the canonical coherator. Correspondence conjecture. Type-theoretic $\omega$-categories correspond precisely to Grothendieck–Maltsiniotis $\omega$-categories. The claim is the semantic form of the proposed comparison between the type-theoretic models and Maltsiniotis's definition; the source explicitly says that a detailed comparison remains future work.