Symmetric Strong Monoidality With Respect to Products. The groupoid completion functor of Item 1 has a symmetric strong monoidal structure
\[ \webleft (\mathrm{K}_{0},\mathrm{K}^{\times }_{0},\mathrm{K}^{\times }_{0|\mathbb {1}}\webright ) \colon \webleft (\mathsf{Cats},\times ,\mathsf{pt}\webright ) \to \webleft (\mathsf{Grpd},\times ,\mathsf{pt}\webright ) \]
being equipped with isomorphisms
\[ \begin{gathered} \mathrm{K}^{\times }_{0|\mathcal{C},\mathcal{D}} \colon \mathrm{K}_{0}\webleft (\mathcal{C}\webright )\times \mathrm{K}_{0}\webleft (\mathcal{D}\webright ) \xrightarrow {\cong }\mathrm{K}_{0}\webleft (\mathcal{C}\times \mathcal{D}\webright ),\\ \mathrm{K}^{\times }_{0|\mathbb {1}} \colon \mathsf{pt}\xrightarrow {\cong }\mathrm{K}_{0}\webleft (\mathsf{pt}\webright ), \end{gathered} \]
natural in $\mathcal{C},\mathcal{D}\in \text{Obj}\webleft (\mathsf{Cats}\webright )$.