Gabriel-Zisman localization in formalized mathematics has been studied by Carlos Simpson.

]]>Good! Let us know how you get on.

It seems Voevodsky worked on localization:

]]>To test the applicability of Univalent Foundations to actual formalization of mathematics I wrote a library of formalized mathematics for Coq which developed abstract algebra up to the construction of localization of commutative rings.

I think there is only one way to find out, namely to try it :-), and I hope to do it over the next couple of days (in Cubical Agda).

]]>Kevin Buzzard takes the issue of the identity between $R[1/f][1/g]$ and $R[1/f g]$ as a problem for type theory.

Say I wanted to show that for a ring, $R$, a set of its elements, $S$, and a partition of $S$ into $S_1$ and $S_2$, that $R[S]^{-1}$ and $(R[S_1]^{-1})[S_2]^{-1}$ are ’canonically’ identical, is this really a problem for HoTT?

]]>There is already entry commutative localization.

]]>sorry, I should have put this into *localization of a ring*. Done so now and added the definition by quotienting an ideal to *localization of a commutative ring*.

added the explicit definition at *localization of a commutative ring*