Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure
LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science Saarbrücken Germany July, 2020(2020)
摘要
We present two proofs of coherence for cartesian closed bicategories. Precisely, we show that in the free cartesian closed bicategory on a set of objects there is at most one structural 2-cell between any parallel pair of 1-cells. We thereby reduce the difficulty of constructing structure in arbitrary cartesian closed bicategories to the level of 1-dimensional category theory. Our first proof follows a traditional approach using the Yoneda lemma. For the second proof, we adapt Fiore's categorical analysis of normalisation-by-evaluation for the simply-typed lambda calculus. Modulo the construction of suitable bicategorical structures, the argument is not significantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics.
更多查看译文
关键词
bicategories, cartesian closure, coherence, type theory, normalisation, normalisation-by-evaluation
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要