Commit 2025-12-18 13:14 a2089aef

refactor(CategoryTheory): make morphisms in full subcategories a 1-field structure (#26446) This PR refactors the definition of morphisms in full subcategories (and induced categories), by making them a 1-field structure. This prevents certain defeq abuse, and improves automation. (The only issue is that this adds an extra layer: f sometimes becomes f.hom, etc.) (It would make sense to redefine CommGrp/Grp/CommMon as full subcategories of Mon, rather than defining CommGrp by applying InducedCategory twice, which adds one unnecessary layer of .hom, but no attempt was made to change this in this PR.)