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. 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 who live in the free multicategorical structures are the same whenever the normal forms of the associated class of terms are equal. As an application, we obtain syntactic proofs of Mac Lane's coherence theorems for (symmetric) monoidal categories.

翻译：我们建立了资源演算与相应线性多范畴之间的形式对应关系。研究了（对称）可表示多范畴、对称闭包多范畴以及自主多范畴的情形。对于所有这些结构，我们证明对应的自由构造中的态射可以通过带类型的资源项（在约化关系下）来表示。得益于演算的线性性质，我们通过定义适当的递减度量，利用组合方法证明了强规范化性质。由此获得一个普适性的一致性结论：在自由多范畴结构中，当关联项类的范式相等时，这些态射必然相同。作为应用，我们给出了麦克兰关于（对称）幺半范畴一致性定理的语法证明。