Abstract de la publi numéro 7845
We study coherence, that is, the equality of canonical natural transformations in non-free symmetric monoidal closed categories (SMCCs). To this aim, we use proof theory of intuitionistic multiplicative linear logic (IMLL) with unit. The study of coherence in non-free SMCCs is reduced to the study of equivalences on terms (representing morphisms) in free category, that include the equivalence induced by the SMCC structure. The free category is reformulated as the sequent calculus for IMLL with unit so that only the equivalences on the derivations of this system are to be considered. We establish that any equivalence induced by the
equality in a model can be axiomatized by some set of "critical pairs" of derivations. From this we derive certain sufficient conditions for full coherence and establish that the system of identities defining SMCCs is not Post-complete in the sense that extending this system with and identity which does not hold in free case does not in general cause the collapse into a preorder.