论文标题
严格和连贯性的弦图
String diagrams for Strictification and Coherence
论文作者
论文摘要
尽管对严格的单体类别的弦乐图有充分的理解，并且在计算机科学的几个领域中发现了应用，但研究的图形形式主义的研究较少。在本文中，我们通过发电机和非图案单体类别的字符串图的关系提供了演讲，并展示了该构造如何处理诸如数字电路和编程语言之类的域中的应用程序。我们证明了我们的构建的正确性，这提供了Mac Lane严格定理的新颖证明。这反过来又导致了Mac Lane相干定理的基本图形证明，特别是允许在单型类别中的典型同构的感应构造。
Whereas string diagrams for strict monoidal categories are well understood, and have found application in several fields of Computer Science, graphical formalisms for non-strict monoidal categories are far less studied. In this paper, we provide a presentation by generators and relations of string diagrams for non-strict monoidal categories, and show how this construction can handle applications in domains such as digital circuits and programming languages. We prove the correctness of our construction, which yields a novel proof of Mac Lane's strictness theorem. This in turn leads to an elementary graphical proof of Mac Lane's coherence theorem, and in particular allows for the inductive construction of the canonical isomorphisms in a monoidal category.
