Limits and colimits of synthetic $\infty$-categories

TL;DR

This paper develops the theory of limits and colimits in $ abla$-categories within the synthetic framework of simplicial Homotopy Type Theory, showing that limits of spaces can be computed as dependent products.

Contribution

It extends the synthetic approach to $ abla$-categories by formalizing limits and colimits, and demonstrates how to compute limits of spaces as dependent products in this setting.

Findings

Limits and colimits are formalized in synthetic $ abla$-categories.

Limits of spaces can be computed as dependent products.

The framework integrates $ abla$-categories with Homotopy Type Theory.

Abstract

We develop the theory of limits and colimits in $\infty$-categories within the synthetic framework of simplicial Homotopy Type Theory developed by Riehl and Shulman. We also show that in this setting, the limit of a family of spaces can be computed as a dependent product.