We introduce and study a purely syntactic notion of lax cones and $(\infty,\infty)$-limits on finite computads in \texttt{CaTT}, a type theory for $(\infty,\infty)$-categories due to Finster and Mimram. Conveniently, finite computads are precisely the contexts in \texttt{CaTT}. We define a cone over a context to be a context, which is obtained by induction over the list of variables of the underlying context. In the case where the underlying context is globular we give an explicit description of the cone and conjecture that an analogous description continues to hold also for general contexts. We use the cone to control the types of the term constructors for the universal cone. The implementation of the universal property follows a similar line of ideas. Starting with a cone as a context, a set of context extension rules produce a context with the shape of a transfor between cones, i.e.~a higher morphism between cones. As in the case of cones, we use this context as a template to control the types of the term constructor required for universal property.

翻译：我们在\texttt{CaTT}（一种由Finster与Mimram提出的用于$(\infty,\infty)$-范畴的类型理论）中，针对有限计算图引入并研究了一种纯句法意义上的松弛锥与$(\infty,\infty)$-极限概念。便利之处在于，有限计算图恰好对应\texttt{CaTT}中的语境。我们通过对其底层语境的变量列表进行归纳，将锥定义为一个语境。当底层语境为球状时，我们给出了锥的显式描述，并推测类似描述对一般语境同样成立。我们利用该锥来控制泛锥的项构造器的类型。泛性质的实现遵循相似的思路：从一个作为语境的锥出发，通过一组语境扩展规则生成一个具有锥间变换（即锥间高阶态射）形状的语境。与锥的情形类似，我们利用该语境作为模板，以控制实现泛性质所需的项构造器的类型。