$\DeclareMathOperator\Sh{Sh}$Informally, a [quasi-excellent ring][1] is a Noetherian ring with a few technical extra regularity conditions that make it turns out to be the largest class of rings that allow for all singularities to be resolved. It is excellent if it is also catenary.

Is there a constructive definition of this property? This is a fairly natural question to ask where one would be tempted to conjecture that there is one, because resolution of singularity is a geometric concept that you can expand to relative schemes, and in that case you would be led to the conjecture that a relative affine scheme over $S$ has no singularities if it can be viewed generated by an excellent ring in the [internal language][2] of $\Sh(S)$. 

In general however, the internal language of $\Sh(S)$ does not satisfy the law of the excluded middle, which is slightly annoying because unlike more natural notions like coherence, Noetherian rings are notably less well behaved constructively and split into several non-equivalent definitions that are classically equivalent. Is there a definition of quasi-excellent rings that constructively captures the geometric intuition?


  [1]: https://en.wikipedia.org/wiki/Excellent_ring
  [2]: https://arxiv.org/abs/2111.03685