for C being Cocartesian_category holds C is with_finite_coproduct