The symmetric monoidal structure on a category with chosen finite products.

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.braiding_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X : C} {X' : C} {Y : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f g) (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ g f)

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_forward {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X : C) (Y : C) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z)).isLimit (ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z) X).isLimit).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y X Z).hom (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id Y) (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom))

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_reverse {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X : C) (Y : C) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y) Z).isLimit (ℬ Z (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)).isLimit).hom (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X) (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Z).isLimit (ℬ Z Y).isLimit).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Z Y).inv (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom (CategoryTheory.CategoryStruct.id Y)))

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.symmetry {C : Type u} [CategoryTheory.Category.{v, u} C] (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (CategoryTheory.Limits.BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)

def CategoryTheory.symmetricOfChosenFiniteProducts {C : Type u} [CategoryTheory.Category.{v, u} C] (𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C)) (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) : CategoryTheory.SymmetricCategory (CategoryTheory.MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)

The monoidal structure coming from finite products is symmetric.