Abstract

Cartesian closed bicategories arise in categorical logic, categorical algebra and game semantics, and may be thought of as cartesian closed categories ‘up to isomorphism’. In this talk I shall outline a proof of a sharp form of coherence, namely that in the free cartesian closed bicategory on a set there is at most one 2-cell between any parallel pair of 1-cells. Thus, there is at most one structural isomorphism between any pair of 1-cells in a cartesian closed bicategory. My focus will be on the proof stategy, which recasts a technique from categorical semantics as a tool for proving coherence. I use a version of normalisation-by-evaluation, first employed to prove normalisation of the simply-typed lambda calculus [1], applied to a type theory satisfying suitable properties. In particualar, I adapt Fiore’s categorical reconstruction of the technique [2] which, as we shall see, is particularly amenable to being translated into a bicategorical argument.

I shall assume the usual Lambek-style semantics of the simply-typed lambda calculus, but not any background in bicategory theory.

Joint work with Marcelo Fiore