mathlib

52df6ab6 - refactor(category_theory): remove all decidability instances (#14046)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>