🔬 HoTT: Any Practical Applications Yet? (serious thread)

ok so I've been deep in the HoTT book for about 6 months now (on my third read, send help) and I keep running into this wall where I can't figure out if any of this actually does anything in the real world yet. serious question, not trying to start a flamewar.

Background for anyone who isn't familiar: Homotopy Type Theory (HoTT) is a foundational framework that interprets types as topological spaces, where proofs of equality are paths between points. The big result is the Univalence Axiom — roughly, "equivalent types are equal." This is philosophically beautiful but the axiom itself is not computationally interpretable in standard MLTT.

My question: has this moved beyond pure foundations? Like, is there actual software being written with it? Can I write a verified web server or something in HoTT today and have it run? Or is it still "we have these gorgeous mathematical results but they don't extract to runnable code"?

I ask because I spent three hours explaining univalence to my CS professor last week and when I said "and you can use this to formally verify software" she asked me to show her a real example and I had nothing. Embarrassing. I need actual ammunition here.

Things I'm specifically interested in:
1. Can univalence be given computational content?
2. What's the state of Higher Inductive Types in actual proof assistants?
3. Has anyone done synthetic homotopy theory proofs that compute?
4. Is Cubical Agda the answer to all of this?

Please be civil, this is the (serious thread) tag for a reason. nya~

Blunt answer: No. HoTT does not have practical applications in the sense of "software engineering" yet. The theory is extraordinarily beautiful and I have enormous respect for the people working on it, but you're not writing a verified web server in HoTT in 2024 and having it actually run fast enough to be useful.

The core problem is what you identified yourself — the Univalence Axiom in its original "Book HoTT" form is not computationally interpretable. It's an axiom. Axioms in type theory mean "I assert this is true but I cannot give you a program that witnesses it." The HoTT book was written on purpose without worrying about this — it's a foundations project, not a software engineering project.

The honest state of affairs: HoTT is a brilliant new foundation for mathematics, and on the math side things are happening. But "formal verification of software" is being done much more productively in Coq/Lean/Rocq without HoTT extensions. Those tools have massive libraries, good extraction, and real industrial users.

Ask your professor about Lean 4 or the CompCert verified C compiler if she wants practical formal verification.

@ProofIrrelevant I have to push back on this quite hard, sorry. You're conflating "Book HoTT" with the whole field, which is unfair.

The computational problem you describe WAS a real problem. It's been addressed. The answer is Cubical Type Theory and its implementation in Cubical Agda. Here's the deal:

This is not a minor thing. The whole criticism that "univalence has no computational content" was resolved by cubical type theory. Here's what a Higher Inductive Type looks like in Cubical Agda — specifically the circle S¹ as a HIT:

  data S¹ : Type where
    base : S¹
    loop : base ≡ base

  -- A path in S¹ from base to base.
  -- This is the generator of π₁(S¹) ≅ ℤ
  -- And YES, this computes definitionally.

The diagram for a basic HIT pushout looks like this ASCII art I keep in my notes:

       A
      / \
     /   \
    f     g
   /       \
  B ──────── C
   \         /
    \       /
     \     /
      \   /
       \ /
      B⊔ᴬC
      (pushout)

  HIT:  data Pushout (f : A → B) (g : A → C) where
          inl : B → Pushout
          inr : C → Pushout  
          push : (a : A) → inl (f a) ≡ inr (g a)
  -- 'push' is a PATH CONSTRUCTOR (higher constructor!)

You literally cannot write this kind of thing in plain Coq/Lean without ugly workarounds. In Cubical Agda it's first-class. This IS practical — it means your proofs about data structures that are equal-up-to-isomorphism can actually use that equality as a real equality.

Adding to what CubicalCat said — the synthetic homotopy theory angle is genuinely exciting and it's where I'd say "practical" means something different than "I can ship a web app with it."

The HoTT book proof that π₁(S¹) ≅ ℤ — i.e., the fundamental group of the circle is the integers — is a theorem proved purely synthetically inside type theory. No point-set topology. No quotient constructions. The circle is defined as a HIT with one point constructor and one path constructor, and the whole proof flows from that. And now in Cubical Agda, it computes.

More recently, people have been formalizing serious algebraic topology results. The Steenrod squares in HoTT! Cellular homology! Connected covers! Eilenberg-MacLane spaces! These are real mathematical results that are now machine-checked proofs, and the HoTT framework makes them shorter and more natural than classical proofs, not longer.

From the CS side: univalence means you can prove things about one data structure and automatically transfer them to an isomorphic one. That's practically useful for any verified library that has multiple implementations of the same interface. Yes it takes expertise to use, but it's real.

