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.

翻译：我们给出关于具有内和的（内）$(\infty,1)$-范畴的双纤维化的结构结果。这包括Moens定理的高阶版本，该定理将lex基上具有广泛（即稳定且不交）内和的笛卡尔双纤维化刻画为lex函子的Artin粘合。我们还处理了Streicher给出的Moens定理的推广版本，该版本不需要Beck–Chevalley条件。此外，我们证明在此设定中，Moens纤维化也可通过Zawadowski给出的条件来刻画。我们的论述整体遵循Streicher对Bénabou式纤维化范畴理论的表述，将结果推广到内、高阶范畴情形，并以合成设定表述。具体而言，我们在单纯同伦类型论中工作，该理论由Riehl和Shulman引入，作为一种逻辑系统来推理内$(\infty,1)$-范畴，这些范畴被解释为任意Grothendieck–Rezk–Lurie $(\infty,1)$-意象中的Rezk对象。