The span category of finite sets is semiadditive

Proof. Consider finite sets \(S_i\) for \(i=1, \dots , n\). We have spans of the form \[ \bigsqcup _{i=1}^n S_i \hookleftarrow S_i \xrightarrow {\id _{S_i}} S_i \] We claim that these morphisms exhibit \(\bigsqcup _{i=1}^n S_i\) as a product of the sets \(S_i\) in \(\Span (\Fin )\). Indeed, note that for every map \(U \to \bigsqcup _{i=1}^n S_i\) of finite sets we may write \(U = \bigsqcup _{i=1}^n U_i\), where \(U_i\) is the preimage of \(S_i\). This gives the desired equivalence of groupoids

By the dual argument (reversing a span gives a bijection between spans from \(S\) to \(T\) and spans from \(T\) to \(S\)) we see that similarly the spans \[ S_i \xleftarrow {\id _{S_i}} S_i \hookrightarrow \bigsqcup _{i=1}^n S_i. \] exhibit \(\bigsqcup _{i=1}^n S_i\) also as the coproduct of the \(S_i\) in \(\Span (\Fin )\). The composite from \(S_i\) into this coproduct and then to the \(j\)-th product factor is represented by the pullback \(S_i \times _{\bigsqcup _k S_k} S_j\). It is the identity span when \(i=j\) and the zero span otherwise. Hence the canonical comparison from the coproduct to the product is an isomorphism. For \(n=0\), the same argument says that the empty set is a zero object. Thus \(\Span (\Fin )\) is semiadditive. □