📐 Higher Inductive Types — what are they and why do we need them?

Okay so you've learned about ordinary inductive types — ℕ, lists, trees, etc. You know that they're defined by point constructors: zero : ℕ, suc : ℕ → ℕ, and so on. Every element of the type is built from these constructors.

But here's the thing: in Homotopy Type Theory (HoTT), types are spaces and equality proofs are paths. So what if we want to define a type that has non-trivial path structure baked in from the start? Like… what if we want a type that is a circle? A torus? This is exactly where Higher Inductive Types (HITs) come in!

HITs are inductive types that can have not just point constructors, but also path constructors (and higher path constructors). A path constructor introduces a proof of equality between elements of the type being defined.

Key insight: ordinary inductive types tell you what the points of a type are; HITs additionally tell you what the paths (and higher paths) are.

The canonical first example is the circle. The circle S¹ is inductively generated by a single point and a single non-trivial loop. In Cubical Agda:

The loop constructor says "there is a path from base to base". This is a non-trivial path — it's not refl! This single path constructor is enough to give S¹ the homotopy type of the topological circle.

The elimination/recursion principle is also richer: to define a function out of S¹, you must provide not only a point in the target, but also a loop at that point. A map f : S¹ → X is specified by giving a point and a loop in X — the image of the generators.

Let's go further. The torus is generated by one point, two loops, and a 2-path (a path-between-paths) witnessing that the two loops commute. In Cubical Agda it looks like:

Functions defined by pattern-matching on HITs compute definitionally, for all constructors. This means we get actual computational content, not just propositional equalities!

Nyaa~ That last line is wild. The torus is (propositionally equal to) the product of two circles. This is an elementary result in topology that has a surprisingly non-trivial proof in Book HoTT due to lack of definitional computation for higher constructors, but in Cubical Agda with proper HITs it's almost trivial!

Another key example: suspensions. Given a type A, the suspension Σ A has two poles and a meridian path for each point of A:

The suspension operation builds higher spheres from lower ones. Susp Bool ≃ S¹, Susp S¹ ≃ S², and so on. This is the key to doing synthetic homotopy theory in type theory!

HITs aren't just for topology nerds. They're also essential for logic! Truncations can be constructed using higher inductive types and are quite important to doing homotopy theory in type theory.

The propositional truncation ‖ A ‖₋₁ (aka ∥ A ∥) squashes all paths together so the result is a mere proposition:

The (-1)-truncation is known as the propositional truncation: given a type A it returns a proposition ∥ A ∥ which is true if and only if A is inhabited. The path constructor squash adds paths between all pairs of elements — collapsing the type into a proof-irrelevant proposition.

More generally, the n-truncation ‖ A ‖ₙ equates all morphisms of level higher than n in A. For example:

• (-2)-truncation: contractibility (everything is trivial)
• (-1)-truncation: mere proposition (propositional truncation)
• 0-truncation: h-set (set-truncation — the set of connected components)
• 1-truncation: h-groupoid (groupoid-truncation)

Perhaps the most general construction: pushouts. Given types A, B, C and maps f : C → A, g : C → B, the pushout glues A and B together along C:

HITs generalise quotient types, and allow us to define types with non-trivial higher equality types, such as spheres, suspensions and the torus. But they also construct more mundane things like the Cauchy reals, free algebras, and quotient types!

Short answer: because classical set-theoretic foundations can't directly express homotopy-invariant constructions. In set theory, a "quotient" is always a quotient by a set-level equivalence relation. HITs let us quotient by a higher structure.

Also: without HITs, we can't even define the fundamental group of the circle internally in type theory! We need S¹ to even state what π₁(S¹) = ℤ means.

Next to univalence, HITs are the most important new aspect of homotopy type theory, allowing us to construct higher-dimensional "spaces" such as spheres and tori; perform homotopical constructions such as suspensions, truncations, localizations, and homotopy colimits; and generate free algebraic structures of all sorts.

