Evaluation embedding into cogenerator products
ID: evaluation-embedding-into-cogenerator-products
For a small cogenerating family in a locally small category, the evaluation arrow 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.
New to topics? Read the docs here!