A category has biproducts when the same objects are both the products and coproducts. Has anyone investigated the proof theory of categories with biproducts?Perhaps the best-known example is the category of vector spaces, in which the direct sum and direct product constructions give the same vector space. This means vector spaces and linear maps are a slightly degenerate model of linear logic, and I am curious what a type theory which accepts this degeneracy would look like. 
Proof theory of biproducts?
reference request;lo.logic;pl.programming languages;type theory;ct.category theory
Samson Abramsky and I wrote a paper about the proof theory of compact categories with biproducts.Abramsky, S. and Duncan, R. (2006) A Categorical Quantum Logic,  Mathematical Structures in Computer Science 16 (3).  10.1017/S0960129506005275The ideas were later developed a bit further in this book chapter:Duncan, Ross (2010) Generalised Proof-Nets for Compact Categories  with Biproducts in Semantic Techniques in Quantum Computation,  Cambridge University Press, pp70--134 arXiv:0903.5154v1The full details are there, but the short version is that your logic is inconsistent, because you have a zero proof for every implication, and the rest of your proofs are equivalent to matrices, where the matrix entries are the proofs in the biproduct-free part of the logic.  Speaking without the caveats required to make this precise, the resulting category of proofs is the free biproduct category on some category of axioms.