Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A synthetic construction of universal cocartesian fibrations

Christian Sattler, David Wärn

Abstract

We give a model-independent construction of directed univalent cocartesian fibrations of $(\infty,1)$-categories, and prove a straightening equivalence against such fibrations. The key step is showing that cocartesian fibrations descend along localisations, which we accomplish by analysing mapping spaces of localisations. Along the way we introduce a directed version of the join construction, giving a sequential colimit description of the full image of any functor.

A synthetic construction of universal cocartesian fibrations

Abstract

We give a model-independent construction of directed univalent cocartesian fibrations of -categories, and prove a straightening equivalence against such fibrations. The key step is showing that cocartesian fibrations descend along localisations, which we accomplish by analysing mapping spaces of localisations. Along the way we introduce a directed version of the join construction, giving a sequential colimit description of the full image of any functor.

Paper Structure

This paper contains 28 sections, 12 theorems, 4 equations.

Table of Contents

  1. Introduction
  2. Overview
  3. Preliminaries
  4. Comma and slice categories
  5. The fundamental theorem of category theory
  6. Full and wide subcategories
  7. Adjunctions
  8. Spaces, groupoids, and extensivity
  9. Left and right fibrations
  10. Cofinal functors
  11. Left Kan extension
  12. The Yoneda lemma
  13. Descent for left fibrations
  14. Limits and colimits in functor categories
  15. Mapping spaces of sequential colimits
  16. ...and 13 more sections

Key Result

corollary 1

Consider a cartesian square of categories \begin{tikzcd} D \ar[r] \ar[d] & C \ar[d] \\ B \ar[r] & A \end{tikzcd}where $A$ is a groupoid. Then the square remains cartesian after localisation.

Theorems & Definitions (23)

  • corollary 1
  • proof
  • lemma 1
  • proof
  • lemma 2
  • proof
  • lemma 3
  • proof
  • lemma 4: label=s-ortho
  • proof
  • ...and 13 more