A canonical graphical syntax for non-empty finite products a nd sums
Dominic Hughes · 2002
Cockett and Seely recently introduced a Lambek-style deductive system for finite products and sums, and proved decidability of equality of morphisms. The question remained as to whether one can present free categories with finite products and sums in a canonical way, i.e., as a category with morphisms and composition defined directly, rather than modulo equivalence relations. This paper shows that the non-empty case (i.e., omitting initial and final objects) can be treated in a surprisingly simple way: morphisms of the free category can be viewed as certain binary relations, with composition the usual composition of binary relations. In particular, there is a forgetful functor into the category Rel of sets and binary relations. The paper ends by relating these binary relations to proof nets.