Bicartesian Coherence

dc.creatorDosen, K.
dc.creatorPetric, Z.
dc.date2000-06-07
dc.date2007-09-13
dc.date.accessioned2026-07-07T08:29:13Z
dc.date.available2026-07-07T08:29:13Z
dc.descriptionCoherence 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.)
dc.description22 pages, corrected proof of maximality
dc.identifierhttps://arxiv.org/abs/math/0006052
dc.identifierhttp://arxiv.org/abs/math/0006052
dc.identifierStudia Logica 71(2002), 331-353
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/137890
dc.subjectCategory Theory
dc.subjectLogic
dc.subject18A30, 18A15
dc.titleBicartesian Coherence
dc.typetext

Files

Collections