---- > [!theorem]+ Theorem. ([[coproducts are disjoint unions in set]]) > [[disjoint union|Disjoint unions]] $A \amalg B$ (or, more precisely, $A \amalg B$ together with information of the [[inclusion map|inclusion-embeddings]] $A \xrightarrow{\iota_{A}} A \amalg B$ and $B \xrightarrow{\iota_{B}} A \amalg B$) are [[terminal object|initial]] in the [[two-object coslice category|two-object coslice]] [[category]] $\mathsf{Set}^{A,B}$. Hence, [[category|categorically speaking]], $A \amalg B$ is the [[categorical coproduct|coproduct]] of $A$ and $B$ in $\mathsf{Set}$. ^theorem > [!proof]+ Proof. ([[coproducts are disjoint unions in set]]) > The [[disjoint union]] $A \amalg B$ is the union of two disjoint [[bijection|isomorphic]] ('tagged') copies $A',B'$ of $A,B$ respectively; e.g. we may let $A'=\{ 0 \} \times A$ and $B'=\{ 1 \} \times[](multi-object%20coslice%20category.md) defined $a \xmapsto{\iota_{A}} (0,a) \text{ and } b \xmapsto{\iota_{B}}(1,b),$ viewing these elements as members of $(\{ 0 \} \times A)\cup (\{ 1 \} \times B)$. Now let $f_{A}: A \to Z$, and $f_{B}:B \to Z$ be arbitrary morphisms with common target $Z$. Define $\sigma: A \amalg B \to Z$ as $\sigma( j, c ):=\begin{cases} f_{A}(c) & j=0 ;\\ f_{B}(c) & j = 1 .\end{cases}$ Observe that this definition makes the diagram commute and is in fact forced upon us by this commutativity, proving existence and uniqueness of $\sigma$. ^proof #### ----- #### References > [!backlink] > ```dataview TABLE rows.file.link as "Further Reading" FROM [[]] FLATTEN file.tags GROUP BY file.tags as Tag > [!frontlink] > ```dataview > TABLE rows.file.link as "Further Reading" > FROM outgoing([[]]) > FLATTEN file.tags as Tag > WHERE Tag = "#definition" OR Tag = "#theorem" OR Tag = "#MOC" OR Tag = "#proposition" OR Tag = "#axiom" > GROUP BY Tag > ``` #reformatrevisebatch01