Hello,

I have recently been toying with the idea of doing nonstandard analysis in Coq, and I’m running into an issue. I can construct the hyperreals using ultrapowers (I use nonconstructive axioms so the use of Zorn’s lemma is perfectly fine to me), but I have no idea how to even state the transfer principle. The usual statements involve logic and model theory, but Coq uses its own foundations so I find it difficult to use the usual formulations of the transfer principle in Coq. I feel like I would want to have some kind of definition that would take propositions to their hyperreal variant, but I have no idea how that could even be done. I could maybe manage by just manually utilizing the properties of ultrapowers, but that seems to be removing most of the power of nonstandard analysis, since the transfer principle is so vital to it.

So my question is, is there some way of formulating the transfer principle in NSA in Coq? Or maybe, something similar that produces a similar result?