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

Marcelo Fiore, Philip Saville

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationLICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science
Place of PublicationNew York
PublisherACM
Pages425–439
Number of pages15
ISBN (Electronic)9781450371049
DOIs
Publication statusPublished - 8 Jul 2020
EventThirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science - Saarbrücken, Germany
Duration: 8 Jul 202011 Jul 2020
http://lics.siglog.org/lics20/

Conference

ConferenceThirty-Fifth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2020
Country/TerritoryGermany
CitySaarbrücken
Period8/07/2011/07/20
Internet address

Keywords / Materials (for Non-textual outputs)

  • bicategories
  • cartesian closure
  • coherence
  • type theory
  • normalisation
  • normalisation-by-evaluation

Fingerprint

Dive into the research topics of 'Coherence and normalisation-by-evaluation for bicategorical cartesian closed structure'. Together they form a unique fingerprint.

Cite this