mathlib

bb103f35 - refactor(category_theory): custom structure for full_subcategory (#14767)

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.