In intensional MLTT, are a function and its lambda abstraction propositionally equal?

Question

Suppose $f \in \Pi_{x \in A}B(x)$, can I derive a proof term $p \in \mathrm{Id}_{\Pi_{x \in A}B(x)}(f,\lambda(x \in A).f(x))$? In general, if I have a proof term for $g(x)=f(x) [x\in A]$, how can I derive $p \in \mathrm{Id}_{\Pi_{x \in A}B(x)}(f, g)$? I know both equalities are false if we ask for definitional (i.e. intensional) equality.

Answer 1

Neither of these are provable, depending on which specific intensional type theory you're using. Indeed, one might say that "intensional type theory" is so named because the propositional equality is intensional, not just the judgmental/definitional equality (although I don't know for certain whether that's historically accurate).

The first property you mention is $η$ (eta) equality. It's not uncommon for it to be added to the judgmental equality of a type theory, because it is convenient and there are still strategies for deciding the judgmental equality with it around. But I think it would usually not be considered part of the 'computational' behavior of the terms like $β$ is. I'm not sure if any presentation of intenstional type theory by Martin-löf himself included the $η$ rule, but it wouldn't surprise me, and I'm fairly sure that he gave presentations without $η$.

The second property is extensional equality of functions. Historically it's not included in intensional type theory, because that's what extensional type theory was for, I believe. You also can't add it to the judgmental equality without breaking its decidability, which requires you to take a different approach in a proof assistant than the usual intensional type theory approach. A fair amount of work was done on how to add it as an 'axiom' (without getting stuck) under the name Observational Type Theory. However, that work never saw any 'mainstream' implementation to my knowledge. But, the recent interest in homotopy and cubical type theory has given rise to implementations of intensional-like type theory that admit proving extensional equality propositionally. And for instance this paper shows how to step back into something more like OTT was, but presented in the new cubical way.