mathlib documentation


Full monoidal subcategories #

Given a monidal category C and a monoidal predicate on C, that is a function P : C ā†’ Prop closed under šŸ™_ and āŠ—, we can put a monoidal structure on {X : C // P X} (the category structure is defined in category_theory.full_subcategory).

When C is also braided/symmetric, the full monoidal subcategory also inherits the braided/symmetric structure.


  • prop_id' : P (šŸ™_ C) . "obviously"
  • prop_tensor' : (āˆ€ {X Y : C}, P X ā†’ P Y ā†’ P (X āŠ— Y)) . "obviously"

A property C ā†’ Prop is a monoidal predicate if it is closed under šŸ™_ and āŠ—.

Instances of this typeclass
@[protected, instance]

When P is a monoidal predicate, the full subcategory for P inherits the monoidal structure of C.


A property C ā†’ Prop is a closed predicate if it is closed under taking internal homs

Instances of this typeclass