Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Limits and colimits of synthetic $\infty$-categories

César Bardomiano Martínez

TL;DR

This work develops a comprehensive synthetic theory of limits and colimits for $(\infty,1)$-categories within simplicial Homotopy Type Theory (sHoTT). By introducing extension types, Segal types, and covariant families, it provides a robust framework to define cones, cocones, and universal (co)limits inside a type-theoretic setting compatible with Univalence. A key contribution is the demonstration that, under suitable univalence assumptions and the presence of a universe of spaces, the limit of a diagram of spaces can be computed as a dependent product, mirroring classical formulas. The paper also establishes preservation results for adjoints, proves uniqueness up to isomorphism in Rezk types, and validates the synthetic theory against the bisimplicial-sets semantics, tying the internal synthetic definitions to the standard external models of $\infty$-categories. Collectively, these results advance a cohesive, computer-verified foundation for limits and colimits in synthetic $\infty$-categories and their semantic interpretation in bisimplicial sets.

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.

Limits and colimits of synthetic $\infty$-categories

TL;DR

This work develops a comprehensive synthetic theory of limits and colimits for -categories within simplicial Homotopy Type Theory (sHoTT). By introducing extension types, Segal types, and covariant families, it provides a robust framework to define cones, cocones, and universal (co)limits inside a type-theoretic setting compatible with Univalence. A key contribution is the demonstration that, under suitable univalence assumptions and the presence of a universe of spaces, the limit of a diagram of spaces can be computed as a dependent product, mirroring classical formulas. The paper also establishes preservation results for adjoints, proves uniqueness up to isomorphism in Rezk types, and validates the synthetic theory against the bisimplicial-sets semantics, tying the internal synthetic definitions to the standard external models of -categories. Collectively, these results advance a cohesive, computer-verified foundation for limits and colimits in synthetic -categories and their semantic interpretation in bisimplicial sets.

Abstract

We develop the theory of limits and colimits in -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.
Paper Structure (18 sections, 34 theorems, 96 equations)

This paper contains 18 sections, 34 theorems, 96 equations.

Table of Contents

  1. Introduction
  2. Limits and colimits
  3. Outline
  4. Computer verified proofs.
  5. Extension types, Segal types and covariant families
  6. Extension types
  7. Relative function extentionality axiom
  8. Segal types
  9. Discrete types
  10. Rezk types
  11. Covariant families
  12. Yoneda lemma
  13. Limits and colimits
  14. Preservation of limits and colimits
  15. (Co)Limits in Rezk types
  16. ...and 3 more sections

Key Result

Theorem 2.2

If $t:I\: | \:\phi\vdash\psi$, $X:\{t:I\: | \:\psi\}\rightarrow \mathcal{U}$ and $Y:\prod\limits_{t:I\: | \:\psi}(X\rightarrow U)$, while $a:\prod_{t:I\: | \:\psi}X(t)$ and $b:\prod_{t:I\: | \:\phi}Y(t,x(t))$, then

Theorems & Definitions (80)

  • Remark 2.1
  • Theorem 2.2
  • proof
  • Theorem 2.3
  • Definition 2.6
  • Definition 2.7
  • Definition 2.8
  • Theorem 2.9
  • Proposition 2.10
  • proof
  • ...and 70 more