We define and develop two-level type theory (2LTT), a version of Martin-L\"of 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，可在HoTT中构造至多n层的半单纯类型"这类断言，无法在HoTT自身中表达，但可在2LTT中形式化并证明，其中n是外层理论中的变量——这一观点受预层模型保守性观察的启发；其二，2LTT是适于表述可能添加到HoTT中的额外公理的框架。该思想深受Voevodsky同伦类型系统（HTS）的启发，而HTS正是2LTT的一个具体实例。HTS含有一条确保自然数类型行为与外部自然数相同的公理，这使得构建半单纯类型的宇宙成为可能。在2LTT中，该公理可简单表述为要求内层和外层自然数同构。在定义2LTT后，我们建立了一套工具集，旨在使2LTT成为未来发展的便捷语言。作为首个此类应用，我们以Shulman的风格发展了Reedy纤维化图表理论。延续这一思路，我们提出了(无穷,1)-范畴的定义并给出若干实例。