Identity Types in HoTT vs. Book HoTT vs. Cubical — what's the actual difference?

ok so I keep seeing these terms thrown around and honestly I need a definitive thread about this. Like we have:

• Id — the Martin-Löf identity type (inductive family, J eliminator)
• Path — cubical path types (maps out of an interval)
• PropEq — the thing Agda calls _≡_ (also Id basically??)
• Book HoTT style — whatever the HoTT Book does
• Cubical HoTT — Cubical Agda / CCHM / etc.

Are these literally the same type? Are they equivalent but not definitionally equal? Does it matter which one I use? I'm so confused nya~~

Like I can see in Cubical Agda there's Cubical.Core.Id for "identity type" and also Path from the cubical primitives, and they're both there but apparently different?? The docs even say something about this but I find it really confusing.

Specific questions:
1. What is the fundamental definitional difference?
2. Why does cubical have BOTH Id and Path?
3. Is PropEq in vanilla Agda the same as Id in HoTT? Or Book HoTT?
4. What does univalence have to do with all this?
5. What is PathP??

Please someone who actually understands this stuff give me a good explanation 🙏 gonna make tea and wait nya~

OK perfect question, let me give the big picture first and then go deep nya~

THE FUNDAMENTAL SPLIT: Inductive Id vs. Path Types

Martin-Löf Identity Type (Id / PropEq): This is the OG. The identity type is introduced as an inductive family with one constructor (refl), and everything follows from the J eliminator. This is what standard MLTT has, what the HoTT Book uses as its formal foundation, and what vanilla Agda's _≡_ is.

Cubical Path Types: Completely different animal. In cubical type theory, maps out of an interval primitive are used to define cubical path types, rather than the inductive family of Martin-Löf identity types. A path from a to b in type A is literally a function I → A where I is an abstract interval.

The correspondence is taken very literally in Cubical Agda: a path in a type A is represented like a function out of the interval, I → A. This is the core philosophical shift.

(continuing my previous post, hit the char limit)

So why does Cubical Agda have BOTH?

Good question! Cubical Agda has Path (the native cubical type) and also Cubical.Core.Id (the identity type defined using cubical primitives). The cubical identity type and the path type are equivalent, so all of the results for one can be transported to the other one (using univalence).

The reason both exist is ergonomics. The Id type in Cubical Agda supports J and pattern matching on refl (which J-encoded proofs rely on), but the native cubical Path type is much nicer to work with interactively because you can define proofs using lambda notation.

For example with Path types you can directly compose paths, apply them, and use them in function extensionality proofs without needing combinators. With Id you're stuck doing everything through J.

The official recommendation in Cubical Agda is: "use the cubical identity types unless you really need J to compute on refl."

wait so in Coq/vanilla Agda when I write Prop or eq or _≡_ that's just the inductive family Id type right? And it's basically what "Book HoTT" uses?

And the whole point of going cubical is to make univalence actually COMPUTE instead of just being an axiom that's stuck?

I feel like that's the crux of it but maybe I'm missing something

Exactly! You've got the core insight. Cubical type theory is a version of homotopy type theory in which univalence is not just an axiom but a theorem, hence, since this is constructive, has "computational content."

In Book HoTT, the situation is:

In Cubical Agda:

So the practical payoff is: transporting along the path that we get from applying ua to an equivalence is hence the same as applying the equivalence — but in cubical this is a definitional equality, not just propositional. Your proofs can actually compute nya~

Also this is why function extensionality is a theorem in cubical rather than an axiom: function extensionality is a theorem in cubical type theory, rather than an axiom as is the case in Martin-Löf type theory.

Let me add the "Book HoTT vs Cubical" framing more explicitly because I think that's the confusion OP is having:

Book HoTT (first generation HoTT):

Cubical Type Theory (second generation HoTT):

The big philosophical difference CubicalCat didn't mention: in Book HoTT, operations such as transport and path composition are defined by induction on the paths; thus they reduce when the paths are reflexivity, but are stuck otherwise. However you CAN prove they reduce typally based on the form of the type.

