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

TL;DR

This paper extends classical results on bifibrations and internal sums to the setting of higher category theory within simplicial homotopy type theory, providing new characterizations and generalizations of Moens' Theorem.

Contribution

It generalizes Moens' Theorem and related results to internal, higher-categorical contexts using synthetic methods in homotopy type theory.

Findings

Higher version of Moens' Theorem established

Characterization of cartesian bifibrations with internal sums

Generalization of Moens' Theorem without Beck--Chevalley condition

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 \`{a} la B\'{e}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.