📐 Cubical Type Theory ELI5 — I keep hearing about it but am scared

Hi everyone!! Long time lurker, first real post (aside from my intro).

So I've been trying to get into HoTT and I keep seeing "cubical type theory" everywhere. People on this forum and on the HoTT discord throw the acronyms CCHM, CHM, Cubical Agda around like they're obvious, but when I try to read the actual papers my brain just gives up immediately. 😭

I've read the HoTT Book (like, most of it) and I vaguely understand that univalence is an axiom there — you postulate it. And I know that's apparently a problem? But I don't really understand why that's bad or what cubical type theory actually does differently.

Could someone please give me a gentle ELI5? I'm not scared of math but I am scared of 50-page papers full of De Morgan algebras. 🙈

Thank you in advance!! 🐱

Welcome to your first real post!! 🎉 This is actually one of my favourite topics to explain, so let me try.

The core problem with Book HoTT

You're right that univalence in the HoTT Book is an axiom. That means it's a statement you add to the type theory without giving it any computational rule — you just say "this is true, trust me." The problem is that when you add an axiom, there is no way for Agda or Coq to know how it should compute. In particular, canonicity no longer holds — you can produce terms that are stuck (booleans that are neither true nor false, for example, that don't reduce further). It's like having a programming language where you can't actually run the programs.

What cubical type theory does instead

Cubical TT gives the univalence axiom actual computational content. Instead of just asserting it, the type theory is built so that univalence is a provable theorem. This means the system stays canonical — every closed term computes to a value. This is also why it's called "cubical": the key idea is to add an interval type I where a variable i : I corresponds intuitively to a point in the real unit interval [0, 1].

A path between two terms a b : A is literally a function I → A that sends i0 to a and i1 to b. A 2-dimensional path (a homotopy between paths) is a function I → I → A. A 3-dimensional one is I → I → I → A. Hence: cubes!

Notice funExt: in Book HoTT you need to postulate it. In cubical TT it falls out directly! Function extensionality is directly provable.

Great start from CubicalCatgirl! Let me add a bit more intuition for OP.

Think of it this way. In ordinary MLTT, equality is given by the identity type Id A a b, which is inductively generated just by refl : Id A a a. The elimination principle (J) is powerful, but opaque — you can't look inside a proof of equality and compute with it directly.

Cubical TT replaces this opacity with something concrete. The core idea of HoTT is a correspondence between paths (as in topology) and proof-relevant equalities — and in cubical TT this correspondence is taken very literally: a path in type A is represented as a function out of the interval, I → A. You can evaluate that function. Paths compute!

This is the magic: because equality proofs are functions, you can do things to them. You can compose paths, reverse them (using the De Morgan negation ~ i on the interval), and crucially, you can transport values along them in a way that actually computes.

The De Morgan algebra on I

The interval I isn't just a boring interval. Its elements form a De Morgan algebra with min (∧), max (∨), and negation (~). This gives you "connections" — the ability to build higher-dimensional cubes out of lower-dimensional ones. It's what makes the whole thing tick.

In Book HoTT you prove sym by J-induction. Here it's a one-liner that literally just flips the interval. 🤯

Oh wow okay this is starting to click!! So the interval type is what makes everything work — paths are actual functions, not abstract tokens of equality that you can only eliminate via J.

But I still don't quite get how this gets you univalence as a theorem rather than an axiom. Like... the whole point of univalence is that equivalent types are equal, right? How does having an interval type magically prove that? There must be more going on?

Also — what are these "Glue types" I've seen mentioned? And what's the difference between CCHM and CHM? I've seen both and have no idea if they're different things or the same thing abbreviated differently. 😅

Great questions! Let me address both.

Glue types and how univalence becomes provable

Having the interval alone isn't enough for univalence — you need a way to "glue together" different types along an equivalence. Enter Glue types. The rough idea: given a type A and a partial equivalence T ≃ A defined on some "face" of the cube, you can construct a new type that equals A on one side but looks like T on the other.

So univalence (ua) is literally a definition using Glue, not an axiom you postulate!

CCHM vs CHM — the acronym zoo 🦁

So when someone says "Cubical Agda uses CCHM," they mean the underlying theory. When they say "it follows CHM for HITs," they mean the specific decomposition that makes the HIT schema work.

Adding some context on why canonicity matters practically, because I think this point is undersold.

In Book HoTT with univalence as an axiom, you can write a proof that some function f : ℕ → ℕ satisfies some property — but if your proof uses the univalence axiom somewhere in the chain, the proof term is stuck. Your proof assistant can't reduce it. You can't extract computational content from it. It's a mathematical proof, but not a program.

Cubical TT addresses this by making univalence compute. Cubical type theory provides a novel representation of equality proofs that gives computational content to univalence, making it possible to constructively transport programs and properties between equivalent types.

A concrete example: In Cubical Agda, if you have Bool ≡ Bool via the negation equivalence (swap true and false), you can transport the proof true ≠ false along this path and it will actually compute to false ≠ true. In Book HoTT with an axiom, that transport is stuck.

Let me make a direct comparison table since OP asked about Book HoTT vs Cubical. This is the thing that confused me for a long time too:

The tradeoff: cubical is computationally richer, but the path type doesn't have J computing definitionally, which can make some proofs that rely on pattern-matching on identity proofs slightly more awkward. In practice the Cubical Agda library provides both, and most people use path types.

There's also a HoTT-UF.agda compatibility layer in the agda/cubical library that provides the standard Book HoTT interface but implemented with cubical primitives under the hood — best of both worlds for migration!

Okay I changed my avatar from scared cat to happy cat because I'm actually understanding this 😸

The table from PathsAllTheWayDown is really helpful. One more question: what's the actual relationship between CCHM cubical and Cartesian cubical type theory? I've also seen "RedTT" mentioned somewhere. Are there like... multiple competing cubical type theories?

And should a beginner just dive straight into Cubical Agda, or is there a better starting point?

Yes, there are several competing (and complementary) cubical type theories! The differences lie mostly in what cube category you use and what filling operations you have. Here's a quick tour:

Where to start? My recommendation:

1. Install Agda + the agda/cubical library from GitHub
2. Read the Cubical Agda docs — they're surprisingly gentle
3. Try the lecture notes from Anders Mörtberg's cubicaltt hands-on introduction (HoTT blog, 2017)
4. Start by proving things like funExt, sym, cong cubically — it'll click fast
5. Then try the circle S¹ as a HIT and compute π₁(S¹) ≅ ℤ

The 1lab is also a fantastic modern cubical Agda library with great documentation — highly recommend poking around there.

Perfect thread. Let me give a TL;DR for anyone finding this later:

@CubeScared you're clearly already thinking about this the right way. Fear not the cubes — they are your friends! 🧊🐱

Welcome to the cubical side. We have refl on everything.