Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

$(\infty,1)$-Categorical Comprehension Schemes

Raffael Stenzel

Abstract

We define and study notions of comprehension in $(\infty,1)$-category theory. In essence, we do so by implementing Bénabou's foundations of naive category theory in a univalent meta-theory. In particular, we develop natural generalizations of smallness and relative definability in this context, and show for instance that the universal cartesian fibration is small. Furthermore, by building on Johnstone's notion of comprehension schemes for ordinary fibered categories, we characterize and relate numerous higher categorical properties and structures such as left exactness, local cartesian closedness, univalent morphisms and internal $(\infty,1)$-categories in terms of comprehension schemes.

$(\infty,1)$-Categorical Comprehension Schemes

Abstract

We define and study notions of comprehension in -category theory. In essence, we do so by implementing Bénabou's foundations of naive category theory in a univalent meta-theory. In particular, we develop natural generalizations of smallness and relative definability in this context, and show for instance that the universal cartesian fibration is small. Furthermore, by building on Johnstone's notion of comprehension schemes for ordinary fibered categories, we characterize and relate numerous higher categorical properties and structures such as left exactness, local cartesian closedness, univalent morphisms and internal -categories in terms of comprehension schemes.

Paper Structure

This paper contains 8 sections, 48 theorems, 92 equations.

Table of Contents

  1. Introduction
  2. Preliminaries on indexed and fibered $(\infty,1)$-category theory
  3. Diagrammatic $(\infty,1)$-comprehension schemes
  4. Standard diagrammatic comprehension for cartesian fibrations
  5. Externalization of internal $(\infty,1)$-categories
  6. Fibered notions of general comprehension and definability
  7. Univalence and smallness
  8. Model independence

Key Result

Proposition \ref{lemmabenabou}

Let $G\colon I\rightarrow J$ be a map of simplicial sets and $p\colon\mathcal{E}\twoheadrightarrow\mathcal{C}$ be a cartesian fibration. The fibration $p$ has $G$-comprehension if and only if for every vertical diagram $X\in\llbracket I,\mathcal{E}\rrbracket$ the $(\infty,1)$-category $G^{\ast}\down

Theorems & Definitions (151)

  • Definition 1.1
  • Definition 1.2
  • Proposition \ref{lemmabenabou}
  • Theorem \ref{thmsmall=ext}
  • Proposition \ref{proprightadj}
  • Proposition \ref{propintfunctorscomp}
  • Proposition \ref{propunivalentcomprehensioncats}
  • Corollary \ref{chartopssmall}
  • Definition 2.1
  • Definition 2.3
  • ...and 141 more