Commit 2020-07-11 08:43 36a25d9f

feat(algebra/category/*): get rid of the local reducible hack (#3354) I thought I did this back in April, but apparently never made the PR. We currently use a strange hack when setting up concrete categories, making them locally reducible. There's a library note about this, which ends:

TODO: Probably @[derive] should be able to create instances of the	
required form (without `id`), and then we could use that instead of	
this obscure `local attribute [reducible]` method.

This PR makes the small change required to delta_instance to make this happen, and then stops using the hack in setting up concrete categories (and deletes the library note explaining this hack).