Remove `isSet` accessors for algebraic structures?

[MatthiasHu]

I propose to delete the following lemmas:

isSetGroup
isSetRing
isSetDistLattice
isSetCommAlgebra
isSetLeftModule
isSetField
isSetAlgebra
isSetLattice
isSetCommRing
isSetAbGroup
isSetOrderedCommMonoid
isSetCommMonoid

They seem unnecessary, since all these algebraic structures expose an is-set field through the inheritance mechanism of the Is<Something> records already (as demonstrated in https://github.com/agda/cubical/pull/1033). Also note that some structures are missing, e.g. Monoid.

I would say it is better to directly use is-set everywhere (and I would be willing to implement that change). Are there other opinions on this?

[felixwellen]

I agree. One could be unhappy about "public" use of 'is-set' which is not in line with the naming conventions. I am not though. Especially when thinking of using instance resolution to prove h-levels in the future.

[mzeuner]

I support that change as well, especially given that only some structures have such a lemma.

[MatthiasHu]

Good -- I will do this now.