In this talk I shall describe a deductive system for categories with finite products and coproducts, prove decidability of equality of morphisms via cut elimination, and prove a "Whitman theorem" for the free such categories over arbitrary base categories. This result provides a nice illustration of some basic techniques in categorical proof theory, and also seems to have slipped past unproved in previous work in this field.
Joint work with Robin Cockett