4:00 - 5:00 R.A.G. Seely

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