Coherence completions of categories
Hongde Hu, André Joyal · Theoretical Computer Science · 1999
This is the first of a series of papers on coherence completions of categories. Here we show that there is a close connection between Girard's coherence spaces and free bicomplete categories. We introduce a new construction for creating models of linear logic, the coherence completion of a category. By presenting coherence completions as categories enriched over the category of pointed sets and the category of coherence spaces, the free structures on coherence completions are obtained in a very natural way. We show that if C is monoidal closed or ★-autonomous then so is its coherence completion. We also prove that if C is a model of linear logic then so is its coherence completion. A key idea of the paper which is introduced into linear logic is the notion of softness. We hope that this idea could be of use in solving the full completeness for larger fragments of linear logic.