Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories

TL;DR

This paper develops a theory of two-sided cartesian fibrations within synthetic $( abla,1)$-category theory, providing characterizations, a Yoneda lemma, and closure properties, all formulated internally and invariant under homotopy.

Contribution

It introduces a comprehensive synthetic framework for two-sided cartesian fibrations, including new characterizations, a Yoneda lemma, and modular fibered fibration notions, extending existing $ abla$-cosmos theory.

Findings

Characterizations of two-sidedness condition

A two-sided Yoneda Lemma proved

Closure properties of fibrations established

Abstract

Within the framework of Riehl-Shulman's synthetic $(\infty,1)$-category theory, we present a theory of two-sided cartesian fibrations. Central results are several characterizations of the two-sidedness condition \`{a} la Chevalley, Gray, Street, and Riehl-Verity, a two-sided Yoneda Lemma, as well as the proof of several closure properties. Along the way, we also define and investigate a notion of fibered or sliced fibration which is used later to develop the two-sided case in a modular fashion. We also briefly discuss discrete two-sided cartesian fibrations in this setting, corresponding to $(\infty,1)$-distributors. The systematics of our definitions and results closely follows Riehl-Verity's $\infty$-cosmos theory, but formulated internally to Riehl-Shulman's simplicial extension of homotopy type theory. All the constructions and proofs in this framework are by design invariant under homotopy equivalence. Semantically, the synthetic $(\infty,1)$-categories correspond to internal $(\infty,1)$-categories implemented as Rezk objects in an arbitrary given $(\infty,1)$-topos.