Definition [efr-KO4T]

Let \mathcal {D} \to \mathcal {C} be a (Grothendieck) fibration, and let \mathcal {C} \to \mathcal {C}' be a faithful, identity-on-objects functor. Suppose \mathcal {C} admits pullbacks, and given a pair of morphisms P \to X,Y \in \mathcal {C}' over Z, where P \to X is in \mathcal {C}, there is a unique common factorization P \to X \times _Z Y.

1. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {C} as the vertical category, spans X \leftarrow P \to Y in \mathcal {C} equipped with a section X \to P \in {\mathcal {C}'} as horizontal cells, and maps of spans which commute with the sections as 2-cells.
2. The double category \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) lying over \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C}) has \mathcal {D} as the vertical category, and spans \bar {X} \xleftarrow {f} \bar {P} \xrightarrow {g} \bar {Y} where f is Cartesian, decorated with a section X \to P in \mathcal {C}' as the horizontal cells, and maps of such spans (so that the underlying thing commutes with the sections) as the 2-cells. We will call the horizontal cells decorated spans.
3. There is an apparent forgetful functor \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {D} / \mathcal {C}) \to \mathsf {\mathbb Span}_{\mathcal {C}'}(\mathcal {C})