1
$\begingroup$

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

$\endgroup$

1 Answer 1

3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

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