Geodesic
Finite sum - product logic
Theory and applications of categories, Tome 8 (2001), pp. 63-99.

Voir la notice de l'article provenant de la source Theory and Applications of Categories website

In this paper we 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. Furthermore, it suggests a type-theoretic approach to 2-player input-output games.
Classification : 03B70, 03F05, 03F07, 03G30
Keywords: categories, categorical proof theory, finite coproducts, finite products, deductive systems. 
@article{TAC_2001_8_a4,
     author = {J. R. B. Cockett and R. A. G. Seely},
     title = {Finite sum - product logic},
     journal = {Theory and applications of categories},
     pages = {63--99},
     publisher = {mathdoc},
     volume = {8},
     year = {2001},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/TAC_2001_8_a4/}
}
TY  - JOUR
AU  - J. R. B. Cockett
AU  - R. A. G. Seely
TI  - Finite sum - product logic
JO  - Theory and applications of categories
PY  - 2001
SP  - 63
EP  - 99
VL  - 8
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TAC_2001_8_a4/
LA  - en
ID  - TAC_2001_8_a4
ER  - 
%0 Journal Article
%A J. R. B. Cockett
%A R. A. G. Seely
%T Finite sum - product logic
%J Theory and applications of categories
%D 2001
%P 63-99
%V 8
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TAC_2001_8_a4/
%G en
%F TAC_2001_8_a4
J. R. B. Cockett; R. A. G. Seely. Finite sum - product logic. Theory and applications of categories, Tome 8 (2001), pp. 63-99. http://geodesic.mathdoc.fr/item/TAC_2001_8_a4/