The Kock-Lawvere axiom for a topos $\mathcal{E}$ states that given a specified commutative ring object $R \in \mathcal{E}$, for all local Artinian $R$-algebra objects $A \in \mathcal{E}$, the morphism


$$A \to R^{\mathrm{Spec}\_R(A)}$$


is an isomorphism.


Now, we don't assume that the Kock-Lawvere axiom holds for the topos $\mathcal{E}$. Assuming that in the topos $\mathcal{E}$ one could define the power series ring $R[[\epsilon]]$ of $R$ as the inverse limit of the local Artinian $R$-algebras $R[\epsilon]/(\epsilon^n)$ and the formal spectrum $\mathrm{Spf}(R[[x]])$ of $R[[\epsilon]]$ as the inductive limit of the spectra $\mathrm{Spec}(R[\epsilon]/(\epsilon^n))$, is it consistent to assume that the morphism


$$R[[\epsilon]] \to R^{\mathrm{Spf}(R[[\epsilon]])}$$


is an isomorphism?



Analogue of Kock-Lawvere axiom for power series rings?
Yes, it is consistent, it even follows from the Kock-Lawvere axiom, as follows.


We defined $\mathrm{Spf}(R[[\epsilon]]) := \mathrm{colim}\_n \mathrm{Spec}(R[\epsilon]/(\epsilon^n))$, so we have
$$R^{\mathrm{Spf}(R[[\epsilon]])} = R^{\mathrm{colim}\_n \mathrm{Spec}(R[\epsilon]/(\epsilon^n))} = \mathrm{lim}\_n R^{\mathrm{Spec}(R[\epsilon]/(\epsilon^n))}$$
by the universal property of the colimit. By the Kock-Lawvere axiom we have $R^{\mathrm{Spec}(R[\epsilon]/(\epsilon^n))} = R[\epsilon]/(\epsilon^n)$, so we get exactly $\mathrm{lim}\_n R[\epsilon]/(\epsilon^n)$, which is how we defined $R[[\epsilon]]$.


(However, I might misunderstand you question. Do you ask for a topos where the Kock-Lawvere axiom *does not* hold but the morphism in question is still an isomorphism?)


