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.