📐 n-Truncations, h-levels, and the hierarchy of types in HoTT

Okay everyone, I wanted to write up a somewhat comprehensive intro to the h-level hierarchy (also called truncation levels, or n-types) because I feel like this is one of the most beautiful structural ideas in HoTT and it took me an embarrassingly long time to really grok it. This ended up long. Grab your tea or catnip. 🍵

§1 — The Core Idea

In classical set theory, all collections are essentially sets — elements are equal or they aren't, full stop. But in HoTT, types carry homotopical structure: paths between points, paths between paths, and so on upward. The h-level (or truncation level) of a type measures how much of this higher structure is non-trivial.

The key insight: every type in type theory is naturally an ∞-groupoid, with the structure of morphisms, 2-morphisms, 3-morphisms, etc., given by the identity type (propositional equality). The truncation level tells you at what dimension this structure collapses to triviality.

§2 — The Hierarchy

Here's the full table. Note that Voevodsky originally called these "types of h-level n" starting at 0, but the community now commonly uses the homotopy-theoretic numbering starting at −2:

Level	HoTT Name	Classical Analogue	Intuition
−2	Contractible (contr)	Singleton / terminal object	Exactly one element, up to homotopy
−1	hProp / mere proposition	Truth value (Bool, Prop)	At most one element up to equality
0	hSet / set	Ordinary set (ZFC, ETCS)	Elements with no higher path structure
1	hGroupoid / groupoid	Category with invertible morphisms	Non-trivial paths, trivial 2-paths
2	2-groupoid	Bigroupoid	Non-trivial 2-paths, trivial 3-paths
n	n-type	n-groupoid	Trivial above dimension n
∞	General type (∞-groupoid)	Topological space (up to hmtpy)	Possibly non-trivial at all levels

§3 — Propositions: the −1-types (hProps)

A type A is a mere proposition (or hProp, or −1-type) if any two of its elements are propositionally equal. Formally:

isProp (A : Type) : Type
  := ∀ (x y : A), x = y

This means there is at most one proof of the proposition — all proofs are equal. This is "proof irrelevance." Examples: ⊤ (trivially), ⊥ (vacuously), x = y in an hSet, and any statement about decidable equality in ℕ.

The −1-truncation ‖A‖₋₁ (written ∥A∥) collapses any type into a proposition — it tells you merely whether A is inhabited, erasing the witness. This is also called "squashing" or propositional truncation. It's implemented beautifully as a higher inductive type that forces all elements to be equal.

§4 — Sets: the 0-types (hSets)

A type A is an h-set (or 0-type) if all its identity types are propositions. That is:

isSet (A : Type) : Type
  := ∀ (x y : A), isProp (x = y)

In other words, there is at most one path between any two points — uniqueness of identity proofs (UIP). Examples: ℕ, ℤ, Bool, finite types, and most "ordinary" mathematical objects you encounter every day. The 0-truncation ‖A‖₀ gives you the set of connected components of the space A.

§5 — Groupoids: the 1-types

A 1-type is like a groupoid: it can have non-trivial paths between points (morphisms), but all 2-paths (paths between paths) are trivial — they are all equal. The universe of sets Set is itself a 1-type! (Because paths between sets are equivalences, and two equivalences are equal iff they agree on all elements — which is a proposition.)

A great motivating example: the circle S¹ in HoTT is a 1-type with a non-trivial fundamental group π₁(S¹) ≅ ℤ, while all higher homotopy groups vanish by 1-truncatedness.

§6 — The General Pattern

A type A is an n-type iff all of its identity types are (n−1)-types. This gives us a recursive definition rooted at contractibility (−2-types). Every n-type is also an m-type for all m ≥ n.

§7 — Connection to Classical Topology

The correspondence with classical topology is deep and beautiful. Every topological space X has a fundamental ∞-groupoid whose k-morphisms are the k-dimensional paths in X. HoTT's type theory natively encodes this: the identity types give you path spaces, and the tower of iterated identity types encodes all higher homotopy groups.

The n-types in HoTT correspond precisely to homotopy n-types in classical topology — spaces whose homotopy groups πₖ vanish for k > n. So an hSet (0-type) is like a space with trivial π₁, π₂, ... — just a discrete set of connected components.

Categorically, n-types correspond to n-groupoids. The homotopy hypothesis says this correspondence is essentially an equivalence of theories!

Anyway, hope this helps someone! This took me forever to internalize. Questions/corrections welcome nya~ 🐾

Great write-up! Stickying this for the Foundations subforum 📌

I want to add some precision to §3. The propositional truncation ‖A‖ isn't just "forgetting the witness" — it's a genuine higher inductive type construction. In Agda-style notation it looks roughly like:

data ‖_‖ (A : Type) : Type where
  ∣_∣    : A → ‖ A ‖                      -- constructor
  squash : (x y : ‖ A ‖) → x ≡ y          -- path constructor

The squash path constructor forces all elements of ‖A‖ to be equal, making it a proposition. The universal property says: to map out of ‖A‖ into a proposition P, it suffices to give a map A → P.

Also worth noting: the −2-type (contractible type) is the base of the whole recursion. A type is contractible iff it's equivalent to the unit type 𝟙. Everything collapses there. Being contractible is strictly stronger than being a proposition — it's not just "at most one element" but "exactly one." This is important because equivalences are defined so that their fibers are contractible, not merely propositional!

