Mathematics – Category Theory
Scientific paper
2000-06-07
Studia Logica 71(2002), 331-353
Mathematics
Category Theory
22 pages, corrected proof of maximality
Scientific paper
Coherence is demonstrated for categories with binary products and sums, but without the terminal and the initial object, and without distribution. This coherence amounts to the existence of a faithful functor from a free category with binary products and sums to the category of relations on finite ordinals. This result is obtained with the help of proof-theoretic normalizing techniques. When the terminal object is present, coherence may still be proved if of binary sums we keep just their bifunctorial properties. It is found that with the simplest understanding of coherence this is the best one can hope for in bicartesian categories. The coherence for categories with binary products and sums provides an easy decision procedure for equality of arrows. It is also used to demonstrate that the categories in question are maximal, in the sense that in any such category that is not a preorder all the equations between arrows involving only binary products and sums are the same. This shows that the usual notion of equivalence of proofs in nondistributive conjunctive-disjunctive logic is optimally defined: further assumptions would make this notion collapse into triviality. (A proof of coherence for categories with binary products and sums simpler than that presented in this paper may be found in Section 9.4 of {\it Proof-Theoretical Coherence}, revised version of September 2007, http://www.mi.sanu.ac.yu/~kosta/coh.pdf.)
Dosen Kosta
Petric Zoran
No associations
LandOfFree
Bicartesian Coherence does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Bicartesian Coherence, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Bicartesian Coherence will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-290261