Commit 2020-08-26 18:55 080746fd

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 (Add)(Comm)[Mon|Group], (Comm)(Semi)Ring, 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 prop_limits branch.