Great, thanks. I linked to it from synthetic differential geometry.

]]>Okay, I wrote something here. Unfortunately I don’t really have the leisure for this at the moment

]]>We have some SDG constructions elsewhere. Worth including here? Something like

]]>A tangent vector field is a section of the map of $X^D \to X$ corresponding to evaluation at 0, so is a map $f: X \to X^D$, such that $f(x)(0) = x$. Uncurrying, this is equivalent to a map $f^{\ast}:X \times D \to X$, with $f^{\ast} (x, 0) = x$. Currying the first variable yields a map $D \to X^X$, i.e., to the group of diffeomorphisms of $X$.

The term “flow of a vector field” used to redirect to *exponential map*, which however is really concerned with a somewhat different concept. So I have created now a separate entry *flow of a vector field*.