# Does microaffineness imply function extensionality?

I am currently working through Bell's Primer of Infinitesimal Analysis. Because constructive math (in the sense of Martin-Löf Type Theory) does not have function extensionality, I wondered whether it follows from microaffineness. Bell defines microaffineness as:

For each function $$g:Δ → R$$, there is a unique $$b$$ in $$R$$ such that $$g(ε) = g(0) + bε$$ for all $$ε$$ in $$Δ$$,

where $$Δ$$ is the part of all $$x$$ such that $$x² = 0$$. Bell never mentions function extensionality, but liberally talks about things like the derivative function. Can extensionality be proved in the context of smooth infinitesimals? I am especially sceptical because microaffineness is only for functions defined on $$Δ$$, not on all of $$R$$.

Bell never mentions function extensionality because he does not work in Martin-Löf Type Theory. Instead, he works in the local set theory of a topos, where function extensionality is always a theorem, without any assumptions (you can find a proof e.g. here). This answers your question as stated: yes, extensionality can be proved in the usual context of smooth infinitesimals.

That's nice, but what happens if we do Smooth Infinitesimal Analysis by extending MLTT with a smooth real line $$R$$, appropriate ring operations on $$R$$, and an inhabitant $$\texttt{kl}$$ for the propositions-as-types version of the Kock-Lawvere axiom? [1]

First of all, you seem to be under the impression that referring to the derivative of a function would be precluded by the lack of function extensionality. This is not so: we can use the term $$\texttt{kl}$$ to define another term $$\texttt{der}: R^R \rightarrow R^R$$ which assigns to each function $$f: R \rightarrow R$$ the canonical derivative function $$\texttt{der}\:f$$ of $$f$$. Whenever we reference the derivative of $$f$$, we actually reference $$\texttt{der}\:f$$, a unique and well-defined object. The lack of extensionality causes no issues at all. Of course, $$\texttt{der}$$ will assign extensionally equal $$\texttt{der}\:f_1$$ and $$\texttt{der}\:f_2$$ to extensionally equal $$f_1$$ and $$f_2$$ (and provably so).

Does this extended MLTT/SIA prove function extensionality? I'll take a bold stance and suggest, without proof, that it almost certainly does not.

I don't see anything that would block the integration of the usual Dialectica models refuting function extensionality with presheaves on loci, as outlined in the Moerdijk-Reyes book, to create a model for MLTT/SIA. Such a model would not be well-adapted, of course, but it would refute function extensionality. However, as always, the devil is in the details. Digging into the specifics might reveal some obstacles that I can't see when I just sketch the construction and although I could probably tackle these intricacies, I strongly prefer not to. So I guess I'll leave this as a conjecture for now, although I doubt there will be any individuals motivated to put in the effort to settle it.

[1] aside: I think I was the first to actually do this, in Péter Diviánszky's Agda course module in 2012. Using the then-fresh reflection capabilities, I even developed a rudimentary ring solver that could apply the KL axiom; IIRC Mátyás Manninger and I planned to develop it further that summer, but we never got around to it, and sadly, the whole library is now lost.