I'll stop here for now — this post is already getting long nya~ But please ask questions! I'm especially happy to go deeper on any specific HIT. Next post I'll cover the induction principle in detail — i.e., how to actually prove things about HITs using dependent elimination. 🐾

Excellent intro MewMorphism! 🐾 I want to add something that I think is often glossed over — the distinction between book HoTT HITs and Cubical HITs.

In the HoTT Book (and Agda without --cubical), HITs are postulated axiomatically. You get the statements of the computation rules but they don't hold definitionally — only propositionally. This means you have to manually transport along these equalities everywhere, which becomes a huge pain.

In Cubical Agda, HITs are first-class citizens. The cubical mode extends Agda with computational univalence and higher inductive types, giving computational meaning to HoTT and Univalent Foundations. This means path constructors compute definitionally — no manual transports needed!

The key technical insight is that Cubical Agda implements a variation of CCHM Cubical Type Theory where the Kan composition operations are decomposed into homogeneous composition and generalized transport — this is what makes the general schema for HITs work.

The primitive building block in cubical type theory is the interval type I. A path p : a ≡ b is literally a function I → A with p i0 = a and p i1 = b. This is why path constructors like loop : I → S¹ with boundary conditions make sense!

One thing I'd add to your §6 on pushouts: many other HITs are special cases of pushouts! Suspensions, joins, mapping cones, wedge sums… they're all homotopy pushouts. There's a whole research area on the interdefiability of HITs — trying to build as many HITs as possible from just the pushout.

Also worth mentioning: Cubical Agda supports parameterized and recursive HITs too — like set quotients, propositional truncation, the integers modulo 2, free monoids, etc. These go beyond the "geometric" HITs and into actual programming use-cases!

Thank you both! This is exactly the thread I needed nya~~

I want to zoom in on something OP mentioned: the role of univalence in making HITs work properly. It's subtle but important.

Right! And even with S¹ defined as a HIT, computing π₁(S¹) = ℤ requires univalence in an essential way. The univalence axiom plays an essential role in calculating homotopy groups — without univalence, type theory is compatible with an interpretation where all paths, including the loop on the circle, are the identity.

In other words: if you define S¹ as a HIT but work in plain MLTT (no univalence), you cannot prove that loop ≠ refl! The loop might be trivial for all you know. Univalence is what gives the path constructors their "teeth". Univalence allows paths in the universe to have computational content, and this is used to extract information from paths in higher inductive types.

The proof of π₁(S¹) ≅ ℤ is one of the highlights of HoTT. Here's the strategy:

• Define the universal cover of S¹ as a fibration over S¹
• The fiber over base is ℤ (with the integers as a HIT themselves, or via univalence)
• The transport along loop gives the successor function on ℤ
• Hence Ω(S¹, base) ≃ ℤ by the encode-decode method

This is synthetic homotopy theory! We don't need to build CW-complexes or topological spaces — it all falls out of the type-theoretic structure.

And it goes even further! Combining HITs with univalence, we can calculate π₃(S²), construct long exact sequences and the Hopf fibration, and prove the Freudenthal suspension theorem. All formally, machine-checked in Agda. Wild nya.

The Hopf fibration is defined as a fibration S¹ → S³ → S², and its fiber sequence gives the exact sequence that lets us compute π₃(S²) = ℤ. This was one of the first major results of synthetic homotopy theory!

Hi!! Lurker here, first post 🐾 This thread is amazing!

I have a question about the HIT induction principle for S¹. I get how S¹-rec works (recursion into a non-dependent type), but how does the dependent eliminator work? Like, what if I want to prove a property of every element of S¹?

The PathP part is confusing me. It seems like a "path over a path"? Like a dependent path?

Great question NyaTopos!! Welcome to CGPA nya~ 🐾

So: PathP is a "heterogeneous path" or "path over a path". The type PathP (λ i → A i) a b is a path from a : A i0 to b : A i1 that lies over the path λ i → A i.

