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$.


1 Answer 1


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.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .