Implication Details

Assumptions: coproducts, generating set, zero morphisms

Conclusions: generator

Reason: If SS is a generating set, we claim that U:=∐G∈SGU := \coprod_{G \in S} G is a generator. For this it is not required to have zero morphisms, we only need that for all G,G′∈SG,G' \in S there is at least one morphism G→G′G \to G'. This implies that each inclusion G→UG \to U has a left inverse. Now let f,g:A⇉Bf,g : A \rightrightarrows B be two morphism with fh=ghf h = g h for all h:U→Ah : U \to A. If G∈SG \in S, any morphism G→AG \to A extends to UU by our preliminary remark. Thus, fh=ghfh = gh holds for all h:G→Ah : G \to A and G∈SG \in S. Since SS is a generating set, this implies f=gf = g.