Coherence for Skew-Monoidal Categories

被引：10

作者：

Uustalu, Tarmo ^{[1
]}

机构：

[1] Tallinn Univ Technol, Inst Cybernet, Tallinn, Estonia

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2014年 / 153期

关键词：

D O I：

10.4204/EPTCS.153.5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

I motivate a variation (due to K. Szlachanyi) of monoidal categories called skew-monoidal categories where the unital and associativity laws are not required to be isomorphisms, only natural transformations. Coherence has to be formulated differently than in the well-known monoidal case. In my ( to my knowledge new) version, it becomes a statement of uniqueness of normalizing rewrites. I present a proof of this coherence theorem and also formalize it fully in the dependently typed programming language Agda.

引用

页码：68 / 77

页数：10

共 15 条

[1] Monads Need Not Be Endofunctors
Altenkirch, Thorsten
Chapman, James
Uustalu, Tarmo
[J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, PROCEEDINGS, 2010, 6014 : 297 - +
[2] Categorification, term rewriting and the Knuth-Bendix procedure
Beke, Tibor
[J]. JOURNAL OF PURE AND APPLIED ALGEBRA, 2011, 215 (05) : 728 - 740
[3] Beylin I, 1996, LECT NOTES COMPUT SC, V1158, P47
[4] Categories for computation in context and unified logic
Blute, RF
Cockett, JRB
Seely, RAG
[J]. JOURNAL OF PURE AND APPLIED ALGEBRA, 1997, 116 (1-3) : 49 - 98
[5] Buckley M., 2013, ARXIV13070265
[6] Burroni A., 1971, CAH TOP GEOM DIF, V12, P215
[7] Kelly G. M., 1964, J ALGEBRA, V1, P397
[8] Lack S., 2013, ARXIV13024488
[9] Lack S, 2012, THEOR APPL CATEG, V26, P385
[10] Lane Saunders Mac, 1963, RICE I PAMPHLET RICE, V49, P28

← 1 2 →