Commit 2022-05-27 04:25 bae02292

feat(category_theory/monoidal/subcategory): full monoidal subcategories (#14311) We use a type synonym for {X : C // P X} when C is a monoidal category and the property P is closed under the monoidal unit and tensor product so that full_monoidal_subcategory can be made an instance.