H-level

In homotopy type theory, the h-level of a type is a measure of "how propositional" it is.

A type $T$ is a proposition if any of its two inhabitants are identified:

  is-prop : ∀ {ℓ} → Type ℓ → Type ℓ
  is-prop T = (x y : T) → x ≡ y

A type is a set if its identities are proof-irrelevant:

  is-set : ∀ {ℓ} → Type ℓ → Type ℓ
  is-set T = (x y : T) → is-prop (x ≡ y)

In fact, if a type is a set, an identity $x\equiv y$ is a full-on a equality.

Further, a type whose identities are sets is called a groupoid:

  is-groupoid : ∀ {ℓ} → Type ℓ → Type ℓ
  is-groupoid T = (x y : T) → is-set (x ≡ y)

And so on. This sequence of propositions to sets to groupoids corresponds to higher and higher h-levels. Propositions are at h-level 1, sets are h-level 2, groupoids are h-level 3, and so on. H-level 0 is some other shit about contractible types lol.

Inbox

• A contractible type has an inhabitant called the "center of contraction," and a path from every other other inhabitant to the center. A singleton up to homotopy.[cite:@rijke2022introduction]

References

• [cite:@1lab]

• [cite:@rijke2022introduction]