类型论语义的一个通用框架
A General Framework for the Semantics of Type Theory
AI总结：
本文提出类型论的抽象概念，统一Martin-Löf、双层与立方类型论的语义，并证明双初始模型、内部语言及理论范畴与模型2-范畴的双等价等基本结果。
摘要：
我们提出一种类型论的抽象概念，以统一各种类型论的语义，包括Martin-Löf类型论、双层类型论和立方类型论。我们建立了类型论语义中的基本结果：每个类型论都有一个双初始模型；每个类型论的模型都有其内部语言；一个类型论之上的理论范畴双等价于该类型论模型2-范畴的一个满子2-范畴。
英文摘要：
We propose an abstract notion of a type theory to unify the semantics of various type theories including Martin-Löf type theory, two-level type theory and cubical type theory. We establish basic results in the semantics of type theory: every type theory has a bi-initial model; every model of a type theory has its internal language; the category of theories over a type theory is bi-equivalent to a full sub-2-category of the 2-category of models of the type theory.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
