Hello, I have posted an update to Foundations library at https://github.com/vladimirias . There is now basic rational arithmetic defined using set quotients of types as well as an extended version of the abstract algebra files, including many results on relations and some results on integral domains and ( geometric ) fields. Vladimir.