A better way to compute the mapping spaces of the category of spans in an enriched tensored category?

Question

Let X be a tensored and cotensored V-category, where V is a fixed complete, cocomplete, closed symmetric monoidal category.

Define $C:=Span(X)$ to be the category of spans in X (this is the functor category $X^{Sp}$ where $Sp$ is the walking span). We notice that $C$ is automatically "tensored" over $V$ (by computing the tensor product pointwise). Then C has a natural V-enriched structure given as follows: $Map_C(a,b)$ is the object of $V$ representing the functor $M_{ab}(\gamma):= Hom_C(\gamma \otimes a, b)$ (such an object exists by the adjoint functor theorem and since the tensor product is cocontinuous).

We can give another description of the mapping space as: $$Map_C(a,b)=Map_X(A,B)\underset{Map_X(A,B'\times B'')}{\times} (Map_X(A',B')\times Map_X(A'',B''))$$

Where $a=A'\leftarrow A \to A''$ and $b=B'\leftarrow B \to B''$.

To prove that these two descriptions are equivalent, I applied Yoneda's lemma to the second definition of $Map_C(a,b)$, which gives us $$Hom_V(Q,Map_C(a,b))=Hom_X(Q\otimes A, B)\underset{Hom_X(Q\otimes A,B'\times B'')}{\times}(Hom_X(Q\otimes A',B')\times Hom_X(Q\otimes A'',B''))$$

Which by the ordinary fiber product in the category of sets is precisely the set of triplets of arrows $(Q\otimes A\to B,(Q\otimes A'\to B',Q\otimes A''\to B''))$ giving the commutativity of the natural transformation diagram in $X$. This construction is obviously functorial in $Q$ for fixed $a$ and $b$.

Surely there must be a better way to do this, presumably without relying so heavily on the definition of the fiber product in the category of sets. What does such a proof look like? I assume there must be a simpler proof, because this fact was asserted as though it were trivial in a book I'm reading.

Question: What's a slicker way to prove that the two definitions are equivalent?

Answer 1

Because of the way you've chosen to write your second description, I don't think you're going to be able to avoid using something about the fiber product in Set. But there is a general fact here: any V-functor V-category [A,X], where A and X are V-categories, inherits any V-enriched (weighted) limits that X has, constructed pointwise. Tensors are a particular kind of V-weighted limit, and your category C is the V-functor V-category [V[Sp],X], where V[-] denotes the free V-category on an ordinary category, whose hom-objects are coproducts of copies of the unit object of V. The property that V-valued homs represent the functor $M_{a b}$ is a reformulation of the definition of tensors as a V-enriched limit, so the question then simply becomes, why is your second description an equivalent description of the canonical V-enrichment structure on C?

Now the V-valued homs of such a functor category are "always" given by writing down the Set-valued homs as a limit of homsets in Set and reinterpreting it as a limit of hom-objects in V. The universally applicable way to do this is with an end, as Finn says, but any other way that is equivalent in Set will be equivalent in V as well, for the same Yoneda reason as in your proof. So the question becomes simply, is the set of natural transformations between two spans (considered as functors out of Sp) described by the analogous pullback of homsets in Set? And there you have to know something about pullbacks in Set.

Answer 2

Not quite an answer, but I hope it helps:

Your second definition looks (somewhat) like the usual definition of the V-valued hom of V-functors $[Sp,X] (a,b) = \int_{A \in Sp} X(aA, bA)$. If that's right then $$ V(\gamma, [Sp,X] (a,b)) \cong \int_A V(\gamma,X(aA,bA)) \cong \int_A(\gamma \otimes aA,bA) = [Sp,X] (\gamma \otimes a,b) $$ and the first definition follows by applying $V(I,-)$. One way to prove the converse would be to show that $\operatorname{Nat}(?\otimes a, b) \cong \operatorname{Dinat}(?, X(a-,b-))$ in [V,Set], which is probably true, but my dinaturality-fu isn't what it should be, so that's as far as I can go.