Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure
| Autor: | Marcelo Fiore, Philip Saville |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
bicategories
Computer science Structure (category theory) 5003 Philosophy 4904 Pure Mathematics Yoneda lemma Mathematical proof Bicategory coherence normalisation Algebra Cartesian closed category 50 Philosophy and Religious Studies type theory Mathematics::Category Theory cartesian closure 49 Mathematical Sciences normalisation-by-evaluation Lambda calculus Category theory computer computer.programming_language Normalisation by evaluation |
| Zdroj: | LICS Fiore, M & Saville, P 2020, Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure . in LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science . New York, pp. 425–439, Thirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, 8/07/20 . https://doi.org/10.1145/3373718.3394769 |
| DOI: | 10.17863/cam.57511 |
| Popis: | We present two proofs of coherence for cartesian closed bicat- egories. 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 signif- icantly more complex than its 1-categorical counterpart. It also opens the way for further proofs of coherence using (adaptations of) tools from categorical semantics. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|