Coherence completions of categories (Q1575878)

A new construction for creating models of linear logic, the coherence completion of a category is introduced. If \({\mathbb C}\) is monoidal closed or \(*\)-autonomous the same is true for its coherence completion; if it is a model of linear logic, then so is its coherence completion. If \({\mathbb C}\) is an arbitrary category, the category of \({\mathbb C}\)-coherence spaces is introduced. Each \({\mathbb C}\)-coherence space consists of a coherence space and a family of objects in \({\mathbb C}\); each \({\mathbb C}\)-linear morphism is a linear morphism together with a family of arrows in \({\mathbb C}\). The category of coherence spaces \(\text{Coh}\) is viewed as \(\text{Coh}\{*\}\). The main techniques used are the categorically enriched structures. \(\text{Coh}({\mathbb C})\) is a category enriched over the category \(\text{Set}_*\) of pointed sets as well as over \(\text{Coh}\). With the approach of \(\text{Coh}({\mathbb C})\) enriched over \(\text{Set}_*\), the full subcategory of \(\text{Coh}({\mathbb C})\) whose objects are contractible \({\mathbb C}\)-coherence spaces is exactly the free bicomplete category of \({\mathbb C}\) under the zero object, products and coproducts. When \(\text{Coh}({\mathbb C})\) is regarded as enriched over \(\text{Coh}\), the coherence completion is presented as a monad on the category of categories and functors. A key idea explored in the paper is the enriched softness between products and coproducts. (The property that means that each linear morphism factors through either a product projection or a coproduct injection.) There is a connection with Abramsky's interaction categories. The main difference is that the interaction categories admit (weak) biproducts which is not necessarily the case in \(\text{Coh}({\mathbb C})\). Softness between external tensor and external par is also studied. It makes further connections to Cockett and Seely's work on weakly distributive categories and Hyland and de Paiva's work on tensor-par logic.