Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Internal languages of locally cartesian closed $(\infty,1)$-categories

El Mehdi Cherradi

Abstract

We establish a DK-equivalence between the relative category of $π$-tribes and the relative category of locally cartesian closed quasicategories. From this follows one of the internal languages conjecture: Martin-Löf type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed $(\infty,1)$-categories.

Internal languages of locally cartesian closed $(\infty,1)$-categories

Abstract

We establish a DK-equivalence between the relative category of -tribes and the relative category of locally cartesian closed quasicategories. From this follows one of the internal languages conjecture: Martin-Löf type theory with dependent sums, intensional identity types, and dependent products satisfying functional extensionality is the internal language of locally cartesian closed -categories.

Paper Structure

This paper contains 8 sections, 29 theorems, 27 equations.

Table of Contents

  1. The canonical path tribe
  2. Some fibration categories of tribes
  3. The rigidification tool
  4. Proof of the conjecture
  5. The DK-equivalences between categories of tribes and their semi-cubical counterparts
  6. The DK-equivalence $\mathbf{scTrb_\pi^p} \to \mathbf{scTrb_\pi}$
  7. Preservation of the internal product: from up-to-equivalence to up-to-isomorphism
  8. Final step in the proof of the conjecture

Key Result

Theorem 1.1

Given fibration categories $\mathcal{F}_0$ and $\mathcal{F}_1$, as well as an exact functor $H : \mathcal{F}_0 \to \mathcal{F}_1$, the following are equivalent:

Theorems & Definitions (76)

  • Conjecture 1
  • Definition 1.1
  • Theorem 1.1: Cisinski
  • Definition 1.2
  • Definition 1.3
  • Remark 1.1
  • Lemma 1.2
  • proof
  • Proposition 1.3
  • proof
  • ...and 66 more