Two-sided Cartesian fibrations of synthetic \((\infty, 1)\)-categories (Q6612003)

One important milestone in category theory is the development of the theory of fibrations. Starting with ideas of figures such as Grothendieck, various notions of fibrations have been developed to capture the data of certain functors. Important examples include \textit{discrete fibrations} and \textit{Grothendieck fibrations}, capturing functors valued in the category of sets or the category of categories. Despite their utility, Grothendieck fibrations do not capture all relevant examples, motivating category theorists, such as Street, to introduce a further variant, namely \emph{\(2\)-sided (discrete) fibrations}, which corresponds to profunctors (also known as distributors or modules) [\textit{R. Street}, Lect. Notes Math. 420, 104--133 (1974; Zbl 0327.18006)]. A prime example of a \(2\)-sided discrete fibration is given by the source target projection \(\mathcal{C}^{[1]} \to \mathcal{C} \times \mathcal{C}\), which corresponds to the Hom profunctor \(\mathrm{Hom}\colon \mathcal{C}^{op} \times \mathcal{C} \to \mathrm{Set}\), arguably the most prominent example of a profunctor. As this example might suggest, \(2\)-sided fibrations have played a prominent role in the study of various generalizations of the Yoneda lemma.\N\NCategory theory has been generalized to various notions of \textit{higher categories}, and particularly \textit{\((\infty,1)\)-category theory}, which is a generalization of category theory where various identities and conditions, such as a choice of composition or associativity, only holds up to a coherent choice of further identities (i.e. homotopies). \((\infty,1)\)-category theory has become the standard way to study parts of mathematics where such higher identities naturally occur, such as algebraic topology, derived geometry, homological algebra, and topological field theory. As a result, in recent decades there has been significant effort to properly develop \((\infty,1)\)-categorical analogues to different categorical concepts. This, in particular, includes \((\infty,1)\)-categorical versions of categorical fibrations, such as \textit{Cartesian fibrations} and \textit{\(2\)-sided \((\infty,1)\)-fibrations}, commencing with the work of \textit{A. Joyal} [J. Pure Appl. Algebra 175, No. 1--3, 207--222 (2002; Zbl 1015.18008)] and \textit{J. Lurie} [Higher topos theory. Princeton, NJ: Princeton University Press (2009; Zbl 1175.18001)].\N\NWhile \((\infty,1)\)-categorical techniques have found many powerful applications and helped solve major theorems, the inherent complexity also presents new challenges: in particular it increases the likelihood of subtle mistakes and makes it challenging to teach. This, among other reasons, motivated Riehl and Shulman to develop \((\infty,1)\)-category theory in type theoretic foundations [\textit{E. Riehl} and \textit{M. Shulman}, High. Struct. 1, No. 1, 147--224 (2017; Zbl 1437.18016)]. Concretely, building on the work of Voevodsky and others on \textit{univalent foundations} and \textit{homotopy type theory} [\textit{The Univalent Foundations Program}, Homotopy type theory. Univalent foundations of mathematics. Princeton, NJ: Institute for Advanced Study; Raleigh, NC: Lulu Press (2013; Zbl 1298.03002)], Riehl and Shulman developed an extension called \textit{simplicial homotopy type theory (sHoTT)}, which enables proving \((\infty,1)\)-categorical results in a type theoretical setting. Moreover, sHoTT has motivated the development of the proof assistant \textit{Rzk}, which has, for the first time, enabled the formal verification of \((\infty,1)\)-categorical results. A prominent example is the recent formalization of the \((\infty,1)\)-categorical Yoneda lemma via Rzk [\textit{N. Kudasov} et al., ``Formalizing the \(\infty\)-Categorical Yoneda Lemma'', Preprint, arXiv:2309.08340].\N\NWhile the work of of Riehl and Shulman is an important first step, many aspects of \((\infty,1)\)-category theory remain to be developed in this context. As a first step towards remedying this situation, Buchholtz and Weinberger developed a theory of Cartesian fibrations in the setting of sHoTT [\textit{U. Buchholtz} and \textit{J. Weinberger}, High. Struct. 7, No. 1, 74--165 (2023; Zbl 1535.18039)]. As a next step, in the current paper the second author continues this line of work and develops the \((\infty,1)\)-categorical \(2\)-sided fibrations in the setting of sHoTT. In particular, the author provides several ways to characterize \(2\)-sided fibrations (\textit{Theorem 4.1}), establishes various closure properties (\textit{Theorem 4.1}), and proves a Yoneda Lemma (\textit{Theorems 6.1 and 6.2}).\N\NIn order to prove these (and many other) results, the author employs the theory of \textit{\(\infty\)-cosmoi}, developed by \textit{E. Riehl} and \textit{D. Verity} [Elements of \(\infty\)-category theory. Cambridge: Cambridge University Press (2022; Zbl 1492.18001)]. \(\infty\)-cosmos theory utilizes \(2\)-categorical methods to develop \((\infty,1)\)-category theory, in contrast to older approaches, such as Joyal or Lurie, which primarily used simplicial methods. This abstract \(2\)-categorical approach makes it particularly suitable for a formal approach in a context of simplicial type theory, resulting in elegant proofs in a type theoretical setting.