2026-08-16T19:48:48Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19686 2024-03-06T11:04:39Z ddc:004 open_access

Coherence by Normalization for Linear Multicategorical Structures Olimpieri, Federico Coherence Linear Multicategories Resource Calculi Normalization We establish a formal correspondence between resource calculi and appropriate linear multicategories. We consider the cases of (symmetric) representable, symmetric closed and autonomous multicategories. For all these structures, we prove that morphisms of the corresponding free constructions can be presented by means of typed resource terms, up to a reduction relation and a structural equivalence. Thanks to the linearity of the calculi, we can prove strong normalization of the reduction by combinatorial methods, defining appropriate decreasing measures. From this, we achieve a general coherence result: morphisms that live in the free multicategorical structures are the same whenever the normal forms of the associated terms are equal. As further application, we obtain syntactic proofs of Mac Lane’s coherence theorems for (symmetric) monoidal categories. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Federico Olimpieri 2024 Is Part Of LIPIcs, Volume 288, 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2024.43 urn:nbn:de:0030-drops-196865 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2024.43 eng https://creativecommons.org/licenses/by/4.0/legalcode