This [paper](https://homepages.inf.ed.ac.uk/gdp/publications/trace.pdf) says that $FinVect\_k$ is collectively complete for traced symmetric monoidal categories, in the sense that given distinct arrows in the free traced SMC (over some generating monoidal signature) there exists a strong functor (from the free traced SMC) into $FinVect\_k$ distinguishing them.


Is there an analogous result for Cartesian categories? It would seem intuitive to me that $Set$ might be collectively complete for Cartesian categories in the sense above -- but I can't find a reference anywhere. Is this true, and is there somewhere I could find a proof?



Is Set (collectively) complete for Cartesian categories?
If I understand what you are asking, the answer is yes.
Indeed:


**Proposition.**
Let $\mathcal{C}$ be a locally small cartesian monoidal category and let $f\_0, f\_1 : X \to Y$ be a parallel pair of morphisms in $\mathcal{C}$.
Then there is a cartesian monoidal functor $F : \mathcal{C} \to \textbf{Set}$ such that $F f\_0 = F f\_1$ implies $f\_0 = f\_1$.


*Proof.* Take $F = \mathcal{C} (X, -)$ and consider $\textrm{id}\_X \in F (X)$. ◼


(This is basically a small part of the Yoneda lemma.)


