FredericPaugam

Sorry, i can't download the article. I was also meaning an entirely constructive approach (without LEM) in the very same spirit, without using prime ideal, but a functorial one. You...

I found the reference on spectral schemes on the web and found it quite nice and concrete. The functorial approach also has some advantages, and seems to me quite adapted...

Thank you for pointing out this synthetic approach. I am not sure that it is directly related but i would be interested to see how it is implemented. There is...

Incidentally, i just realized that the relation with the lattice approach is the following: one would like to prove from what is already in the cubical library that R->Spec(A)(R)=Hom(A,R) is...

I mean that if A is fixed, the functor $Spec(A)=Hom(A,-):D(r)\mapsto Hom(A,R[r^{-1}])$ defined on generators $D(r)$ of the Zariski lattice of any ring $R$ should extend to a sheaf $Spec(A)=Hom(A,-)$ of...