There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.

翻译：近年来，利用带有单值性和高阶归纳类型依赖类型论的扩展，合成数学领域取得了若干进展：单纯同伦类型论、合成代数几何以及合成Stone对偶。我们在此构建了一个在构造性元理论中类型论的高阶层模型基础，并特别地建立了这些形式系统的构造性模型。