CatDat

Implication Details

Assumptions: disjoint finite coproductsstrict terminal object

Conclusions: thin

Reason: Let 11 be the strict terminal object, and let AA be any object. Then 1A+11 \to A + 1 is an isomorphism, since 11 is strict. Also, AA+1A \to A + 1 is a monomorphism by assumption. It follows that the unique morphism u:A1u : A \to 1 is a monomorphism. For all f,g:BAf,g : B \to A we have uf=uguf = ug (since 11 is terminal), hence f=gf = g.