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