Intensional vs Extensional Equality 🔒 Locked

Okay so I keep seeing this conflation between intensional equality and extensional equality everywhere (including in some recent proof-assistant discourse on the birdsite) and I want to lay it out carefully for once. Let's have a proper technical thread.

Quick framing: in intensional type theory (the kind Lean 4, Rocq/Coq, and Agda use), the identity type Id A a b (or a = b) is an inductively defined type family. It's inhabited only by refl up to definitional equality, and you interact with it via the J eliminator (path induction). Critically, propositional equality is not the same as definitional/judgmental equality.

-- Lean 4: the Id type is inductive
inductive Eq {α : Sort u} : α → α → Prop
  | refl : (a : α) → Eq a a

-- J eliminator / path induction
theorem J {α} {a : α} (P : ∀ (b : α), a = b → Prop)
    (h : P a rfl) : ∀ {b} (p : a = b), P b p := ...

In extensional type theory (ETT), you add the equality reflection rule: if you have a proof p : a =_A b, then a and b are definitionally equal. This collapses propositional and judgmental equality into one.

The cost is steep: type checking becomes undecidable in ETT. NuPRL is the classic example of a proof assistant based on this design — it uses meaning explanations instead of a decidable type checker. Most modern proof assistants deliberately avoid ETT for this reason.

I think there are real tradeoffs here worth discussing. What does the forum think? Are there situations where ETT's convenience outweighs the undecidability cost?

Wonderful, I've been waiting for this thread. Let me add the HoTT angle since neither of you have fully gone there yet.

The really beautiful thing about intensional type theory — precisely because propositional equality is separate from definitional equality — is that identity types have room to be interesting. In HoTT / Univalent Foundations, identity types are interpreted as path spaces. The type a = b is not merely a proposition, it's a space of paths from a to b.

This is exactly what breaks under ETT. The reflection rule forces a = b to always be a proposition (h-level 1, a set in HoTT terms). ETT is fundamentally incompatible with univalence because the universe itself would need to be an h-set, killing all higher structure.

-- HoTT-Agda style: loop space of the circle is ℤ
-- This only makes sense if Id types can be non-trivial!
S¹ : Type    -- higher inductive type
base : S¹
loop : base = base    -- nontrivial path!

-- In ETT with reflection, loop would be forced = refl
-- The circle collapses to a point. That's the murder of topology.

So the question "should we use ETT?" is partly the question "do you want to do synthetic homotopy theory?" If no, ETT might be fine for setoid-level math. But you're giving up something profound.

I partially agree but let's be precise: "setoid hell" is partly an artifact of specific proof assistants, not an inherent property of intensional type theory. Cubical Type Theory (CTT) is intensional in the relevant sense — no reflection rule — but gives you computational univalence, so function extensionality and many quotient-type operations just hold by computation.

Agda's cubical mode makes a lot of the traditional setoid pain go away. You get HITs, you get proper quotients, you get function extensionality — all without the reflection rule and without sacrificing decidability of type checking.

-- Cubical Agda: integers as a HIT (ℤ without setoid hell)
data ℤ : Type where
  pos  : ℕ → ℤ
  neg  : ℕ → ℤ   -- neg 0 = pos 0 via path constructor
  posneg : pos 0 ≡ neg 0

-- no quotient noise; equality is baked into the type

So "ETT to escape setoid hell" is a solution to a problem that CTT solves better, without the undecidability cost.

That's a massive mischaracterization. The people working on NuPRL and Nuprl-style systems were not "giving up" — they had a coherent philosophical position rooted in Martin-Löf's meaning explanations. The idea that propositional equality should collapse into definitional equality if you have a proof of it is a defensible semantic position, not incompetence.

I think ETT is a bad choice for foundational tools for specific technical reasons — undecidability of type checking being the main one. Not because its practitioners are cognitively deficient. This kind of rhetoric makes people defensive and turns a technical conversation into a status contest.

I defended the intellectual tradition behind ETT while calling the specific design choice bad for engineering, which is a completely coherent position. These are not the same thing. If you can't read at that level of resolution, maybe formal logic isn't for you.

And "nobody uses NuPRL" is a red herring. By that logic, nobody uses Agda either compared to Python. Usage numbers don't determine semantic correctness.

Let's get back on track. I want to address something that came up in the omitted posts: the claim that "Observational Type Theory is just ETT with extra steps."

This is wrong. OTT (Altenkirch-McBride) keeps propositional equality separate from definitional equality. It's very much in the intensional family. What it does is provide a computational characterization of propositional equality by structural induction on types, so you get things like functional extensionality and propositional extensionality by construction — no reflection rule, no undecidability.

-- OTT: equality is defined by induction on type structure
-- Eq : (A : Set) → A → A → Prop
Eq (A → B) f g  =  ∀ x, Eq A x x → Eq B (f x) (g x)
Eq (A × B) p q  =  Eq A (fst p) (fst q) × Eq B (snd p) (snd q)
-- Functions: equal if pointwise equal. Extensionality for free!
-- But Eq is always a proposition. No higher structure.

Setoid Truncated Type Theory (SETT), Quotient Inductive Types (QITs), and the whole Observational spectrum all live in the intensional camp. The line is the reflection rule. It's really one of the most semantically meaningful single rules in all of type theory.

I started this thread to discuss intensional vs extensional type theory and it is turning into a Lean vs Rocq culture war. Can we please not do this.

I used Rocq as an example in #4 because I was working in Rocq at the time, not because Rocq is uniquely bad. I use Lean 4 too. They both have their annoyances. Both are fine proof assistants. The setoid story in Lean 4 is better due to Quotient and typeclass automation, but neither is free of propositional equality overhead in the general case.

Can we return to the actual topic: the reflection rule, its consequences, and whether there are meaningful use cases for ETT in 2025?

Okay. Attempting to salvage the technical content. Let me summarize the actual dichotomy cleanly since it got buried:

Intensional TT (ITT): Definitional equality (≡_def) and propositional equality (a = b) are distinct. Type checking is decidable. Identity types can have higher structure (HoTT). Function extensionality is an optional extra axiom or follows from computational rules (CTT). Used by: Lean 4, Rocq, Agda, all Cubical systems.

Extensional TT (ETT): Adds equality reflection: p : a = b ⊢ a ≡_def b. Propositional and definitional equality collapse. Type checking becomes undecidable. Function extensionality and quotients are "free" but at the cost of decidability. Used by: NuPRL (historical). Incompatible with HoTT/univalence.

The interesting modern space is the various middle grounds: OTT, 2LTT, Quantitative Type Theory, XTT (which has the reflection rule restricted to a strict equality type separate from the HoTT identity type). These try to get the ergonomic wins of ETT without losing decidability.

I think that's the real answer to EqEqEq's original question: nobody chooses raw ETT in 2025. The active research is in finding carefully limited extensionality principles that preserve the good properties of ITT.

admin-nyanko please just lock this thread at this point. TypeNihilistKat and UnivalentUnicorn wrote genuinely good technical content in posts #90 and #91 and that's probably the best summary this thread will produce. Everything since post #92 has been pure entropy.

I'm sorry for starting this. I thought we could have a nice technical discussion. I was naive.