Lemma 5.3.16 (A slice adjunction for spans). For every finite set \(S\), the inclusion of forward maps induces a functor \[ \Fin _{/S}\longrightarrow \Span (\Fin )_{/S} \] which admits a left adjoint. On objects, this left adjoint sends a span \[ T\xleftarrow {f}U\xrightarrow {g}S \] to the map \(g\colon U\to S\). The same construction restricts to the relative slices used below: \[ \Fin ^{\leq 1}_{/S}\longrightarrow \Span (\Fin ^{\leq 1})_{/S}. \]
Proof. There is a morphism in \(\Span (\Fin )_{/S}\) from the displayed span to the forward map \(g\colon U\to S\), represented by the span \(T\xleftarrow {f}U\xrightarrow {\id _U}U\). Composition with this morphism identifies maps from \(g\colon U\to S\) to a forward map \(V\to S\) with maps from the original span to \(V\to S\) in \(\Span (\Fin )_{/S}\). This is the required adjunction. □
Generated from the authoritative LaTeX source.