A type-theoretic definition of lax $(\infty,\infty)$-limits
Thomas Jan Mikhail
TL;DR
This work defines lax $(\infty,\infty)$-limits within the CaTT framework by treating diagrams as finite computad contexts and building cones as inductively generated contexts. It develops a universal cone and a precise universal property using a hierarchy of context-based constructions, including Gray operations and higher transfors, to model postcomposition, whiskering, and coherence data. The approach yields a type-theoretic, algebraic handle on lax limits in $(\infty,\infty)$-categories and shows how to realize the universal property through a structured, rule-based extension of CaTT, including cut-admissibility. Overall, it provides a foundation for formalizing lax limits in a purely syntactic setting, with explicit rules for cones, transfors, and the universal cone morphism. This has potential implications for formalization and automated reasoning about higher-categorical limits in proof assistants grounded in CaTT_lim.
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.