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 Type 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 Type as fibrant types, inner types, and types, respectively.

Function-types belong to Type 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 Type instead if all their inputs belong to Type. In particular, any type in Type has an isomorphic copy in SSet defined as a trivial record:

record c (A : Type) : 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 Type 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 : Type a} (x : A) : A → Type 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 : Type} {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 Type when the motive lies in SSet. Similarly, we can map from the strict natural numbers into the ordinary ones:

data ℕ : Type 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 Type, but this feature is disputed.)