# Commit 2022-05-27 04:25 bae02292

View on Github →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.