I'm a computer scientist, not a mathematician, so apologies if I've messed up a lot of things greatly.

I've been reading about synthetic differential geometry, and trying to formalize it in Coq. While dealing with the axiomatic specification is quite pleasing, actually constructing a (computable / effective) model of this seems frightfully hard.

The simplest model that I could find comes from Differential Geometry in Toposes: Ryszard Paweł Kostecki is $\mathbf{Set}^{\mathbb R- \mathbf{Alg}}$: That is, functors from $\mathbb R$ algebras to $\mathbf{ Set}$. This is quite painful to formalize within Coq, and at the end, I don't think what's left will be computable (since the reals are not computable)

My questions are (in descending order of importance)

How do I get a computable model of SDG, in the sense that, I should at the end of the whole process be abel to use a computable version of (say) the derivative operator within Coq. Is this possible? If yes, what model of synthetic differential geometry is this?

Does restricting to the case of

*discrete*differential geometry make life any easier for me? Is there a study of "synthetic discrete differential geometry"?

**EDIT**: adding more details about what I'm looking for

I know that one can impement differentiable programming languages by using implementations of automatic differentiation. There's a categorical interpretation to this, for example, see The simple essence of automatic differentiation.

What I'm looking for is a way to perform computational differential *geometry*. So, not only do I want to be able to be able to calculate the *value* of $f'(x_0)$ at a given $x_0$, I want to be able to compute the differential of $f$ *as a computable function*. So, for example, I want there to exist an operator $d: (f : M \rightarrow N) \rightarrow (T_x M \rightarrow T_{f(x)}N)$.

Ideally, I want this setup such that I can:

- prove things about the operator $d$ within the axiomatic system as laid out by SDG (in Coq).
- Create a computable model that satisfies those axioms (implement the axiomatic system in Coq)
- Finally, extract out runnable Haskell / OCaml code that allows computable access to things like the differential map $d$, such that when I feed it in $f(x) = x +2$, I should get $d f \equiv 1$ ($\equiv$ reasoning between equality of functions extentionally).

I don't know if this is too much of an ask, or indeed, a coherent ask. The goal really for me is to have a verified, computable differential geometry (or at least, discrete differential geometry) library, with proofs that can be done *easily*, which is the whole point of SDG.

Cartan Geometry in Modal Homotopy Type Theoryby Wellen. $\endgroup$ – David Roberts Nov 19 '19 at 12:35