Natural transformations span

Construction 13.2.1. Consider adequate triples \((C,C_L,C_R)\) and \((D,D_L,D_R)\) and let \(F,G\colon C \to D\) be morphisms of adequate triples. Let \(\alpha \colon F \Rightarrow G\) be a natural transformation, and assume that the following two conditions are satisfied:

(1)

The morphism \(\alpha (X)\colon F(X) \to G(X)\) lies in \(D_R\) for every object \(X\) of \(C\);

(2)

For every morphism \(l\colon Z \to X\) in \(C_L\) the commutative square

is a pullback square in \(D\).

We will construct a natural transformation \[ \Span ^{\mathrm {R}}(\alpha )\colon \Span (F) \implies \Span (G) \] of functors \(\Span _{L,R}(C) \to \Span _{L,R}(D)\) which is objectwise given by the forward spans \[ F(X) \xleftarrow {=} F(X) \xrightarrow {\alpha (X)} G(X) \] for \(X \in C\). For this, equip \([1]\) with the adequate triple structure \(([1],[1]^{\simeq },[1])\). Then the product \(C \times [1]\) is an adequate triple with backward and forward classes \(C_L \times [1]^{\simeq }\) and \(C_R \times [1]\), respectively. Regarding \(\alpha \) as a functor \(C \times [1] \to D\), conditions (1) and (2) say precisely that it is a morphism of adequate triples. Indeed, the only additional pullback squares to check are sent to pastings of images under \(F\) or \(G\) of adequate pullback squares with the naturality squares from (2). We therefore obtain a functor \[ \Span _{L,R}(C \times [1]) \to \Span _{L,R}(D). \] Using that \(\Span (-)\) preserves products by Proposition 13.1.19 and that \(\Span _{\tiso ,\all }([1]) \simeq [1]\) by Lemma 13.1.16, this functor takes the form \[ \Span _{L,R}(C) \times [1] \to \Span _{L,R}(D). \] The restrictions to \(0\) and \(1\) are precisely \(\Span (F)\) and \(\Span (G)\), so this produces the desired natural transformation \(\Span ^{\mathrm {R}}(\alpha )\).