This is exactly what I needed, thank you!! I was struggling with the connection between the formal definition and the geometric intuition.

Question for §7: you say "n-types in HoTT correspond to homotopy n-types in classical topology — spaces whose homotopy groups πₖ vanish for k > n." So does that mean the 2-sphere S² is NOT an hSet (0-type) in HoTT? Because S² has non-trivial π₂ and also non-trivial π₃ = ℤ (the Hopf fibration!)?

Exactly right! The 2-sphere S² defined as a higher inductive type in HoTT is not an hSet — in fact it's not even a 1-type (groupoid). It has non-trivial π₂ ≅ ℤ, so it's at least a 2-type. And because of the famous result π₃(S²) ≅ ℤ (via the Hopf fibration), it's not a 2-type either! S² is actually an ∞-type — it has interesting homotopy groups in infinitely many dimensions (this is the deep mystery of homotopy groups of spheres).

The HoTT community has actually computed π₃(S²) ≅ ℤ synthetically inside type theory using the Hopf fibration — which is a stunning achievement. See the HoTT Book chapter on homotopy theory!

For contrast: the circle S¹ is a 1-type. It has π₁(S¹) ≅ ℤ (proven in HoTT!), and all higher homotopy groups vanish — which is exactly what 1-truncatedness means. So S¹ is a groupoid (1-type) but not a set (0-type). Beautiful, right? nya~

Worth adding: the truncation operation is a modality — or more precisely, the predicate "is an n-type" is part of a (reflective) modality. This means n-truncation has a universal property as a left adjoint:

This is exactly like how sheafification (in topos theory) is left adjoint to the inclusion of sheaves into presheaves. The modality viewpoint is explored in the HoTT Book in the chapter on modalities, and ties into the broader framework of orthogonal factorization systems on the universe — the (n-connected, n-truncated) factorization system.

The connection to classical topology is via Postnikov towers: every space X has a Postnikov tower where the k-th stage is the k-truncation τ≤ₖX, and the whole tower assembles to recover X. In HoTT this is totally native!

Follow-up: what about the universe 𝒰 itself? What truncation level is it?

Excellent question and the answer is: no finite level. The universe 𝒰 is an ∞-type. Here's why: paths in 𝒰 between types A and B are equivalences A ≃ B (by univalence). So π₁(𝒰) is the "groupoid of types and equivalences." But equivalences between A and A form the autoequivalence group Aut(A), which can be arbitrarily complex — e.g., Aut(S²) has complicated higher homotopy groups. So 𝒰 cannot be n-truncated for any finite n.

In fact, univalence implies that the subuniverse of all h-sets inside a univalent universe is itself not an h-set — it's at least a 1-type (groupoid), because paths between h-sets are equivalences (bijections), and automorphisms of a set form a group, not just a set.

This is one of those places where HoTT diverges wildly from classical foundations. The "type of all types" has genuinely infinite-dimensional structure. Very meow-worthy. 🐾

One thing that tripped me up forever: there are two numbering schemes floating around in the literature and they're off by two from each other!

• Voevodsky's original h-level numbering: contractible = h-level 0, propositions = h-level 1, sets = h-level 2, groupoids = h-level 3, ...
• Homotopy-theoretic truncation level (what OP uses): contractible = −2, propositions = −1, sets = 0, groupoids = 1, ...

The second is now more standard in the community and matches classical algebraic topology. Voevodsky himself used the first in his early Coq libraries. If you're reading old papers or the original Agda/Coq HoTT libraries, watch out for this discrepancy nya~

Also a quick note on implementation: in Lean 4 / Mathlib, propositions are the Prop universe which is exactly the (-1)-types. In Agda with --cubical, you have access to all the truncation levels natively through the HITs machinery. In Coq-HoTT, truncation levels are represented as natural numbers offset by 2 (i.e. Voevodsky's numbering).

Oh yes, thank you for this — I should have emphasized it more. The offset-by-2 comes from the fact that Voevodsky started at 0 (for contractible) while homotopy theorists start at −2, and the off-by-2 comes from the recursive step (an n-type is one whose identity types are (n-1)-types, so you need to bottom out somewhere).

For those confused: Voevodsky's h-level n = truncation level n − 2 in the homotopy-theoretic convention.

The reason −2 is the base case is elegant: "being contractible" is the statement that a type is equivalent to the unit type, i.e., it's trivial at all dimensions. Starting there, −1-types (propositions) are types whose identity types are all contractible (i.e., there is at most one path between any two points), and 0-types (sets) are types whose identity types are all propositions. The recursion bottoms out perfectly. nya~

This thread is gold. Adding to the topology connection in §7:

Classically, an Eilenberg–MacLane space K(G, n) is a space that has πₙ ≅ G and all other homotopy groups trivial. In HoTT, these can be constructed synthetically — K(G,1) is just the delooping BG of the group G, defined as a higher inductive type. K(G,n) for higher n is then constructed iteratively. The fact that you can construct Eilenberg–MacLane spaces as HITs and then prove they have the right homotopy groups entirely within type theory — that's genuinely mind-blowing to me.

And the 0-truncation ‖A‖₀ corresponds to π₀(A) — the set of path components of A. So truncation is just HoTT's native way of talking about the classical Postnikov tower. meow!! 🐾