Rename overloaded sym in apartness

[bsaul]

Currently in IsHeytingCommutativeRing, sym is overloaded as it is exported both from IsCommutativeRing and IsApartnessRelation. This PR renames the apartness sym to #-sym.

NOTE: #-sym is also removed from Algebra.Apartness.Properties.HeytingCommutativeRing as it is now redundant.

[jamesmckinna]

Hmmm... interesting. Thanks for the PR!
Tagging it as a bug because we should have caught this before when defining these things.

Ahead of a proper review:

• just removing the definition from Algebra.Apartness.Properties.HeytingCommutativeRing would nominally be a breaking change, so for v2.3 we should add a deprecation warning indicating the new source for the property; otherwise, for v3.0 we can simply make the break;
• the PR itself draws attention to the fact that Symmetric _#_ is in fact a redundant part of the definition of IsHeytingCommutativeRing, so it might be worth having an Algebra.Apartness.Structures.Biased smart constructor which puts the pieces together, but this could be developed downstream;
• the whole definition of HCR now seems a bit odd (compared to HCF?): why should a Ring admit inverses of elements apart from 0? As opposed to simply being a CommutativeRing with a Tight apartness relation? There might be a wider issue to raise about refactoring the whole caboodle? shoutouts to @cspollard and @Taneb for comment See [ refactor ] Definitions of Relation.Binary.Apartness and Algebra.*.*Heyting* #2587

[cspollard]

Hi @jamesmckinna . I'm not at all opposed to having things re-arranged, especially if it can become more accessible/ergonomic and, of course, more correct.

I remember a discussion on why we should not call this a LocalRing [eventually it became HeytingCommutativeRing], but I cannot find the discussion at the moment. I believe LocalRing had too many potential meanings and/or wasn't very precise. These structures are split into what we call HeytingCommutativeRing and HeytingField based on

https://ncatlab.org/nlab/show/local+ring#in_weak_foundations

I did manage to find some discussions on this in zulip from a while ago:

https://agda.zulipchat.com/#narrow/channel/264623-stdlib/topic/Fields.2C.20OrderedFields.2C.20etc.20in.20the.20standard.20library.3F

but not a direct decision on the naming convention chosen.

[jamesmckinna]

Thanks @cspollard for the back pointer to the extensive prior discussion on Zulip (before I joined! So I wasn't across this ... see #2219 )

[MatthewDaggitt]

Otherwise, this looks good to me! @jamesmckinna raises some good points for downstream, but I don't think should stop this immediate bug fix 😄

[jamesmckinna]

@bsaul are you happy undertaking the requested changes?

[bsaul]

@bsaul are you happy undertaking the requested changes?

Yes. Will do (probably later today).

[jamesmckinna]

I've made suggestion by way of emphasis, but it's not a deal-breaker.
Otherwise this looks great!
(And I've stashed a copy of the old proof of #-sym so that it can be incorporated into a hypothetical future Algebra.Apartness.Structures.Biased etc.)

[jamesmckinna]

@MatthewDaggitt are you happy with @bsaul 's changes per you review? if so, let's merge!