Implication Details

Assumptions: binary coproducts, left cancellative

Conclusions: thin

Reason: For every object AA the codiagonal A+A→AA + A \to A is a split epimorphism, and by assumption a monomorphism, hence an isomorphism. Hence, the two inclusions i1,i2:A→A+Ai_1,i_2 : A \to A + A coincide. Now, if f,g:A→Bf, g : A \to B are two morphisms, consider the induced morphism h:A+A→Bh : A + A \to B and compute f=h∘i1=h∘i2=gf = h \circ i_1 = h \circ i_2 = g.