# 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.