We define and develop two-level type theory (2LTT), a version of Martin-Löf type theory which combines two different type theories. We refer to them as the inner and the outer type theory. In our case of interest, the inner theory is homotopy type theory (HoTT) which may include univalent universes and higher inductive types. The outer theory is a traditional form of type theory validating uniqueness of identity proofs (UIP). One point of view on it is as internalised meta-theory of the inner type theory. There are two motivations for 2LTT. Firstly, there are certain results about HoTT which are of meta-theoretic nature, such as the statement that semisimplicial types up to level $n$ can be constructed in HoTT for any externally fixed natural number $n$. Such results cannot be expressed in HoTT itself, but they can be formalised and proved in 2LTT, where $n$ will be a variable in the outer theory. This point of view is inspired by observations about conservativity of presheaf models. Secondly, 2LTT is a framework which is suitable for formulating additional axioms that one might want to add to HoTT. This idea is heavily inspired by Voevodsky's Homotopy Type System (HTS), which constitutes one specific instance of a 2LTT. HTS has an axiom ensuring that the type of natural numbers behaves like the external natural numbers, which allows the construction of a universe of semisimplicial types. In 2LTT, this axiom can be stated simply be asking the inner and outer natural numbers to be isomorphic. After defining 2LTT, we set up a collection of tools with the goal of making 2LTT a convenient language for future developments. As a first such application, we develop the theory of Reedy fibrant diagrams in the style of Shulman. Continuing this line of thought, we suggest a definition of (infinity,1)-category and give some examples.

翻译：本文定义并发展了双层类型理论(2LTT)，这是马丁-洛夫类型理论的一种变体，它结合了两种不同的类型理论。我们分别称其为内层类型理论与外层类型理论。在本文关注的情形中，内层理论是包含了单值宇宙和高阶归纳类型的同伦类型理论(HoTT)，外层理论则是验证同一性证明唯一性(UIP)的传统类型理论形式。一种视角将其视为内层类型理论的内化元理论。发展2LTT有两方面动机：其一，某些关于HoTT的元理论性质结果（例如：对于任意外部固定的自然数$n$，可构造$n$阶半单纯型）无法在HoTT自身中表述，但可以在2LTT中形式化并证明——此时$n$将成为外层理论中的变量。这一观点受预层模型保守性研究的启发；其二，2LTT是适用于表述HoTT附加公理的框架，该思想深受Voevodsky的同伦类型系统(HTS)影响——HTS正是2LTT的一个特例。HTS通过公理确保自然数类型与外部自然数具有相同行为，从而构造出半单纯型宇宙。在2LTT中，该公理可简化为要求内层与外层自然数同构。在定义2LTT后，我们建立了一系列工具集，旨在使2LTT成为未来研究的便捷语言。作为首个应用实例，我们以Shulman风格发展了Reedy纤维图理论。沿此思路，我们提出(无穷,1)-范畴的定义并给出若干实例。