Why do you need it for circle induction? Because if you have P : S¹ → Type (a fibration over S¹), and you give a point b : P base, the "path" you need to provide over loop goes from b to b... but in the transported fiber. The type of b changes as we travel around the loop!

Concretely: if your fibration P is trivial (doesn't depend on the base), then PathP (λ i → P (loop i)) b b reduces to an ordinary b ≡ b in P base. That's the non-dependent case (recursion). But for genuine induction you need the full PathP.

A worked example: proving that S¹ has a non-trivial self-map using induction, or computing the π₁ using the encode-decode method (which UnivalenceFan sketched above) — these all use the dependent eliminator with PathP!

This thread is purr-fect 🐾 I want to add a perspective from the semantic/model theory side because I think it helps motivate why HITs work the way they do.

The key insight: HITs correspond to homotopy colimits in the world of ∞-groupoids / spaces. The pushout HIT corresponds to the homotopy pushout in spaces. The suspension corresponds to the unreduced suspension in topology. The circle corresponds to the simplest non-trivial CW complex: a point with a 1-cell attached to itself.

From this perspective, the path constructors in a HIT are exactly the attaching maps for cells in a CW complex! HITs provide direct, logical descriptions of some of the basic spaces and constructions of homotopy theory: spheres, cylinders, truncations, localizations, etc.

The reason we need HITs and can't just use ordinary type theory + axioms is that axioms destroy computation. When you postulate a path constructor axiomatically, transporting along it has no reduction rule. With a proper HIT in cubical type theory, the transport reduces definitionally. This is crucial for actually computing things.

And this is not just abstract theory — HITs have concrete programming applications! Free algebras (free monoids, free groups, free categories), finitely presented algebras, multisets, association lists modulo permutation — all HITs! The Cauchy reals are a beautiful example where HITs eliminate the need for the axiom of choice.

One more important HIT family I didn't see mentioned yet: set quotients. This is arguably the most practically useful HIT for day-to-day programming and proof work.

The squash/ truncation constructor is what makes the quotient an actual set (0-type) rather than something with non-trivial higher structure. This is a two-level HIT: one path constructor for the equivalences, and one for set-truncation.

The 0-truncation of a space is the set of its connected components. And importantly, we can build free algebras this way — free monoids, free groups, and more. The combination of point constructors (operations), path constructors (equations), and truncation constructors (set-level) gives us finitely presented algebraic structures as HITs!

By the way, for those interested in the theoretical underpinnings — check out the papers by Lumsdaine & Shulman on semantics of HITs in model categories, and the Coquand-Huber-Mörtberg paper on HITs in cubical type theory. The interdefiability question (which HITs can be built from pushouts) is also a really nice research area!

Resources:

• 🔗 Cubical Agda learning resources megathread
• 🔗 HoTT Book reading group (Chapter 6 — HITs)
• 🔗 Walkthrough: π₁(S¹) = ℤ proof in Cubical Agda
• 🔗 The Hopf fibration formalized

Can I ask a practical question nya? I've been trying to use propositional truncation in Agda and I keep running into this issue:

I understand conceptually that ∥ A ∥ is a proposition so the squash case should be fine, but Agda won't accept it without me explicitly handling it...

Use recPropTrunc (or ∥-∥-rec in some libraries) nya! You're not supposed to pattern-match on a truncated type directly when the target is not propositional. Instead, use the recursor:

The key insight: the elimination principle for ∥ A ∥ into a proposition P only asks for A → P. The path constructor case (squash) is automatically satisfied because P is already a proposition! This is the whole point — you can "extract" information from a truncation as long as you're mapping into something that doesn't care about the proof.

In Cubical Agda, if you're using --cubical mode, you can also just do ∥-∥.rec isPropP f or use the do-notation for propositional truncation. It's quite ergonomic once you get used to it 🐾