Funnily, in programming languages based on Martin Lof Type Theory, the topic of function extensionality is a whole rabbit hole for reasons other than the haltin

Funnily, in programming languages based on Martin Lof Type Theory, the topic of function extensionality is a whole rabbit hole for reasons other than the halting problem. There is a distinction between intensional Martin Lof type theory and extensional Martin Lof type theory, which differ in their treatments of equality. First, one must distinguish between judgmental equality x = y, which is a statement in the mathematical metalanguage that two terms are equal, and propositional equality, which "internalizes" judgmental equality within the programming language through the equality type Id(A, x, y), the type of proofs that x and y are judgmentally equal. In extensional type theory, judgmental equality also follows from propositional equality, and together with the eta-conversion rule for functions, function extensionality is provable [0]. However, typechecking extensional type theory is undecidable [1]. Alternatively, in Homotopy Type Theory (HoTT), supports function extensionality is provable from the univalence axiom, which states that isomorphic types are equal [2]. Function extensionality is trivially provable in Cubical Agda [3], which gives a computational interpretation of HoTT's notion of equality. [0] https://cstheory.stackexchange.com/questions/46331/extensional-type-theory-and-function-extensionality/46342#46342 https://cstheory.stackexchange.com/questions/46331/extension... [1] https://cs.stackexchange.com/a/112559 https://cs.stackexchange.com/a/112559 [2] https://ncatlab.org/nlab/show/function+extensionality#relation_to_the_univalence_axiom https://ncatlab.org/nlab/show/function+extensionality#relati... [3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.html https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...