Anders Mörtberg
Anders Mörtberg
Some files import things public which can cause problems later when renaming and refactoring. We should get rid of all public imports that are not crucial (for example the Prelude...
The library contains a lot of different representations of the integers: - https://github.com/agda/cubical/tree/master/Cubical/HITs/Ints - https://github.com/agda/cubical/tree/master/Cubical/Data/DiffInt - https://github.com/agda/cubical/tree/master/Cubical/Data/Int - https://github.com/agda/cubical/blob/master/Cubical/HITs/S1/Base.agda#L40 and the rationals: - https://github.com/agda/cubical/tree/master/Cubical/HITs/Rationals It would be good to collect...
Someone asked how to cite the library on Zulip. How about: ``` @misc{agdacubical, title = {The agda/cubical library}, author = {{The agda/cubical development team}}, year = {2018--}, url = {https://github.com/agda/cubical/},...
We could remove for example `makeGroup` as groups should be constructed using copatterns anyway. It might still be nice to keep the `makeIsGroup` and it should hopefully not be a...
See comment on https://github.com/UniMath/UniMath/pull/606#issuecomment-282258761. This could be a nice exercise for someone who wants to learn UniMath.
Any objections to this? As far as I understand --guardedness is safe and doesn't interfere with anything, but the Codata folder needs it. This should allow us to simplify the...
@martinescardo
I think the category theory in the library should be rewritten to match the way the algebra code is written. In particular, data and properties should be separated so that...
There is currently some unnecessary duplication between `Data.Fin` and `Data.Fin.Inductive`. These two definitions of `Fin` are almost identical, but parts of the library uses one definition and some uses the...