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.
翻译:在Riehl-Shulman合成$(\infty,1)$-范畴理论框架下,我们提出了两侧笛卡尔纤维化的理论体系。核心成果包括:对Chevalley、Gray、Street及Riehl-Verity所定义的两侧性条件给出多重刻画,建立两侧Yoneda引理,并证明若干封闭性质。在此过程中,我们定义并研究了纤维化或切片纤维化的概念,将其作为后续模块化处理两侧情形的基础工具。我们还简要讨论了该框架中对应于$(\infty,1)$-分布子的离散两侧笛卡尔纤维化。本文定义与结果的系统化表述紧密遵循Riehl-Verity的$\infty$-宇宙理论,但内嵌于Riehl-Shulman的单纯同伦类型论拓展框架之中。该框架中的所有构造与证明天然保持同伦等价不变性。从语义角度而言,合成$(\infty,1)$-范畴对应于任意给定$(\infty,1)$-拓扑斯中作为Rezk对象实现的内部$(\infty,1)$-范畴。