title: A Synthetic Perspective on (∞,1)-Category Theory: Fibrational and Semantic Aspects
Creators: name: Weinberger, Jonathan
Publisher: name: UNSPECIFIED
Year: 2022

description: Reasoning about weak higher categorical structures constitutes a challenging task, even to the experts. One principal reason is that the language of set theory is not invariant under the weaker notions of equivalence at play, such as homotopy equivalence. From this point of view, it is natural to ask for a different foundational setting which more natively supports these notions. A possible approach along these lines has been given by Riehl–Shulman in 2017 where they have developed a theory of synthetic (∞,1)-categories. For this purpose they have introduced an extension of homotopy type theory/univalent foundations (HoTT/UF). Pioneered by Voevodsky, this logical system is designed to develop homotopy theory in a synthetic way, meaning that its basic entities can essentially be understood as topological spaces, or more precisely homotopy types. As per Voevodsky's Univalence Axiom, homotopy equivalence between types coincides with logical equivalence. As a consequence, a lot of the conceptual ideas from classical homotopy theory can be imported to reason more intrinsically about homotopical structures. In fact, in 2019 Shulman achieved to prove the long-standing conjecture that any higher topos (in the sense of Grothendieck–Rezk–Lurie) gives rise to a model of homotopy type theory. This gives a precise technical sense in which HoTT can be regarded as a kind of internal language of (∞,1)-toposes ℰ. By analogy, Riehl–Shulman's extension, called simplicial homotopy type theory (sHoTT), can be interpreted in diagram (∞,1)-toposes of the form ℰ^(Δ^op). Syntactic additions make it possible to reason type-theoretically about internal (∞,1)-categories implemented as (complete) Segal objects. Based on Riehl–Shulman's work about synthetic (∞,1)-categories and discrete covariant fibrations, we present a theory of co-/cartesian fibrations including sliced and two-sided versions. The study is informed by Riehl–Verity's work on model-independent ∞-category theory, and transfers results of their ∞-cosmoses to the type-theoretic setting. We prove characterization theorems for cocartesian fibrations and their generalizations, given as existence conditions of certain adjoint functors (Chevalley criteria). Extending the author's previous joint work with Buchholtz, we prove several closure properties of two-sided cartesian fibrations as well as a two-sided Yoneda Lemma. Furthermore, we discuss so-called Beck–Chevalley (bi)fibrations and prove a synthetic (∞,1)-categorical version of Moens' Theorem, after Streicher. Finally, we show how to interpret Riehl–Shulman's strict extension types in the intended higher topos model, in such a way that makes them strictly stable under substitution. This uses a method, originally due to Voevodsky, which has previously been employed in the works of e.g. Kapulkin, Lumsdaine, Warren, Awodey, Streicher, and Shulman. Our work takes up on suggestions in the original article by Riehl–Shulman to further develop synthetic (∞,1)-category theory in simplicial HoTT, including in particular the study of cocartesian fibrations. Together with a collection of analytic results, notably due to Riehl–Verity and Rasekh, it follows that our type-theoretic account constitutes a synthetic theory of fibrations of internal (∞,1)-categories.