Extending the Agda Implementation of Two-Level Type Theory
Master Project

MSc Project: Extending the Agda Implementation of Two-Level Type Theory

Summary

Two-level type theory (2LTT) is a type theory that combines homotopy type theory (HoTT) with a second, strict type theory in a single system. It can express constructions about HoTT — such as semisimplicial types, diagrams over categories, and staged programs — that cannot be written inside HoTT on its own. There is an existing Agda formalization of 2LTT, written by Elif Üsküplü for the Univalence Principle paper. In this project the student will develop that formalization further: complete parts of it that are unfinished, add new material, and improve the library so it is easier to reuse.

Background

In homotopy type theory the identity type a = b is understood as a space of paths, and the univalence axiom makes equality of types the same as equivalence of types. This is powerful, but it means HoTT has no usable notion of strict equality. As a result, some ordinary constructions cannot be stated inside HoTT. The standard example is the type of semisimplicial types: an infinite tower of coherence data that no one has been able to define uniformly in HoTT, precisely because there is no strict equality to phrase it with.

Two-level type theory solves this by putting two type theories side by side in one system. The inner level is HoTT; its types are “fibrant” and have the usual homotopical structure. The outer level is a strict type theory in which uniqueness of identity proofs holds. It behaves like an internal meta-theory: a place to reason about the inner theory. A coercion links the two levels, and the fibrant types of the outer level correspond to genuine HoTT types. In this setting one can, for each fixed natural number n, build the type of n-truncated semisimplicial types, work with Reedy-fibrant diagrams over inverse categories, and define notions such as (∞,1)-categories. A conservativity theorem guarantees that this extra expressive power proves nothing new about the inner theory.

The same two-level structure appears in programming languages. In Kovács’s Staged Compilation with Two-Level Type Theory, the outer level is read as compile time and the inner level as run time; conservativity of 2LTT then matches the correctness of a staged compiler. So one framework covers both parts of synthetic mathematics and metaprogramming.

Agda supports 2LTT through its --two-level flag, which adds a universe SSet of strict types alongside the usual Set. This makes Agda one of the few proof assistants where 2LTT can be used directly rather than encoded.

Starting point

The project builds on the Agda library 2LTT-Agda, written by Elif Üsküplü as part of her PhD thesis Formalizing two-level type theory with cofibrant exo-nat (published in Mathematical Structures in Computer Science, 2025). The library uses Agda’s --two-level flag, with an optional --cumulativity variant, and formalizes the two-level material needed for the Univalence Principle paper by Ahrens, North, Shulman, and Tsementzis.

A key part of this work is the cofibrant exo-natural numbers: the outer-level type of natural numbers, shown to be cofibrant, which is what makes the level-indexed constructions (such as semisimplicial types) work. The formalization also required some new results along the way, including a form of function extensionality for cofibrant types.

The library is not finished. Its documentation states that the 2LTT material assumed by the Univalence Principle paper is complete, but that the other parts of that paper are still in progress. This leaves a clear body of work: the general univalence principle for higher-categorical structures, together with the machinery it needs, has yet to be formalized. There are also open engineering questions, such as the dependence on --cumulativity, keeping the code building against current Agda versions, improving modularity and documentation, and connecting the library to the larger agda-unimath library.

Aims and objectives

The aim is to develop 2LTT-Agda further and, in doing so, to understand two-level type theory in depth. The project has a required core and a set of extensions to choose from.

Core objectives (required).

1. Understand and document the existing library: its module structure, how the two levels are set up, the fibrancy and cofibrancy infrastructure, and the cofibrant exo-nat development.
2. Get the library building against a current version of Agda and its standard library, and set up continuous integration.
3. Make one concrete, self-contained contribution to the unfinished part — for example, formalizing one component of the Univalence Principle development, or removing an assumption such as the use of --cumulativity.

Extension objectives (choose one or more).

• Formalize an application of 2LTT that is not yet in the library, such as n-truncated semisimplicial types, Reedy-fibrant diagrams over a class of inverse categories, or a worked definition and example of an (∞,1)-category.
• Formalize a further part of the Univalence Principle, such as displayed structures, indiscernibility, or the univalence principle for a specific family of structures.
• Investigate the staged-compilation reading of the library, connecting the outer/inner distinction to Kovács’s staged 2LTT and formalizing small staged-programming examples.
• Refactor the library toward a documented, modular interface, and try connecting it to agda-unimath.

Deliverables

• An extended, building 2LTT-Agda library, with the student’s contributions clearly separated and released under an open-source licence with continuous integration.
• Documentation of the library’s structure and the two-level techniques it uses.
• A thesis placing the work in context (HoTT, 2LTT, the Univalence Principle, and staged compilation if pursued), explaining the design decisions in the formalization, and reporting what was and was not achieved.

Prerequisites

The project suits a student who has, or is willing to acquire quickly:

• experience with a dependently typed proof assistant (Agda preferred; Coq/Rocq, Lean, or Idris are acceptable given willingness to switch to Agda);
• type theory at the level of a graduate course, ideally with some exposure to homotopy type theory;
• the ability to read research papers in the area.

No prior knowledge of two-level type theory is assumed; building that understanding is part of the project.

Key references

• Ahrens, North, Shulman, Tsementzis, The Univalence Principle.
• Annenkov, Capriotti, Kraus, Sattler, Two-level type theory and applications, MSCS.
• Üsküplü, Formalizing two-level type theory with cofibrant exo-nat, MSCS 2025 (arXiv:2309.09395); code: github.com/ElifUskuplu/2LTT-Agda.
• Kovács, Staged Compilation with Two-Level Type Theory, ICFP 2022 (arXiv:2209.09729).
• The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics.
• Agda documentation, Two-Level Type Theory (the --two-level flag).