Commit 2022-08-01 15:32 bb103f35

refactor(category_theory): custom structure for full_subcategory (#14767) Full subcategories are now a custom structure rather than the usual subtype. The advantage of this is that we don't have to fight the simp-normal form of subtypes, as the coercion does more harm than good for full subcategories. We saw a similar refactor for discrete categories, and in both cases, erring on the side of explicitness seems to pay off.