Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Generalized Chevalley criteria in simplicial homotopy type theory

Jonathan Weinberger

Abstract

We provide a generalized treatment of (co)cartesian arrows, fibrations, and functors. Compared to the classical conditions, the endpoint inclusions get replaced by arbitrary shape inclusions. Our framework is Riehl--Shulman's simplicial homotopy type theory which supports the development of synthetic internal $(\infty,1)$-category theory.

Generalized Chevalley criteria in simplicial homotopy type theory

Abstract

We provide a generalized treatment of (co)cartesian arrows, fibrations, and functors. Compared to the classical conditions, the endpoint inclusions get replaced by arbitrary shape inclusions. Our framework is Riehl--Shulman's simplicial homotopy type theory which supports the development of synthetic internal -category theory.
Paper Structure (20 sections, 9 theorems, 46 equations, 1 figure)

This paper contains 20 sections, 9 theorems, 46 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Martin-Löf type theory
  4. Univalence axiom
  5. The homotopy theory of types
  6. Simplicial homotopy type theory
  7. Simplicial shapes
  8. Extension types
  9. Synthetic (∞,1)-category theory
  10. Synthetic fibered (∞,1)-category theory
  11. Relative adjunctions
  12. LARI cells, fibrations, and functors
  13. LARI cells
  14. LARI fibrations
  15. LARI functors
  16. ...and 5 more sections

Key Result

Theorem 3.4

Let $A,B,C$ be Rezk types and $(g: C \to A \leftarrow B: f)$ a cospan. Then the following types are equivalent propositions:

Figures (1)

  • Figure 1: Universal property of $j$-LARI cells (schematic illustration)

Theorems & Definitions (28)

  • Definition 3.1: Transposing relative adjunction
  • Definition 3.2: Relative adjunction via units
  • Definition 3.3: Absolute left lifting diagram
  • Theorem 3.4: Characterizations of relative left adjunctions, cf. RV21, RS17, BW21
  • proof
  • Corollary 3.5
  • Definition 3.6: Relative LARI adjunction
  • Definition 4.1: $j$-LARI cell
  • Definition 4.2: Pushout product
  • Definition 4.3: $j$-LARI family
  • ...and 18 more