What is meant by the inverse function theorem in algebraic geometry? I heard several times the inverse function theorem fails in algebraic geometry. Now I realize I'm pretty confused by this. This question has two parts. The first part asks for the correct formulation of synthetic inverse function theorems. The second asks for clarifications and intuitions about Penon's paper.
Detailed references would be much appreciated - I only know about Kock's two texts, Lavedhomme's book, and Kostecki's notes on SDG and these do not discuss these things, and I don't know the algebraic geometry literature well enough to find this stuff...
Apologies if this is all too elementary!

Part I
In Synthetic Geometry of Manifolds, Kock writes the inverse function theorem takes us "from infinitesimal invertibility to local invertibility", which sounds morally right.


*

*For "local invertibility" I can only think of one interpretation - $f$ étale at a point $x$ implies an open $U\ni x$ such that $f|_U$ is an isomorphism.

*For "infinitesimal invertibility" I can think of two options:


*

*(2a) the usual unique lifting property against infinitesimal neighborhoods;

*(2b) the differential $\operatorname{d}_x\!f$ being an isomorphism at all points.



I'll go with the second option trying to parallel classic differential geometry.
Following Kock's words, am I right to call the following condition "an inverse function theorem"?
Condition IFT1. (2b)$\implies$(1).
Or is this the wrong idea completely?
Also, is the Henselian property all about the implication (2a)$\implies$(1)?
I ask because of the following excerpt from section 2.3 of Néron Models, which, at least for schemes over fields, seems similar.

Let $R$ be a local ring with maximal ideal $\mathfrak m$ and residue field $k$. Let $S$ be the affine (local) scheme of $R$, and let $s$ be the closed point of $S$. From a geometric point of view, Henselian and strictly Henselian rings can be introduced via schemes which satisfy certain aspects of the inverse function theorem.
Definition 1. The local scheme $S$ is called Henselian if each étale map $X\to S$ is a local isomorphism at all points of $X$ over $s$ with trivial residue field extension $k(x)=k(s)$. If, in addition, the residue field $k(s)$ is separably closed, $S$ is called strictly Henselian.

Also, for a morphism $f:X\to S$ for schemes, $f$ is smooth at $x$ iff it's étale-locally a projection, i.e there's an open neighborhood $U\ni x$ such that $f|_U$ factors through an étale morphism followed by a canonical projection from $\mathbb A_S^n$. Replacing smooth with étale looks like an implicit function theorem and I think this is precisely what is meant by the Henselian property over a field. Is this correct, or is some other notion of "local isomorphism" is meant in the excerpt above?

Part II
This paper by Penon formulates a synthetic inverse function theorem and moreover claims that a morphism of equidimensional varieties is étale in several equivalent senses iff it satisfies the usual synthetic definition - the square below is a pullback. $$\require{AMScd} \begin{CD} TM @>{df}>> TN\\ @VVV @VVV\\ M @>>{f}> N \end{CD}$$
I don't read French and I can't make much sense of the pullback square he describes, but I know it only involves infinitesimal objects. Hence, it seems Penon's paper couldn't possibly address "local invertibility" in the sense of open neighborhoods. If so, what's the point of the paper? Note his notion are  also used in this paper by Marta Bunge.
Added. Here's Penon's Thesis. Again, from what I can make out, there's no mention of neighborhoods in the local context.
 A: Penon's thesis "De l'infinitésimal au local" is often cited in this context. A rough overview of some things he does there (which I got from skimming through):


*

*He defines the infinitesimal nbhd of $x_0\in X$ to be all $x\in X$ such that $\neg \neg (x=x_0)$ on p.51. (I'm assuming there's a typo when he defines $\neg \neg \{x\}$, it should probably read $x'\sim x$, not $x' \neq x$.)

*He says $f:X\to Y$ is infinitesimally invertible at $x_0\in X$ if the restriction of $f$ to the infinitesimal nbhds of $x_0$ and $f(x_0)$ is bijective (p. 52).

*On p. 59 he shows that infinitesimal invertibility is equivalent to bijectivity of the tangent map under certain assumptions.

*He defines intrinsic (local) nbhds of $x_0$ on p. 84 to be subset $V\subset X$ s.t. $\forall x\in X \colon (\neg(x = x_0)\vee x \in V)$. Penon translates this into everyday language as "$x$ is discernible from $x_0$ or it is in V".

*He calls $f:X\to Y$ locally invertible at $x_0\in X$ if there exists an intrinsic nbhd. $V \subset X$ of $x_0$ s.t.  $f(V)$ is an intrinsic nbhd. of $f(x_0)$ and $f|_V$ is injective. Here $f|_V$ is the restriction of $f$ to $V$. This is on p. 92.

*On p. 125 he proves that infinitesimal invertibility implies local invertibility for spaces that are opposites of finitely presented smooth rings. This seems to be inverse function theorem.


Hope this helps for the first part of the question. I haven't read the other paper by Penon.
You might also be interested in an upcoming book in english by Bunge "Synthetic Differential Topology", although a quick search only gave me a place where the inverse function theorem is used, no statement of it.
