Two-Level Type Theory

Basics

Two-level type theory (2LTT) refers to versions of Martin-Löf type theory that combine two type theories: one “inner” level that is potentially a homotopy type theory or cubical type theory, which may include univalent universes and higher inductive types, and a second “outer” level that validates uniqueness of identity proofs.

Since version 2.6.2, Agda enables 2LTT with the --two-level flag. The two levels are distinguished with two hierarchies of universes: the usual universes Set for the inner level, and a new hierarchy of universes denoted SSet (for “strict sets”) for the outer level.

Note

The types in SSet have various names in the literature. They are called non-fibrant types in HTS (2017), outer types in 2LTT (2017), and exo-types in UP (2021). Similarly, these references refer to the types in Set as fibrant types, inner types, and types, respectively.

Function-types belong to Set if both their domain and codomain do, and to SSet otherwise. Records and datatypes can always be declared to belong to SSet, and can be declared to belong to Set instead if all their inputs belong to Set. In particular, any type in Set has an isomorphic copy in SSet defined as a trivial record:

record c (A : Set) : SSet where
  constructor ↑
  field
    ↓ : A

open c

The main differences between the two levels are that, firstly, homotopical flags such as --without-K and --cubical apply only to the Set level (the SSet level is never homotopical); and secondly, datatypes belonging to the inner level cannot be pattern-matched on when the motive belongs to the outer level (this is necessary to maintain the previous distinction).

As a primary example, we can define separate inductive equality types for both levels:

infix 4 _≡ˢ_ _≡_

data _≡ˢ_ {a} {A : SSet a} (x : A) : A → SSet a where
  reflˢ : x ≡ˢ x

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  refl : x ≡ x

With these definitions, we can prove uniqueness of identity proofs for the strict equality even if --without-K or --cubical is enabled:

UIP : {a : Level} {A : SSet a} {x y : A} (p q : x ≡ˢ y) → p ≡ˢ q
UIP reflˢ reflˢ = reflˢ

We can also prove that strictly equal elements are also non-strictly equal:

≡ˢ-to-≡ : {A : Set} {x y : c A} → (x ≡ˢ y) → (↓ x ≡ ↓ y)
≡ˢ-to-≡ reflˢ = refl

The opposite implication, however, fails because, as noted above, we cannot pattern-match against a datatype in Set when the motive lies in SSet. Similarly, we can map from the strict natural numbers into the ordinary ones:

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

data ℕˢ : SSet where
  zeroˢ : ℕˢ
  succˢ : ℕˢ → ℕˢ

ℕˢ-to-ℕ : ℕˢ → ℕ
ℕˢ-to-ℕ zeroˢ = zero
ℕˢ-to-ℕ (succˢ n) = succ (ℕˢ-to-ℕ n)

but not vice versa. (Agda does currently allow mapping from the empty SSet to the empty Set, but this feature is disputed.)

If the --two-level flag is combined with --cumulativity, then each universe Set a becomes a subtype of SSet a. In this case we can instead define the coercion c to be the identity function:

c' : Set → SSet
c' A = A

and replace the coercions ↑ and ↓ with the identity function. However, this combination currently allows some functions to be defined that shouldn’t be allowed; see Agda issue #5761 for details.