Adding apartness relations and the beginnings of local rings and fields (II)

[cspollard]

This is a follow-up from #1615 , in which I tried and failed a rebase and needed to start afresh.

Motivated by eventually having constructive Fields in the standard library, I've started to implement apartness relations, local rings, and heyting fields, largely based on

https://ncatlab.org/nlab/show/apartness+relation
https://ncatlab.org/nlab/show/local+ring#in_weak_foundations
https://ncatlab.org/nlab/show/field#constructive

Thanks again to @MatthewDaggitt for your careful review and patience. If there are any further things that need to be cleaned up, I'm happy to do so.

[MatthewDaggitt]

Thanks @cspollard! I've made some minor tweaks, the only major one is removing the private Iso definition by splitting the record field into two.

[MatthewDaggitt]

Okay, merging in. Thanks again @cspollard! Thanks for sticking with it given the long process.