Translations between Type Theories

依赖类型理论是使我们能够形式化地验证定理和证明软件正确性的逻辑系统。商业应用的一个例子是网络浏览器Chrome使用的谷歌加密，而基于计算机的证明助手可以验证现代数学。近年来，新的类型理论甚至开始成为研究复杂数学学科的高度专业化的语言。2010年左右，同伦型理论的诞生彻底改变了这一研究领域，同伦型理论是一种结合了逻辑、编程和抽象同伦理论的变体。受此启发，过去十年出现了大量的新类型理论，包括立方体理论、笛卡尔立方体理论、情态理论、空间理论、衔接理论、定向理论和两级类型理论。它们之间的关系几乎是完全未知的，一个子领域的成功对其他子领域的影响是先验的有限的，显著阻碍了整个研究领域的进步。Triple-T项目将构建类型理论之间的翻译，统一不同社区的努力。这将通过创建多层次类型理论来实现，这是一个结合了个别(目前不兼容的)理论的优势的框架，并提出了一种全新的方法来研究相关性，即所谓的外延保守性。作为一个副作用，它将极大地有利于新型理论的设计，因为它提前确定了需要哪些特征才能保持某些所需的性质。该项目将为该领域提供可立即应用的强大工具，但也有可能产生巨大的长期影响。通过将当前不兼容系统的最有用的方面结合在一起，Triple-T将永久加快新型理论和更先进的证明助手的发展，数学结果的形式化，以及软件的正式验证。

Dependent type theories are logical systems that enable us to formally verify theorems and certify the correctness of software. An example of a commercial application is Google's encryption used by the web browser Chrome, while computer-based proof assistants can verify modern mathematics. In recent years, new type theories have started to even serve as highly specialised languages for the study of complex mathematical disciplines.Around 2010, the research field was revolutionised by the inception of homotopy type theory, a variation that combines insights from logic, programming, and abstract homotopy theory. Inspired by this, the last decade has seen a plethora of new type theories including cubical, cartesian cubical, modal, spatial, cohesive, directed, and two-level type theory. Their relationships with each other are almost completely unknown and a success in one subfield has a priori limited consequences for other subfields, significantly hindering the progress of the research area as a whole.The project Triple-T will construct translations between type theories, unifying the efforts of different communities. This will be achieved by creating multi-level type theory, a framework that combines the advantages of individual (currently incompatible) theories and presents a radically new approach to studying correlations known as conservativity of extensions. As a side effect, it will greatly benefit the design of new type theories by determining in advance which features are needed in order to preserve certain desired properties.While the project will provide the field with powerful tools that can be applied immediately, it also has the potential for enormous long-term impact. By making it possible to combine the most useful aspects of currently incompatible systems, Triple-T will permanently speed up the development of new type theories and more advanced proof assistants, the formalisation of mathematical results, and the formal verification of software.