Synthetic differential geometry and formally étale morphisms?

Question

Upon looking throug Kostcki's synthetic differential geometry notes, I stumbled upon the following definition. (Here $R$ is the geometric line, $W$ is a Weil algebra, and $\operatorname{Spec}_RW$ is the set of $R$-points of (the scheme associated to) $W$).

Definition 8.10. An arrow $f:M\rightarrow N$ between two objects is formal étale if for any small object $\operatorname{Spec}_RW$ and the canonical map $$1\overset{0}{\rightarrow}\operatorname{Spec}_RW$$ called the base point of the small object, the square below is a pullback.

$$\require{AMScd} \begin{CD} M^{\operatorname{Spec}_RW} @>{f^{\operatorname{Spec}_RW}}>> N^{\operatorname{Spec}_RW}\\ @V{M^0}VV @VV{N^0}V\\ M^1 @>>{f}> N^1 \end{CD}$$

1. What is the geometric intuition behind this definition?
2. How is this definition related to the usual definition of formally étale in algebraic geometry?

Answer 1

1. The geometric intuition comes from tangent spaces. In that case, the canonical base point is simply zero, and the pullback square is $$\array{ T X &\stackrel{d f}{\to}& T Y \\ \downarrow && \downarrow \\ X &\stackrel{f}{\to}& Y. }$$ The fact it's a pullback then says the tangent vectors to $X$ are in bijective correspondence to the tangent vectors on $Y$ with basepoints in the image of $X$. The correspondence is given by composing $f$ on a tangent vector. Moreover, by pullback pasting, this implies $df:T_xX\cong T_{f(x)}Y$ so intuitively being formally étale means that locally you are a diffeomorphism.
2. The connection is that the pullback definition is equivalent to the general unique filler diagram in the category of sets, and in any elementary topos, which is where SDG usually takes place.

I asked about the proving formal étaleness from $df:T_xX\cong T_{f(x)}Y$ here.