Cubical flips this: the type-based reductions become judgmental, while the path-based ones become merely propositional. So it's not that cubical is strictly "better" — it makes different tradeoffs!

OK wait that's actually a really cool way to put it. So it's not like cubical is just "strictly better" — it's making a different design choice about WHICH equalities are definitional?

but then my brain short-circuits: if Path and Id in cubical are equivalent (via univalence I guess?) does that mean using either one is "equally valid" for formal proofs? or does the distinction show up in extracted computation?

also you mentioned PropEq in vanilla Agda — that IS the Id inductive family right? just with different notation? I always assumed it was the same thing.

For formal mathematical content: yes, they're equivalent. But for computational purposes: not really.

Think of it this way. Path types in cubical have rich definitional equalities that let proofs actually reduce. Id types (even in cubical) only reduce when you pattern-match on refl. So if you want your extracted programs to compute nicely, you use Path.

There's actually a really nice quote from the Cubical Agda interface that captures this — when they wrap cubical primitives in the Book HoTT style interface, they note that "pattern matching on refl is not available" for the identity type, and you have to use J instead. That's the cost.

As for PropEq in vanilla Agda: yes, _≡_ in standard Agda (without --cubical) is exactly the inductive family identity type. One constructor refl, J eliminator, the whole deal. Same as Book HoTT's Id. The difference is just spelling/notation.

The big difference: in vanilla Agda + HoTT axioms, you're working with stuck terms — ua and funext are postulates that never reduce. In cubical Agda, this gives an axiom-free version of HoTT/UF which computes properly.

Concretely: if you transport a monoid structure along ua of some equivalence, in vanilla HoTT+axioms the resulting operation is stuck. In cubical it actually reduces to the expected operation on the new carrier. That's huge for doing actual verified computation!

Nobody answered OP's question 5 about PathP yet! Let me do that nya~

PathP: heterogeneous path types / path-over types

PathP is a heterogeneous path type. The "P" stands for "path-over" — it's a path that lives over a line of types (a function I → Set). So if you have a path p : A ≡ B (a path between types) then PathP (λ i → p i) a b is a path from a : A to b : B that "lies over" the type path p.

This generalizes the HoTT Book's notion of "path-over" or heterogeneous equality. These non-dependent path types are supposed to correspond to the identity types of HoTT/UF while PathP is a cubical version of the "path-over" types of HoTT, that is, paths living over a line of types.

Why is this useful? Because when working with HITs (higher inductive types), your path constructors often go between terms of different types (or at least types that vary over a dimension). Having built-in PathP is extremely handy — you don't need JM (John Major equality) or other heterogeneous equality hacks from vanilla type theory.

Can I throw in the "practical choice" angle? Because I think there's also a "which should I actually use" dimension here that OP probably cares about:

There are actually good reasons to keep using Book HoTT style (Id type + axioms) even if you know cubical:

Reasons to go cubical:

Honestly for most practical Agda work I see people using Cubical Agda now, but the HoTT Book+axioms style is still the lingua franca for communicating ideas.

Real nerd moment: nobody's mentioned the third generation stuff yet (Shulman's H.O.T.T. / Higher Observational Type Theory)!

The generations go roughly:

The cubical approach has a philosophical cost: cubical type theories achieve computational univalence only by adding syntax for auxiliary/spurious interval types with rewrite rules which encode technical detail that has no abstract motivation — the interval I isn't really a "type" in the traditional sense, it's an exo-type that leaks into the theory.

H.O.T.T. tries to get the computational benefits without the interval machinery. Still work in progress but really exciting stuff! Check out the HOTT thread for more.

OK let me try to write a summary of what I've learned from this thread so far before more replies come in (this blew up fast?? 84 replies already??)

Thank you all so much!!! This is exactly what I needed nya~ 🦊💜 going to install Cubical Agda tonight

still following the thread though because I'm sure someone will bring up XTT or cartesian cubical or something and blow my mind again lmao