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/extension...
[1] https://cs.stackexchange.com/a/112559
[2] https://ncatlab.org/nlab/show/function+extensionality#relati...
[3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...