Commit 2022-08-01 15:32 bb103f35View on Github →
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.