Translations between Type Theories

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.