Is it "write a web server" practical? No. Is it "do real math and CS in a more natural framework that computes" practical? Increasingly yes.

@CubicalCat Fair point about Cubical Agda and computational univalence, I'll concede that. My frustration is more about the gap between "computes in proof assistant" and "is used to verify industrial software." Those are very different bars.

Does anyone here actually use Cubical Agda for software verification day to day? I know people use it for math. But I'm thinking of the OP's use case — convincing a CS professor that HoTT is useful for software.

The UniMath library in Coq, the mathlib in Lean — these have thousands of contributors, millions of lines of formalized math. What's the equivalent on the HoTT side? The agda/cubical library is cool but let's be honest about the scale difference here.

@ProofIrrelevant the scale point is fair. Let me actually lay out the concrete wins, because I think the framing of "practical = industry scale" is too narrow for a research-stage technology.

What Cubical Agda gives you that nothing else does:

1. Computational univalence — the famous axiom is now a theorem with computational content. If A ≃ B then A ≡ B, and this equality can be transported along. No axiom. It actually reduces.

2. HITs with definitional computation rules — Here's a more complex HIT, a Quotient Type:

  -- Integers as a HIT quotient:
  data ℤ-HIT : Type where
    _-_ : ℕ → ℕ → ℤ-HIT
    -- path constructor: (n+1)-(m+1) ≡ n-m
    cancel : ∀ n m → (succ n - succ m) ≡ (n - m)

  -- This is definitionally a quotient. No setoid nonsense.
  -- Proofs about ℤ transfer to ANY isomorphic type via univalence.

3. The Structure Identity Principle (SIP) — if two structured types (e.g., two implementations of a monoid) are pointwise equivalent, they are equal as structured types. This is massively useful for software with multiple implementations.

  -- Roughly: if M₁ ≃ M₂ as monoids, then M₁ ≡ M₂
  -- So any theorem proved about M₁ holds for M₂ for FREE.
  -- No manual transfer lemmas. This is the practical win.

4. Synthetic homotopy theory that runs. π₁(S¹) ≡ ℤ isn't just a theorem, it's a program you can evaluate.

Is this "write a web server"? No. Is it "do verified math and CS without painful bureaucratic lemma-shuffling"? Yes, actually.

Nobody has mentioned the Brunerie number yet so I'll be that person.

Guillaume Brunerie computed π₄(S³) ≅ ℤ/2ℤ in HoTT. This is a hard theorem in classical algebraic topology that requires heavy machinery to prove. In HoTT the proof was done synthetically inside type theory, and when you actually evaluate the type-theoretic proof term in Cubical Agda, it normalizes and gives you the number 2. The generator is 2. The computer confirmed it.

That is, objectively, a practical application of HoTT: using it as a computational engine to compute homotopy groups. Is it what a software engineer means by "practical"? No. Is it doing real mathematics by computer in a way that was previously only possible with enormous hand-proofs? YES.

Also worth noting: the HoTT Book itself is a remarkable artifact — it was written collaboratively by about 50 mathematicians during one year at IAS, and the entire thing is formalized. The book IS a proof assistant output in some sense.

OP here — this thread is already gold, thank you all.

Let me try to synthesize what I'm hearing:

Practical in the "it computes" sense:
✅ Cubical Agda gives computational univalence (the axiom is now a theorem that runs)
✅ HITs with definitional computation rules — quotient types, circle, pushouts, all compute
✅ Synthetic homotopy theory proofs that actually normalize
✅ The Brunerie number was literally computed, not just proved

Practical in the "software engineering" sense:
⚠️ The Structure Identity Principle is genuinely useful for verified libraries
⚠️ Univalence makes proof transfer free — big win for libraries with multiple implementations
❌ No extraction to efficient runnable code yet (compared to Lean/Coq)
❌ Ecosystem is orders of magnitude smaller than mathlib/UniMath

Questions I still have:
- What exactly IS the computational content of univalence in cubical TT? Like mechanically, what does the transport function do?
- Is Observational Type Theory (OTT) an alternative to cubical that might be more practical?
- What's the relationship between HoTT and dependent types in mainstream languages like Idris or Lean?

@UnivalenceFan re: "what is the computational content of univalence" — ok, here is my best ASCII art explanation of this:

  BOOK HoTT (axiomatic):
  ─────────────────────
  ua : (A ≃ B) → (A ≡ B)    -- axiom, no reduction rule
  transport (ua f) x = ???   -- STUCK. Does not compute.

  CUBICAL TYPE THEORY:
  ─────────────────────────────────────────────────────
  The interval I = [0,1] is primitive. A path is a 
  function  I → A.  ua is defined using the interval:

    ua (f : A ≃ B) : A ≡ B
    ua f = λ i → Glue [ i=0 ↦ (A, idEquiv) 
                       , i=1 ↦ (B, f) ]

  transport (ua f) a   =   f .fst a   -- COMPUTES to f(a)!
  ─────────────────────────────────────────────────────

  So: transporting along ua(f) literally applies the 
  underlying function of the equivalence. Univalence 
  is NOT a magic oracle. It is a structured path built 
  from GLUE TYPES that tell the system how to transport.

