标题： 一种类型论定义的松散$(\infty,\infty)$-极限 显示英文标题

标题： A Type-Theoretic Definition of Lax $(\infty,\infty)$-Limits

摘要： 我们引入并研究了在有限计算范畴\texttt{CaTT}中的纯句法概念的松锥和$(\infty,\infty)$-极限，这是一种由 Finster 和 Mimram 提出的$(\infty,\infty)$-范畴类型理论。 方便的是，有限计算范畴正是\texttt{CaTT}中的上下文。 我们定义一个上下文上的锥为一个上下文，该上下文通过对其基础上下文的变量列表进行归纳得到。 在基础上下文为球状的情况下，我们给出了锥的显式描述，并猜想类似的描述也适用于一般上下文。 我们使用锥来控制通用锥的项构造器的类型。 通用性质的实现遵循类似的思路。 从一个作为上下文的锥开始，一组上下文扩展规则生成一个具有锥之间变换形状的上下文，即锥之间的高阶态射。 如同锥的情况一样，我们使用此上下文作为模板来控制通用性质所需的项构造器的类型。 显示英文摘要

摘要： 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.