[ refactor ] `Algebra.Structures.IsQuasiring`?

[jamesmckinna]

Why in this definition is the multiplicative structure (L670-L672)

agda-stdlib/src/Algebra/Structures.agda

Lines 667 to 674 in 5c64117

	record IsQuasiring (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) where
	field
	+-isMonoid : IsMonoid + 0#
	*-cong : Congruent₂ *
	*-assoc : Associative *
	*-identity : Identity 1# *
	distrib : * DistributesOver +
	zero : Zero 0# *

not telescoped back into

*-isMonoid : IsMonoid * 1#

Instead of the more involved unbundling of such a field into its component fields?

Maybe this has come up before, but I can't quite now see why this choice was made...

Ah... the problem of re-opening the substructures to then have to figure out which underlying setoid is in play... fair enough, but it looks a bit weird sometimes!

[JacquesCarette]

So maybe this warrants a comment in the file, so that future maintainers don't end up tripping on the same issue?

[jamesmckinna]

So maybe this warrants a comment in the file, so that future maintainers don't end up tripping on the same issue?

And I should learn this lesson and transfer it over to #2763 and I should track down the original issue which drew attention to the problem... #1617 I think (with shades of #898 too)

[jamesmckinna]

Badged status: duplicate as subsumed by #2781 (and how that got fixed in #1684 )