Commit 2020-08-26 18:55 080746fdView on Github →
feat(algebra/category/*/limits): don't rely on definitions (#3873)
This is a second attempt (which works much better) at #3860, after @TwoFX explained how to do it properly.
This PR takes the constructions of limits in the concrete categories
Module R, and
Algebra R, and makes sure that they never rely on the actual definitions of limits in "prior" categories.
Of course, at this stage the
has_limit typeclasses still contain data, so it's hard to judge whether we're really not relying on the definitions. I've marked all the
has_limits instances in these files as irreducible, but the real proof is just that this same code is working over on the