Coherence for cartesian closed bicategories, via normalisation-by-evaluation

Philip Saville ( University of Edinburgh )

Cartesian closed bicategories, which can be thought of cartesian closed categories 'up to coherent isomorphism', arise in logic, categorical algebra, and game semantics. However, calculations in such settings can quickly get bogged down in long calculations with the structural data. In this talk I will sketch an argument showing cartesian closed bicategories are coherent, in the sense that there is at most one 2-cell between any parallel pair of morphisms. The proof involves a bicategorification of Fiore's categorical treatment of normalisation-by-evaluation for the simply-typed lambda calculus and, in principle, allows one to extract a 'normal form' for every 2-cell in the free cartesian closed bicategory. I will aim to highlight the ways in which the bicategorical proof builds on the categorical one, and draw on this to suggest routes for future coherence proofs. No background in bicategories or higher category theory will be assumed.

Joint work with Marcelo Fiore, University of Cambridge.

Say hello from 1400, talk will start at 1405.