The natural monoidal structure on any category with finite (co)products.
A category with a monoidal structure provided in this way is sometimes called a (co)cartesian category, although this is also sometimes used to mean a finitely complete category. (See https://ncatlab.org/nlab/show/cartesian+category.)
As this works with either products or coproducts, and sometimes we want to think of a different monoidal structure entirely, we don't set up either construct as an instance.
Implementation
For the sake of nicer definitional properties,
we rely on has_terminal and has_binary_products instead of has_finite_products,
so that if a particular category provides customised instances of these
we pick those up instead.
def
category_theory.limits.prod.braiding
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q : C) :
The braiding isomorphism which swaps a binary product.
@[simp]
@[simp]
theorem
category_theory.limits.braid_natural
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : Z ⟶ W) :
The braiding isomorphism can be passed through a map by swapping the order.
theorem
category_theory.limits.braid_natural_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{W X Y Z : C}
(f : X ⟶ Y)
(g : Z ⟶ W)
{X' : C}
(f' : W ⨯ Y ⟶ X') :
@[simp]
theorem
category_theory.limits.prod.symmetry'_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q : C)
{X' : C}
(f' : P ⨯ Q ⟶ X') :
@[simp]
theorem
category_theory.limits.prod.symmetry'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q : C) :
theorem
category_theory.limits.prod.symmetry
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q : C) :
(category_theory.limits.prod.braiding P Q).hom ≫ (category_theory.limits.prod.braiding Q P).hom = 𝟙 (P ⨯ Q)
The braiding isomorphism is symmetric.
theorem
category_theory.limits.prod.symmetry_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q : C)
{X' : C}
(f' : P ⨯ Q ⟶ X') :
(category_theory.limits.prod.braiding P Q).hom ≫ (category_theory.limits.prod.braiding Q P).hom ≫ f' = f'
@[simp]
theorem
category_theory.limits.prod.associator_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q R : C) :
def
category_theory.limits.prod.associator
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q R : C) :
The associator isomorphism for binary products.
Equations
- category_theory.limits.prod.associator P Q R = {hom := category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.fst) (category_theory.limits.prod.lift (category_theory.limits.prod.fst ≫ category_theory.limits.prod.snd) category_theory.limits.prod.snd), inv := category_theory.limits.prod.lift (category_theory.limits.prod.lift category_theory.limits.prod.fst (category_theory.limits.prod.snd ≫ category_theory.limits.prod.fst)) (category_theory.limits.prod.snd ≫ category_theory.limits.prod.snd), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.prod.associator_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(P Q R : C) :
def
category_theory.limits.prod_functor_left_comp
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(X Y : C) :
The product functor can be decomposed.
theorem
category_theory.limits.prod.pentagon
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(W X Y Z : C) :
category_theory.limits.prod.map (category_theory.limits.prod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.prod.associator W (X ⨯ Y) Z).hom ≫ category_theory.limits.prod.map (𝟙 W) (category_theory.limits.prod.associator X Y Z).hom = (category_theory.limits.prod.associator (W ⨯ X) Y Z).hom ≫ (category_theory.limits.prod.associator W X (Y ⨯ Z)).hom
theorem
category_theory.limits.prod.pentagon_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
(W X Y Z : C)
{X' : C}
(f' : W ⨯ (X ⨯ (Y ⨯ Z)) ⟶ X') :
category_theory.limits.prod.map (category_theory.limits.prod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.prod.associator W (X ⨯ Y) Z).hom ≫ category_theory.limits.prod.map (𝟙 W) (category_theory.limits.prod.associator X Y Z).hom ≫ f' = (category_theory.limits.prod.associator (W ⨯ X) Y Z).hom ≫ (category_theory.limits.prod.associator W X (Y ⨯ Z)).hom ≫ f'
theorem
category_theory.limits.prod.associator_naturality
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(f₃ : X₃ ⟶ Y₃) :
category_theory.limits.prod.map (category_theory.limits.prod.map f₁ f₂) f₃ ≫ (category_theory.limits.prod.associator Y₁ Y₂ Y₃).hom = (category_theory.limits.prod.associator X₁ X₂ X₃).hom ≫ category_theory.limits.prod.map f₁ (category_theory.limits.prod.map f₂ f₃)
theorem
category_theory.limits.prod.associator_naturality_assoc
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(f₃ : X₃ ⟶ Y₃)
{X' : C}
(f' : Y₁ ⨯ (Y₂ ⨯ Y₃) ⟶ X') :
category_theory.limits.prod.map (category_theory.limits.prod.map f₁ f₂) f₃ ≫ (category_theory.limits.prod.associator Y₁ Y₂ Y₃).hom ≫ f' = (category_theory.limits.prod.associator X₁ X₂ X₃).hom ≫ category_theory.limits.prod.map f₁ (category_theory.limits.prod.map f₂ f₃) ≫ f'
def
category_theory.limits.prod.left_unitor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(P : C) :
The left unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.left_unitor P = {hom := category_theory.limits.prod.snd (category_theory.limits.has_limit_of_has_limits_of_shape (category_theory.limits.pair (⊤_C) P)), inv := category_theory.limits.prod.lift (category_theory.limits.terminal.from P) (𝟙 P), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
@[simp]
theorem
category_theory.limits.prod.left_unitor_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(P : C) :
@[simp]
@[simp]
theorem
category_theory.limits.prod.right_unitor_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(P : C) :
def
category_theory.limits.prod.right_unitor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(P : C) :
The right unitor isomorphism for binary products with the terminal object.
Equations
- category_theory.limits.prod.right_unitor P = {hom := category_theory.limits.prod.fst (category_theory.limits.has_limit_of_has_limits_of_shape (category_theory.limits.pair P (⊤_C))), inv := category_theory.limits.prod.lift (𝟙 P) (category_theory.limits.terminal.from P), hom_inv_id' := _, inv_hom_id' := _}
theorem
category_theory.limits.prod_left_unitor_hom_naturality_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y)
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.prod.map (𝟙 (⊤_C)) f ≫ (category_theory.limits.prod.left_unitor Y).hom ≫ f' = (category_theory.limits.prod.left_unitor X).hom ≫ f ≫ f'
theorem
category_theory.limits.prod_left_unitor_hom_naturality
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y) :
theorem
category_theory.limits.prod_left_unitor_inv_naturality
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y) :
theorem
category_theory.limits.prod_left_unitor_inv_naturality_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y)
{X' : C}
(f' : ⊤_C ⨯ Y ⟶ X') :
(category_theory.limits.prod.left_unitor X).inv ≫ category_theory.limits.prod.map (𝟙 (⊤_C)) f ≫ f' = f ≫ (category_theory.limits.prod.left_unitor Y).inv ≫ f'
theorem
category_theory.limits.prod_right_unitor_hom_naturality
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y) :
theorem
category_theory.limits.prod_right_unitor_hom_naturality_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y)
{X' : C}
(f' : Y ⟶ X') :
category_theory.limits.prod.map f (𝟙 (⊤_C)) ≫ (category_theory.limits.prod.right_unitor Y).hom ≫ f' = (category_theory.limits.prod.right_unitor X).hom ≫ f ≫ f'
theorem
category_theory.limits.prod_right_unitor_inv_naturality
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y) :
theorem
category_theory.limits.prod_right_unitor_inv_naturality_assoc
{C : Type u}
[category_theory.category C]
{X Y : C}
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(f : X ⟶ Y)
{X' : C}
(f' : Y ⨯ ⊤_C ⟶ X') :
(category_theory.limits.prod.right_unitor X).inv ≫ category_theory.limits.prod.map f (𝟙 (⊤_C)) ≫ f' = f ≫ (category_theory.limits.prod.right_unitor Y).inv ≫ f'
theorem
category_theory.limits.prod.triangle
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_products C]
[category_theory.limits.has_terminal C]
(X Y : C) :
def
category_theory.limits.coprod.braiding
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
The braiding isomorphism which swaps a binary coproduct.
Equations
- category_theory.limits.coprod.braiding P Q = {hom := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, inv := category_theory.limits.coprod.desc category_theory.limits.coprod.inr category_theory.limits.coprod.inl, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.coprod.braiding_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
@[simp]
theorem
category_theory.limits.coprod.braiding_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
@[simp]
theorem
category_theory.limits.coprod.symmetry'
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
theorem
category_theory.limits.coprod.symmetry
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
(category_theory.limits.coprod.braiding P Q).hom ≫ (category_theory.limits.coprod.braiding Q P).hom = 𝟙 (P ⨿ Q)
The braiding isomorphism is symmetric.
def
category_theory.limits.coprod.associator
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q R : C) :
The associator isomorphism for binary coproducts.
Equations
- category_theory.limits.coprod.associator P Q R = {hom := category_theory.limits.coprod.desc (category_theory.limits.coprod.desc category_theory.limits.coprod.inl (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inr)) (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inr), inv := category_theory.limits.coprod.desc (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inl) (category_theory.limits.coprod.desc (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inl) category_theory.limits.coprod.inr), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.coprod.associator_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q R : C) :
(category_theory.limits.coprod.associator P Q R).hom = category_theory.limits.coprod.desc (category_theory.limits.coprod.desc category_theory.limits.coprod.inl (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inr)) (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inr)
@[simp]
theorem
category_theory.limits.coprod.associator_inv
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(P Q R : C) :
(category_theory.limits.coprod.associator P Q R).inv = category_theory.limits.coprod.desc (category_theory.limits.coprod.inl ≫ category_theory.limits.coprod.inl) (category_theory.limits.coprod.desc (category_theory.limits.coprod.inr ≫ category_theory.limits.coprod.inl) category_theory.limits.coprod.inr)
theorem
category_theory.limits.coprod.pentagon
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
(W X Y Z : C) :
category_theory.limits.coprod.map (category_theory.limits.coprod.associator W X Y).hom (𝟙 Z) ≫ (category_theory.limits.coprod.associator W (X ⨿ Y) Z).hom ≫ category_theory.limits.coprod.map (𝟙 W) (category_theory.limits.coprod.associator X Y Z).hom = (category_theory.limits.coprod.associator (W ⨿ X) Y Z).hom ≫ (category_theory.limits.coprod.associator W X (Y ⨿ Z)).hom
theorem
category_theory.limits.coprod.associator_naturality
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
{X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
(f₁ : X₁ ⟶ Y₁)
(f₂ : X₂ ⟶ Y₂)
(f₃ : X₃ ⟶ Y₃) :
def
category_theory.limits.coprod.left_unitor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
(P : C) :
The left unitor isomorphism for binary coproducts with the initial object.
Equations
- category_theory.limits.coprod.left_unitor P = {hom := category_theory.limits.coprod.desc (category_theory.limits.initial.to P) (𝟙 P), inv := category_theory.limits.coprod.inr (category_theory.limits.has_colimit_of_has_colimits_of_shape (category_theory.limits.pair (⊥_C) P)), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.coprod.left_unitor_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
(P : C) :
@[simp]
@[simp]
def
category_theory.limits.coprod.right_unitor
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
(P : C) :
The right unitor isomorphism for binary coproducts with the initial object.
Equations
- category_theory.limits.coprod.right_unitor P = {hom := category_theory.limits.coprod.desc (𝟙 P) (category_theory.limits.initial.to P), inv := category_theory.limits.coprod.inl (category_theory.limits.has_colimit_of_has_colimits_of_shape (category_theory.limits.pair P (⊥_C))), hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.limits.coprod.right_unitor_hom
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
(P : C) :
theorem
category_theory.limits.coprod.triangle
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_binary_coproducts C]
[category_theory.limits.has_initial C]
(X Y : C) :
def
category_theory.monoidal_of_has_finite_products
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C] :
A category with a terminal object and binary products has a natural monoidal structure.
Equations
- category_theory.monoidal_of_has_finite_products C = {tensor_obj := λ (X Y : C), X ⨯ Y, tensor_hom := λ (_x _x_1 _x_2 _x_3 : C) (f : _x ⟶ _x_1) (g : _x_2 ⟶ _x_3), category_theory.limits.prod.map f g, tensor_id' := _, tensor_comp' := _, tensor_unit := ⊤_C, associator := category_theory.limits.prod.associator _inst_3, associator_naturality' := _, left_unitor := category_theory.limits.prod.left_unitor _inst_2, left_unitor_naturality' := _, right_unitor := category_theory.limits.prod.right_unitor _inst_2, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
def
category_theory.symmetric_of_has_finite_products
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C] :
The monoidal structure coming from finite products is symmetric.
Equations
- category_theory.symmetric_of_has_finite_products C = {to_braided_category := {braiding := category_theory.limits.prod.braiding _inst_3, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}
@[simp]
theorem
category_theory.symmetric_of_has_finite_products_to_braided_category_braiding
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(P Q : C) :
β_ P Q = category_theory.limits.prod.braiding P Q
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.tensor_obj
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X Y : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.tensor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
{W X Y Z : C}
(f : W ⟶ X)
(g : Y ⟶ Z) :
f ⊗ g = category_theory.limits.prod.map f g
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.left_unitor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.left_unitor_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.right_unitor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_products.right_unitor_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X : C) :
theorem
category_theory.monoidal_of_has_finite_products.associator_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_binary_products C]
(X Y Z : C) :
def
category_theory.monoidal_of_has_finite_coproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C] :
A category with an initial object and binary coproducts has a natural monoidal structure.
Equations
- category_theory.monoidal_of_has_finite_coproducts C = {tensor_obj := λ (X Y : C), X ⨿ Y, tensor_hom := λ (_x _x_1 _x_2 _x_3 : C) (f : _x ⟶ _x_1) (g : _x_2 ⟶ _x_3), category_theory.limits.coprod.map f g, tensor_id' := _, tensor_comp' := _, tensor_unit := ⊥_C, associator := category_theory.limits.coprod.associator _inst_3, associator_naturality' := _, left_unitor := category_theory.limits.coprod.left_unitor _inst_2, left_unitor_naturality' := _, right_unitor := category_theory.limits.coprod.right_unitor _inst_2, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
@[simp]
theorem
category_theory.symmetric_of_has_finite_coproducts_to_braided_category_braiding
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(P Q : C) :
def
category_theory.symmetric_of_has_finite_coproducts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C] :
The monoidal structure coming from finite coproducts is symmetric.
Equations
- category_theory.symmetric_of_has_finite_coproducts C = {to_braided_category := {braiding := category_theory.limits.coprod.braiding _inst_3, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.tensor_obj
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X Y : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.tensor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
{W X Y Z : C}
(f : W ⟶ X)
(g : Y ⟶ Z) :
f ⊗ g = category_theory.limits.coprod.map f g
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.left_unitor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.right_unitor_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.left_unitor_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_of_has_finite_coproducts.right_unitor_inv
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X : C) :
theorem
category_theory.monoidal_of_has_finite_coproducts.associator_hom
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_binary_coproducts C]
(X Y Z : C) :