Evaluation embedding into cogenerator products
= Evaluation embedding into cogenerator products
For a <small cogenerating family> $(Q_i)$ in a <locally small category>, the evaluation arrow $C\to\prod_{i,q\in\mathcal C(C,Q_i)}Q_i$ is a <monomorphism> whenever that small <product in a category> exists. Equality after all its projections is equality after every map to a cogenerator, hence equality of the original parallel <morphisms>.