Homotopy Level

Definition

A homotopy level (or h-level) is a stratification of types in HoTT based on the complexity of their identity types. The levels are indexed by integers starting at -2.

We define the predicate $is - of - hlevel (n, A)$ by Induction on $n \geq - 2$ :

Base case ( $n = - 2$ ): $A$ is contractible if there is a center of contraction $c : A$ such that for all $x : A$ , $c = x$ . $is - of - hlevel (- 2, A) :\equiv isContr (A) :\equiv \sum_{c : A} \prod_{x : A} (c = x)$
Inductive step ( $n = k + 1$ ): $A$ is of level $n$ if its path spaces are of level $k$ . $is - of - hlevel (k + 1, A) :\equiv \prod_{x, y : A} is - of - hlevel (k, x = y)$ The first few levels are:

The hierarchy is cumulative. If $A$ is of level $n$ , it is also of level $n + 1$ .

$is - of - hlevel (n, A) \to is - of - hlevel (n + 1, A)$

This follows from the fact that a contractible type is a proposition (all paths in a contractible type are contractible).

$h$ -levels are closed under standard type formers.

$Π$ -types: If $B (x)$ is of level $n$ for all $x : A$ , then $\prod_{x : A} B (x)$ is of level $n$ .
$Σ$ -types: If $A$ is of level $n$ and $B (x)$ is of level $n$ for all $x$ , then $\sum_{x : A} B (x)$ is of level $n$ .
Path types: If $A$ is of level $n$ , then $x =_{A} y$ is of level $n - 1$ .
Retracts: If $A$ is a retract of $B$ and $B$ is of level $n$ , then $A$ is of level $n$ .
Equivalence: If $A ≃ B$ and $B$ is of level $n$ , then $A$ is of level $n$ .
Universes: The universe of all $n$ -types is itself an $(n + 1)$ -type (univalence implies the universe of propositions is a set, etc.).

In Cubical Agda, $h$ -levels are often indexed by $N$ starting at 0 to avoid negative integers, shifting the index by 2.

HLevel : Type
HLevel = ℕ
 
isOfHLevel : HLevel → Type ℓ → Type ℓ
isOfHLevel 0 A = isContr A
isOfHLevel (suc n) A = (x y : A) → isOfHLevel n (x ≡ y)