Span category of finite sets

Construction 5.3.1 (Span category). There is an \(\infty \)-category \(\Span (\Fin )\), called the span category of finite sets. Its objects are finite sets, and for finite sets \(S\) and \(T\) its hom animae are given by the groupoids

of spans from \(S\) to \(T\); so the objects of this groupoid are spans \(S \leftarrow U \to T\) and the morphisms are isomorphisms of spans. The identity span is given by \(S \xleftarrow {\id _S} S \xrightarrow {\id _S} S\), and composition of spans is defined by taking pullbacks: