I am curious if (any of) the various inequivalent constructions of the real line in constructive mathematics can be used to build a model of Kock and Lawvere's synthetic differential geometry? In other words, do any of the constructions of the real line (in say HoTT) satisfy the Kock-Lawvere axiom for a class of functions which deserve to be called smooth? If not, how can we "augment" the real line with nilpotent infinitesimals for this to be true?

I am a complete novice when it comes to constructive mathematics, but I'm reasonably comfortable with Anders Kock's synthetic differential geometry texts. Unfortunately, I haven't had a chance to read the Models of SDG text yet, so I apologize if this is covered there.

propertythat the entire ring satisfies. I think Michael is asking a good question, which I would phrase precisely like this: is there any constructive construction of a ring which (1) produces the Kock-Lawvere line object when interpreted in a standard model of SDG, and (2) produces the classical real numbers when interpreted in classical mathematics? I suspect not, but I don't think I have a proof. $\endgroup$ – Mike Shulman Nov 17 '17 at 4:25