Commit 2022-05-22 09:27 52df6ab6

refactor(category_theory): remove all decidability instances (#14046) Make the category theory library thoroughly classical: mostly this is ceasing carrying around decidability instances for the indexing types of biproducts, and for the object and morphism types in fin_category. It appears there was no real payoff: the category theory library is already extremely non-constructive. As I was running into occasional problems providing decidability instances (when writing construction involving reindexing biproducts), it seems easiest to just remove this vestigial constructiveness from the category theory library.