agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
452 stars 138 forks source link

simplify isSet<SomeAlgebraicStructure> #1033

Closed MatthiasHu closed 1 year ago

MatthiasHu commented 1 year ago

This PR simplifies, or at least harmonizes, the definitions of the following lemmas:

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

Each of them is a simple is-set after opening the respective <Something>Str. In the case of Algebra and OrderedCommMonoid, the is-set field was impossible to use since it was exported twice from the respective records; I fixed that by hiding one copy (as it was already done in Ring, for example).

felixwellen commented 1 year ago

Thanks for the nice refactoring!