# Commit 2022-05-22 09:27 52df6ab6

View on Github →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.