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.