agda / agda-stdlib

The Agda standard library
https://wiki.portal.chalmers.se/agda/Libraries/StandardLibrary
Other
575 stars 237 forks source link

[DRY] More redundant `zero` fields in `Algebra.Structures` #2396

Open jamesmckinna opened 4 months ago

jamesmckinna commented 4 months ago

Cf. #2195 and #2253

Possible remedy: introduce a further refinement in which a new IsNonAssociativeRingWithoutOne would the 'right' home for such an argument, with each of the above two structures inheriting from that...?

See for example this blob and prior refactoring via Quasiring... for a possible solution.