Repository logo
 

Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure

Accepted version
Peer-reviewed

Type

Conference Object

Change log

Authors

Saville, Philip 

Abstract

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.

Description

Keywords

5003 Philosophy, 4904 Pure Mathematics, 49 Mathematical Sciences, 50 Philosophy and Religious Studies

Journal Title

Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Conference Name

LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science

Journal ISSN

Volume Title

Publisher

ACM

Rights

All rights reserved