Dominic Hughes - Selected Papers

A canonical graphical syntax for non-empty finite products and sums [pdf - ps - ps.gz - bibtex]
Technical report, 2002.

[Note: This paper essentially uses the resolution condition of MALL proof nets to characterise the free product-sum category. It was never published as it turned out Hongde Hu had already characterised the free category: Contractible coherence spaces and maximal maps, ENTCS 20, 1999. The proof in the technical report can be shortened considerably because of this prior art.]

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.