**Theorem:** A category \\(C\\) with all binary coproducts (there exists a coproduct for every pair of objects) and an initial object \\(\mathbf{0}\\) is a monoidal category where the coproduct is the tensor product and the initial object is the unit. If for any pair of objects \\(x,y\\), there exists a pair of morphisms \\(f : x \to y\\) and \\(f' : y \to x\\), then \\(C\\) is also a symmetric monoidal category.

Proof: Here's what we need to show for \\(C\\) in order to prove it is a symmetric monoidal category.

+ There's a bifunctor \\(\otimes : C \times C \to C\\) which is a functor from the product category \\(C \times C\\) into \\(C\\). We must be able to tensor both objects and morphisms.

+ an identity object \\(I\\): this will be isomorphic to the initial object \\(\mathbf{0}\\)

+ the tensor product must be associative up to isomorphism, meaning there must be a natural isomorphism \\(\alpha_{xyz} : (x \otimes y) \otimes z \cong x \otimes (y \otimes z)\\)

+ tensoring any object \\(x\\) with the identity object must be isomorphic to \\(x\\): so we must have left and right unitor natural isomophisms \\(\lambda_x : I \otimes x \cong x \\) and \\(\rho_x : x \otimes I \cong x\\)

+ both the associator and unitors must satisfy coherence conditions: [triangle and pentagram diagrams](https://ncatlab.org/nlab/show/symmetric+monoidal+category)

+ a braiding natural isomorphism: \\(B_{xy} : x \otimes y \to y\otimes x\\)

+ braiding and the associator obey the [hexagon identities](https://ncatlab.org/nlab/show/symmetric+monoidal+category) and we require \\(B_{yx}B_{xy} = 1_{x\otimes y}\\)

We are given that \\(C\\) has all binary coproducts (as John points out, if you have all binary coproducts, then you also can repeat the binary coproduct to get objects isomorphic to coproducts over any number of objects) and that \\(C\\) has an initial object \\(\mathbf{0}\\). Both of these objects are defined as colimits and have an universal property which we will use to show that we can form a symmetric monoidal category. I'll write the coproduct of \\(A\\) and \\(B\\) as \\(A+ B\\)

+ The universal property of the coproduct of two objects \\(A,B\\) is for any pair of maps \\(f:A \to X\\) and \\(g:B\to X\\), there is an unique map \\([f,g]:A+B\to X\\) such that \\(f\\) and \\(g\\) factor into \\(f = [f,g]i_A\\) and \\(g = [f,g]i_B\\) where \\(i_A : A \to A+B\\) and \\(i_B : B \to A +B\\) are inclusion maps.

+ The universal property of the initial object \\(\mathbf{0}\\) is for any object \\(X\\), there exists an unique map \\(h: \mathbf{0} \to X\\). Note that initial objects are always isomorphic to one another (proof is left to the reader), so even if there's more than one, we can treat them as one object.

For the coproduct \\(+\\) to be the tensor product \\(\otimes\\), we need to define what happens to objects *and* morphisms (or rather pairs of objects and morphisms). The coproduct already says what to do: let \\(A\otimes B = A+B\\). Since \\(C\\) has all binary coproducts, we can do this for all objects. But what do we do with morphisms?

Consider \\(f:x \to y\\) and \\(f' : x' \to y'\\). Tensoring these objects and morphisms should give \\(f \otimes f' : x \otimes x' \to y\otimes y'\\). So we must send the pair \\((f,f')\\) to an unique map \\(x +x' : y +y'\\). But remember the universal property of coproducts, since there's a map \\(i_{y}f : x \to y + y' \\) and \\(i_{y'} f' : x' \to y +y'\\), there must be a unique map \\([f,f']: x + x' \to y + y'\\) such that the following [diagram commutes](https://tikzcd.yichuanshen.de/#eyJub2RlcyI6W3sicG9zaXRpb24iOlswLDBdLCJ2YWx1ZSI6IngifSx7InBvc2l0aW9uIjpbMiwwXSwidmFsdWUiOiJ5In0seyJwb3NpdGlvbiI6WzAsMl0sInZhbHVlIjoieCcifSx7InBvc2l0aW9uIjpbMiwyXSwidmFsdWUiOiJ5JyJ9LHsicG9zaXRpb24iOlswLDFdLCJ2YWx1ZSI6IngreCcifSx7InBvc2l0aW9uIjpbMiwxXSwidmFsdWUiOiJ5K3knIn1dLCJlZGdlcyI6W3siZnJvbSI6MiwidG8iOjQsInZhbHVlIjoiaV97eCd9In0seyJmcm9tIjowLCJ0byI6NCwibGFiZWxQb3NpdGlvbiI6InJpZ2h0IiwidmFsdWUiOiJpX3gifSx7ImZyb20iOjEsInRvIjo1LCJsYWJlbFBvc2l0aW9uIjoibGVmdCIsInZhbHVlIjoiaV95In0seyJmcm9tIjozLCJ0byI6NSwibGFiZWxQb3NpdGlvbiI6InJpZ2h0IiwidmFsdWUiOiJpX3t5J30ifSx7ImZyb20iOjAsInRvIjoxLCJ2YWx1ZSI6ImYifSx7ImZyb20iOjIsInRvIjozLCJ2YWx1ZSI6ImYnIn0seyJmcm9tIjo0LCJ0byI6NSwibGluZSI6ImRhc2hlZCIsInZhbHVlIjoiXFxleGlzdHMhIFxcIFtmLGYnXSJ9XX0=):

\[\begin{matrix} x & \overset{f}{\rightarrow} & y\\\ i_x \downarrow \quad & & \quad \downarrow i_y\\\ x+ x' & \overset{[f,f']}{\rightarrow} & y + y' \\\ i_{x'}\uparrow \quad & & \quad \uparrow i_{y'} \\\ x' & \overset{f'}{\rightarrow} & y' \end{matrix} \]

Using this argument, we get the associator isomorphism. Repeating the binary coproduct \\(n\\) times is isomorphic to a coproduct over \\(n\\) objects. We only need show this for three objects \\(x,y,z\\) such that

\[\alpha_{xyz}: (x+ y)+ z \to x + (y+z) \]

We prove that \\((x +y) + z \to x + (y+z)\\) by showing \\(\hom((x +y) + z,a) \cong \hom(x + (y+z),a)\\) (I think this statement is the Yoneda lemma). By the universal property of the coproduct, for \\(f:x\to a\\), \\(g:y \to a\\), and \\(h: z \to a\\), there's a unique map \\([f,g]: x +y \to a\\) and therefore a unique map \\([[f,g],h] \in \hom((x +y) + z,a) \\), but by the same properties there's a corresponding unique map \\([f,[g,h]] \in \hom(x + (y + z),a) \\), so \\( (x+ y)+ z \cong x + (y+z)\\) and the associator exists!

Using this argument, we also get the braiding natural isomorphism. For any pair of objects \\(x,y\\), if there exists any map \\(f: x\to y\\) and \\(f': y\to x\\), then

\[x + y \cong y + x \]

since there is a unique map \\([f,f'] : x + y \to y + x \\).

Let's show that for any \\(x\\), \\(\mathbf{0}+x \cong x \cong x+\mathbf{0}\\) proving that the initial object serves as an identity object and that the left and right unitor natural isomorphisms exist.

By the universal property of the initial object, there's a unique morphism \\(!_x : \mathbf{0} \to x\\) for any \\(x\\). We always have the identity morphism \\(1_x : x \to x\\) and so by the universal property of the coproduct, we have the unique morphism \\([!,1_x] : \mathbf{0} + x \to x \\) and \\([1_x, !]:x + \mathbf{0} \to x\\). But for any object \\(a\\) we have \\(\hom(\mathbf{0} + x,a)\cong \hom(x,a) \cong \hom(x+\mathbf{0},a)\\) since given \\(f:x\to a\\) there's an unique choice of map for each homset: \\([!_a ,f]\\), \\(f\\), and \\([f,!_a]\\)

All that's left is to show that the coherence conditions hold.

Proof: Here's what we need to show for \\(C\\) in order to prove it is a symmetric monoidal category.

+ There's a bifunctor \\(\otimes : C \times C \to C\\) which is a functor from the product category \\(C \times C\\) into \\(C\\). We must be able to tensor both objects and morphisms.

+ an identity object \\(I\\): this will be isomorphic to the initial object \\(\mathbf{0}\\)

+ the tensor product must be associative up to isomorphism, meaning there must be a natural isomorphism \\(\alpha_{xyz} : (x \otimes y) \otimes z \cong x \otimes (y \otimes z)\\)

+ tensoring any object \\(x\\) with the identity object must be isomorphic to \\(x\\): so we must have left and right unitor natural isomophisms \\(\lambda_x : I \otimes x \cong x \\) and \\(\rho_x : x \otimes I \cong x\\)

+ both the associator and unitors must satisfy coherence conditions: [triangle and pentagram diagrams](https://ncatlab.org/nlab/show/symmetric+monoidal+category)

+ a braiding natural isomorphism: \\(B_{xy} : x \otimes y \to y\otimes x\\)

+ braiding and the associator obey the [hexagon identities](https://ncatlab.org/nlab/show/symmetric+monoidal+category) and we require \\(B_{yx}B_{xy} = 1_{x\otimes y}\\)

We are given that \\(C\\) has all binary coproducts (as John points out, if you have all binary coproducts, then you also can repeat the binary coproduct to get objects isomorphic to coproducts over any number of objects) and that \\(C\\) has an initial object \\(\mathbf{0}\\). Both of these objects are defined as colimits and have an universal property which we will use to show that we can form a symmetric monoidal category. I'll write the coproduct of \\(A\\) and \\(B\\) as \\(A+ B\\)

+ The universal property of the coproduct of two objects \\(A,B\\) is for any pair of maps \\(f:A \to X\\) and \\(g:B\to X\\), there is an unique map \\([f,g]:A+B\to X\\) such that \\(f\\) and \\(g\\) factor into \\(f = [f,g]i_A\\) and \\(g = [f,g]i_B\\) where \\(i_A : A \to A+B\\) and \\(i_B : B \to A +B\\) are inclusion maps.

+ The universal property of the initial object \\(\mathbf{0}\\) is for any object \\(X\\), there exists an unique map \\(h: \mathbf{0} \to X\\). Note that initial objects are always isomorphic to one another (proof is left to the reader), so even if there's more than one, we can treat them as one object.

For the coproduct \\(+\\) to be the tensor product \\(\otimes\\), we need to define what happens to objects *and* morphisms (or rather pairs of objects and morphisms). The coproduct already says what to do: let \\(A\otimes B = A+B\\). Since \\(C\\) has all binary coproducts, we can do this for all objects. But what do we do with morphisms?

Consider \\(f:x \to y\\) and \\(f' : x' \to y'\\). Tensoring these objects and morphisms should give \\(f \otimes f' : x \otimes x' \to y\otimes y'\\). So we must send the pair \\((f,f')\\) to an unique map \\(x +x' : y +y'\\). But remember the universal property of coproducts, since there's a map \\(i_{y}f : x \to y + y' \\) and \\(i_{y'} f' : x' \to y +y'\\), there must be a unique map \\([f,f']: x + x' \to y + y'\\) such that the following [diagram commutes](https://tikzcd.yichuanshen.de/#eyJub2RlcyI6W3sicG9zaXRpb24iOlswLDBdLCJ2YWx1ZSI6IngifSx7InBvc2l0aW9uIjpbMiwwXSwidmFsdWUiOiJ5In0seyJwb3NpdGlvbiI6WzAsMl0sInZhbHVlIjoieCcifSx7InBvc2l0aW9uIjpbMiwyXSwidmFsdWUiOiJ5JyJ9LHsicG9zaXRpb24iOlswLDFdLCJ2YWx1ZSI6IngreCcifSx7InBvc2l0aW9uIjpbMiwxXSwidmFsdWUiOiJ5K3knIn1dLCJlZGdlcyI6W3siZnJvbSI6MiwidG8iOjQsInZhbHVlIjoiaV97eCd9In0seyJmcm9tIjowLCJ0byI6NCwibGFiZWxQb3NpdGlvbiI6InJpZ2h0IiwidmFsdWUiOiJpX3gifSx7ImZyb20iOjEsInRvIjo1LCJsYWJlbFBvc2l0aW9uIjoibGVmdCIsInZhbHVlIjoiaV95In0seyJmcm9tIjozLCJ0byI6NSwibGFiZWxQb3NpdGlvbiI6InJpZ2h0IiwidmFsdWUiOiJpX3t5J30ifSx7ImZyb20iOjAsInRvIjoxLCJ2YWx1ZSI6ImYifSx7ImZyb20iOjIsInRvIjozLCJ2YWx1ZSI6ImYnIn0seyJmcm9tIjo0LCJ0byI6NSwibGluZSI6ImRhc2hlZCIsInZhbHVlIjoiXFxleGlzdHMhIFxcIFtmLGYnXSJ9XX0=):

\[\begin{matrix} x & \overset{f}{\rightarrow} & y\\\ i_x \downarrow \quad & & \quad \downarrow i_y\\\ x+ x' & \overset{[f,f']}{\rightarrow} & y + y' \\\ i_{x'}\uparrow \quad & & \quad \uparrow i_{y'} \\\ x' & \overset{f'}{\rightarrow} & y' \end{matrix} \]

Using this argument, we get the associator isomorphism. Repeating the binary coproduct \\(n\\) times is isomorphic to a coproduct over \\(n\\) objects. We only need show this for three objects \\(x,y,z\\) such that

\[\alpha_{xyz}: (x+ y)+ z \to x + (y+z) \]

We prove that \\((x +y) + z \to x + (y+z)\\) by showing \\(\hom((x +y) + z,a) \cong \hom(x + (y+z),a)\\) (I think this statement is the Yoneda lemma). By the universal property of the coproduct, for \\(f:x\to a\\), \\(g:y \to a\\), and \\(h: z \to a\\), there's a unique map \\([f,g]: x +y \to a\\) and therefore a unique map \\([[f,g],h] \in \hom((x +y) + z,a) \\), but by the same properties there's a corresponding unique map \\([f,[g,h]] \in \hom(x + (y + z),a) \\), so \\( (x+ y)+ z \cong x + (y+z)\\) and the associator exists!

Using this argument, we also get the braiding natural isomorphism. For any pair of objects \\(x,y\\), if there exists any map \\(f: x\to y\\) and \\(f': y\to x\\), then

\[x + y \cong y + x \]

since there is a unique map \\([f,f'] : x + y \to y + x \\).

Let's show that for any \\(x\\), \\(\mathbf{0}+x \cong x \cong x+\mathbf{0}\\) proving that the initial object serves as an identity object and that the left and right unitor natural isomorphisms exist.

By the universal property of the initial object, there's a unique morphism \\(!_x : \mathbf{0} \to x\\) for any \\(x\\). We always have the identity morphism \\(1_x : x \to x\\) and so by the universal property of the coproduct, we have the unique morphism \\([!,1_x] : \mathbf{0} + x \to x \\) and \\([1_x, !]:x + \mathbf{0} \to x\\). But for any object \\(a\\) we have \\(\hom(\mathbf{0} + x,a)\cong \hom(x,a) \cong \hom(x+\mathbf{0},a)\\) since given \\(f:x\to a\\) there's an unique choice of map for each homset: \\([!_a ,f]\\), \\(f\\), and \\([f,!_a]\\)

All that's left is to show that the coherence conditions hold.