 Coherent theory of local rings

Use the signature of unital commutative rings, its equational axioms, and the coherent sequents $0=1⊢\perp$ and $\top {⊢}_x\mathrm{Inv}(x)\vee \mathrm{Inv}(1-x)$, where $\mathrm{Inv}(x)$ abbreviates $\exists y(xy=1)$. In a set-based model the nonunits form its unique maximal ideal; this is the usual nonzero local ring. In a topos the disjunction expresses local existence of a unit witness. Its classifying topos is defined by the Zariski coverage on finitely presented rings.