The theory of $(\infty,1)$-categories can be developed synthetically in an augmentation of homotopy type theory introduced by Riehl--Shulman. Central to their development is an additional type forming operation called extensions. The original article sketches the semantics of this formal system, explaining how the simplicial homotopy theory can be used to reason about $(\infty,1)$-categories presented using the Segal space model. However, they leave it open to demonstrate the strict stability of extension types. We prove this using the splitting method of Voevodsky, later generalized by Lumsdaine--Warren to local universes. The practical upshot is that this system has semantics in simplicial objects of an $\infty$-topos, and thus can be used to prove theorems about internal $\infty$-categories in the sense of Martini--Wolf.

翻译：$(\infty,1)$-范畴理论可以在Riehl–Shulman引入的同伦类型论增强中综合地发展。其核心是一种称为扩展的额外类型形成操作。原始论文概述了这一形式系统的语义，解释了如何利用单纯同伦理论来推理以Segal空间模型呈现的$(\infty,1)$-范畴。然而，他们未证明扩展类型的严格稳定性。我们使用Voevodsky的分裂方法（后由Lumsdaine–Warren推广至局部宇宙）证明了这一点。实际意义在于，该形式系统在$\infty$-拓扑斯的单纯对象中具有语义，从而可用于证明Martini–Wolf意义上的内部$\infty$-范畴定理。