CatDat

Implication Details

Assumptions: cogenerating set, disjoint coproducts

Conclusions: cogenerator

Proof: Assume that $S$ is a cogenerating set and let $Q \coloneqq \coprod_{X \in S} X$. For $X \in S$ we have a monomorphism $i_X : X \to Q$. If $f,g : A \rightrightarrows B$ are two distinct morphisms, there is some $X \in S$ and a morphism $h : B \to X$ with $hf \neq hg$. Hence, $i_X h f \neq i_X h g$. This proves that $Q$ is a cogenerator.