Coherence by Normalization for Linear Multicategorical Structures

TL;DR

This paper establishes a formal link between resource calculi and linear multicategories, proving strong normalization and coherence results that unify morphisms in these structures through normal forms of resource terms.

Contribution

It introduces a novel correspondence between resource calculi and linear multicategories, providing new proofs of coherence and normalization results in categorical structures.

Findings

Proves strong normalization of reduction in resource calculi.

Establishes a coherence theorem for free multicategorical structures.

Provides syntactic proofs of Mac Lane's coherence theorems.

Abstract

We establish a formal correspondence between resource calculi an 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.