The recent paper ["A Type Theory for Synthetic $\infty$-Categories"](https://arxiv.org/abs/1705.07442) proposes the syntax as the theory of the strict interval. In principle, any other suitable theory could be used instead. For instance, using Joyal’s theory of disks would yield a type theory in which to study $(\infty,n)$-categories ($\theta$ categories) in Rezk's style. 


Any one know some work or references on a type theory to study higher categories, more specifically, $(\infty,n)$-categories and $(r,n)$-categories ?



Type Theory to Study $(\infty,n)$-Categories and $(r,n)$-Categories
I don't know of anyone who is specifically working on generalizing our paper to the $(\infty,n)$-case. But there have been other attempts to design a type theory for higher categories, such as Finster's [opetopic type theory](https://ncatlab.org/nlab/show/opetopic+type+theory).


