Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Internal sums for synthetic fibered $(\infty,1)$-categories

Jonathan Weinberger

TL;DR

This work develops a synthetic, higher-categorical perspective on internal sums for fibrations of $(\infty,1)$-categories within RS17-style simplicial HoTT, culminating in a higher Moens correspondence. The authors define and analyze cocartesian, cartesian, lex, and bicartesian fibrations, and prove that lextensive (stable and disjoint) internal sums are precisely captured by Artin gluings of lex functors, a higher analogue of Moens' theorem. They also extend the framework to generalized Moens fibrations without the Beck--Chevalley condition and connect these to Zawadowski's definitions, consolidating several classical results in a synthetic higher setting. The work thereby advances internal higher topos theory and fibered category theory in a model-theoretic, topos-theoretic, and logical program, with potential applications to geometric morphisms and internal higher categorical logic within synthetic HoTT.

Abstract

We give structural results about bifibrations of (internal) $(\infty,1)$-categories with internal sums. This includes a higher version of Moens' Theorem, characterizing cartesian bifibrations with extensive aka stable and disjoint internal sums over lex bases as Artin gluings of lex functors. We also treat a generalized version of Moens' Theorem due to Streicher which does not require the Beck--Chevalley condition. Furthermore, we show that also in this setting the Moens fibrations can be characterized via a condition due to Zawadowski. Our account overall follows Streicher's presentation of fibered category theory à la Bénabou, generalizing the results to the internal, higher-categorical case, formulated in a synthetic setting. Namely, we work inside simplicial homotopy type theory, which has been introduced by Riehl and Shulman as a logical system to reason about internal $(\infty,1)$-categories, interpreted as Rezk objects in any given Grothendieck--Rezk--Lurie $(\infty,1)$-topos.

Internal sums for synthetic fibered $(\infty,1)$-categories

TL;DR

This work develops a synthetic, higher-categorical perspective on internal sums for fibrations of -categories within RS17-style simplicial HoTT, culminating in a higher Moens correspondence. The authors define and analyze cocartesian, cartesian, lex, and bicartesian fibrations, and prove that lextensive (stable and disjoint) internal sums are precisely captured by Artin gluings of lex functors, a higher analogue of Moens' theorem. They also extend the framework to generalized Moens fibrations without the Beck--Chevalley condition and connect these to Zawadowski's definitions, consolidating several classical results in a synthetic higher setting. The work thereby advances internal higher topos theory and fibered category theory in a model-theoretic, topos-theoretic, and logical program, with potential applications to geometric morphisms and internal higher categorical logic within synthetic HoTT.

Abstract

We give structural results about bifibrations of (internal) -categories with internal sums. This includes a higher version of Moens' Theorem, characterizing cartesian bifibrations with extensive aka stable and disjoint internal sums over lex bases as Artin gluings of lex functors. We also treat a generalized version of Moens' Theorem due to Streicher which does not require the Beck--Chevalley condition. Furthermore, we show that also in this setting the Moens fibrations can be characterized via a condition due to Zawadowski. Our account overall follows Streicher's presentation of fibered category theory à la Bénabou, generalizing the results to the internal, higher-categorical case, formulated in a synthetic setting. Namely, we work inside simplicial homotopy type theory, which has been introduced by Riehl and Shulman as a logical system to reason about internal -categories, interpreted as Rezk objects in any given Grothendieck--Rezk--Lurie -topos.
Paper Structure (36 sections, 46 theorems, 74 equations, 8 figures)

This paper contains 36 sections, 46 theorems, 74 equations, 8 figures.

Table of Contents

  1. Introduction
  2. Overview
  3. Beck--Chevalley families
  4. Moens families
  5. Further context and perspective on the work
  6. Geometric families of synthetic (∞,1)-categories
  7. Jibladze's Theorem for higher toposes
  8. Moens' Theorem in $\infty$-cosmoses
  9. Structure, contributions, and related work
  10. Further related work
  11. Synthetic fibered (∞,1)-category theory
  12. Synthetic (∞,1)-categories
  13. Cocartesian families
  14. Cocartesian families
  15. Examples of cocartesian families
  16. ...and 21 more sections

Key Result

Proposition 2.2

Let $P: B \to \mathcal{U}$ be a family.

Figures (8)

  • Figure 1: Logical dependency of notions of fibration
  • Figure 2: Construction of fiberwise terminal objects
  • Figure 3: Cartesian lifts in the family fibration
  • Figure 4: Cocartesian and cartesian lifts in the gluing fibration
  • Figure 5: Action on arrows of $\tau$ (over $u:a \to b$ in $B$)
  • ...and 3 more figures

Theorems & Definitions (99)

  • Definition 2.1: (Iso)inner families, BW21
  • Proposition 2.2: BW21
  • Definition 2.3: Cocartesian arrow, BW21, cf. RV21
  • Definition 2.4: Cocartesian family, BW21, cf. RV21
  • Theorem 2.5: Cocart. families via transport, BW21, cf. RV21
  • Proposition 2.6
  • proof
  • Corollary 2.7: Codomain opfibration
  • Proposition 2.8: Domain opfibration
  • proof
  • ...and 89 more