Is Lean's type theory intensional?

Stream: Type theory

[Marcus Rossel]

I was trying to find out what makes a type theory "intensional" and came upon this nLab article, which says:

[...] if the judgmental equality coincides with the identity type, then the former is also extensional, whence the type theory is called “extensional” — while if the two equalities do not coincide, then the judgmental equality has room to be more intensional than the identity type, making the type theory “intensional”.

In the context of Lean, I'm reading judgemental equality as definitional equality and identity type as propositional equality type. Is that right? And if so, does this make Lean's type theory intensional, as propositional equality does not imply definitional equality?

[Arthur Adjedj]

Yes, Lean's type theory is intensional.

[Max Nowak 🐉]

Lean's intensional type theory is conservative over extensional type theory though, since Lean also has UIP and funext.

[François G. Dorais]

I think you mean that extensionality is conservative over Lean's TT, not the other way around.

To say that extensionality is conservative over LeanTT means that every LeanTT + Ext theorem is a LeanTT theorem (with a different and probably much longer proof). To say that LeanTT is conservative over Ext means that every LeanTT + Ext theorem is an Ext theorem, which is not true.

PS: I've never seen a written proof that Ext is conservative over LeanTT.

[Marcus Rossel]

What does the + Ext mean in LeanTT + Ext here? That is, what does Ext add?

[Arthur Adjedj]

PS: I've never seen a written proof that Ext is conservative over LeanTT.

While I'm confident no work has been done to prove that Ext is conservative over LeanTT of all type theories, Hofmann 1995 does present a proof that Ext is conservative over MLTT+funext+UIP. Futhermore, both funext and UIP are provable in LeanTT.

[François G. Dorais]

Arthur Adjedj said:

While I'm confident no work has been done to prove that Ext is conservative over LeanTT of all type theories, Hofmann 1995 does present a proof that Ext is conservative over MLTT+funext+UIP. Futhermore, both funext and UIP are provable in LeanTT.

Yes, I'm aware of Hofmann and that proof does make it plausible that Ext is conservative over LeanTT. I'm merely expressing some "healthy skepticism" since LeanTT derives funext from quotient types and I don't know how quotients interact with extensionality.

[François G. Dorais]

Marcus Rossel said:

What does the + Ext mean in LeanTT + Ext here? That is, what does Ext add?

It's shorthand for making the type theory extensional. Hofmann's paper linked above has all the details...