I am trying to understand bits and pieces of Lawvere's article Continuously Variable Sets; Algebraic Geometry = Geometric Logic. I'm not doing very well.

I know this is a lot to ask, but basically, I would like for someone to explain in more detail the whole construction described at the end of the paper. I was told the idea is to get a "free local ring", which is free simply because of the internal language of the corresponding sheaf topos which makes any ring locally free, but I really don't know what that means and I still don't understand the idea and details of the construction in the paper. I stress that I'm looking for a detailed explanation; I realize that the idea may be encapsulated in a short elegant statement, but I won't be able to decode it..

So... What the hell is going on there? :D