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

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?

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?
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.