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!