Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with $Π$-, $Σ$-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.

翻译：近年来，内涵类型论的模型已在代数弱分解系统（AWFSs）中构建。AWFSs 催生了理解范畴，这些范畴包含类型之间的非平凡态射；这些态射在 Martin-Löf 类型论于理解范畴中的标准解释中未被使用。我们发展了一种类型论，将类型间的态射内化，从而将这一语义特征反映回句法。我们的类型论包含 $Π$ 类型、$Σ$ 类型和恒等类型。我们讨论了如何将其视为 Martin-Löf 类型论在强制子类型化方面的扩展，如 Coraglia 和 Emmenegger 所概述。此外，我们定义了可解释该类型论的语义结构，并证明了其可靠性结果。最后，我们展示了该语义结构的多个实例，从而提供了丰富的解释。