Repository logo

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

Accepted version


Conference Object

Change log


Saville, Philip 


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.



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




All rights reserved