* 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?

Excepted from original post by @jamesmckinna in #2576 (comment)

There are several things to (re-)consider here:

• the definition of Relation.Binary.Definitions.Tight makes the conventional, but non-stdlib-conventional, design decision, to universally quantify a pair of properties, rather than consider the conjunction of two universally quantified properties (cf. [ refactor ] Reconcile Relation.Binary.Definitions.Adjoint and Function.Definitions.Inverse* #2581 )
• making the stdlib conventional choice exposes one of the conjuncts simply as ∀ x y → (x ≈ y → ¬ x # y), i.e Irreflexive _≈_ _#_, so there's a DRY issue, in that a Tight instance of Relation.Binary.Structures.IsApartnessRelation reduplicates this irrefl property; (eg. in Algebra.Apartness.Structures.IsHeytingField)
• the Heyting structures and bundles should be reorganised:
  • there's no reason for a HeytingCommutativeRing to admit inverses; but the apartness probably should be declared to be Tight (so... a Tight apartness should probably only have the one conjunct, as an 'extension' of the existing irrefl property...)
  • a HeytingField should probably be a HeytingCommutativeRing admitting inverses, ie. the tight field moves to HCR, while invertibility moves from HCR to HF

These would all be breaking changes, so v3.0, but well worth doing IMNSVHO. See #2588