A type-theoretic definition of lax $(\infty,\infty)$-limits

TL;DR

This paper defines and studies a syntactic notion of lax cones and limits in a type theory for $( abla, abla)$-categories, providing a framework for universal cones and higher morphisms in this setting.

Contribution

It introduces a purely syntactic approach to lax $( abla, abla)$-limits within a type theory, extending the understanding of limits in higher category theory.

Findings

Defines cones as contexts obtained by induction over variables.

Provides an explicit description of cones in globular contexts.

Develops a method to control types of universal cone constructors.

Abstract

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.