The Glue type is the key innovation. It says: "at endpoint i=0, this is type A; at endpoint i=1, this is type B; the gluing is given by equivalence f." Transporting along this path just applies f. Beautiful and mundane at the same time.

The CCHM paper (Cohen, Coquand, Huber, Mörtberg) is where this was worked out. Cubical Agda implements a variation of this. It's actual CS with actual reduction rules, not handwaving.

Hot take: HoTT solves a problem that was mostly created by dependent type theory itself. "Quotient types are annoying in Coq" — yes, because you're using setoids, a workaround for a limitation of the theory. HoTT/cubical fixes that limitation. That's nice, but it's not the same as solving a problem in the real world.

The real world doesn't have quotient type problems. It has bugs, race conditions, memory leaks, API mismatches. I want to see HoTT help me verify a concurrent program or a distributed system protocol. Until then, I'm filing it under "beautiful mathematics that I cannot bill a client for."

And yes I know I'm being harsh. I genuinely think it'll get there. But "computes the Brunerie number" is not what OP's professor was asking about nya~

@Setoidpilled I think you're setting an impossible standard. Lean 4 also can't verify a concurrent distributed system easily. Formal verification of concurrent systems is hard for everyone regardless of foundations.

The more relevant comparison is: for the kinds of things formal verification is used for — compiler correctness, crypto protocol verification, mathematical theorem checking — does HoTT/cubical improve on existing tools? And the answer is: for some tasks, yes.

Specifically the Structure Identity Principle (SIP) in Cubical Agda means: if you've proved something about one implementation of a data structure, you get it for free for any equivalent implementation. This eliminates a huge class of boilerplate lemmas that real verification projects suffer from. That's a real productivity win.

Also: Linear HoTT is being developed which extends HoTT with linear types for reasoning about quantum computing / resource usage. That's genuinely novel and very applied. See the NYU Abu Dhabi HoTT & Computing workshop from 2024.

Long time lurker on this topic, finally have something to add.

I work in a group that uses Cubical Agda for formalizing algebraic topology results. Here is my honest practitioner's view:

Where HoTT/Cubical is legitimately better than alternatives:

• Working with quotient structures. Integers as ℕ×ℕ/~, fractions as ℤ×ℤ⁺/~, etc. These are genuinely painful in standard Agda or Coq without HIT-style quotients. In Cubical Agda you just define the HIT and the whole machinery works.

• Proof transfer via univalence. We proved a huge theorem about one algebraic structure and then needed it for an isomorphic one. In Cubical Agda: transport (ua theEquivalence) theProof. Done. In standard Coq it would have been weeks of work rewriting lemmas.

• The proofs are often more conceptually transparent. You can literally see what the topological content of an algebraic argument is.

Where it's harder:

• The learning curve is brutal. Cubical primitives are not intuitive. The cube syntax took me months to internalize.

• The ecosystem. Mathlib for Lean has basically everything. Agda/cubical is much more research-focused.

• Compilation/checking speed. Large cubical proofs can be slow to typecheck.

So: practical? For the right applications, yes, today. For general software verification, not yet but the foundations are being laid.

@OmegaCatGirl this is exactly the kind of practitioner view I was hoping for. Thank you.

So my takeaway for convincing my professor: don't pitch HoTT as "better Coq for software verification." Pitch it as "a new foundations that makes certain classes of formal proof dramatically easier, particularly anything involving quotient structures, isomorphism-invariant reasoning, and synthetic topology/algebra."

And for the computational question: "the HoTT book uses an axiom, but Cubical Type Theory has replaced that axiom with a genuine computation rule, and Cubical Agda implements this, giving us a proof assistant where HoTT-style reasoning actually computes."

Is that a fair summary for someone to give a skeptical professor?

Also @CubicalCat your ASCII diagram of the Glue type was genuinely the best explanation of computational univalence I've ever seen. Bookmarking this whole thread. 💜

📌 MODERATOR NOTE: Great thread quality so far! Keeping this stickied to the top of the category for a while. Please keep the [serious] tag discussion civil. No "HoTT vs set theory" holy wars please — that's what the Foundations War Megathread is for.

Reminder that replies continue on pages 2–5. This is page 1 of 5 (89 total replies).

~ nya-chan-mod 🐱