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