A type theory for cartesian closed bicategories

Philip Saville, University of Cambridge. Part of the proofs, constructions and computations seminar series.

Bicategories (categories "up to isomorphism") are a natural setting for the study of many categorical phenomena, especially where composition of morphisms is defined by universal properties. The downside to this generality is that working in a bicategory can entail a great deal of calculation with canonical isomorphisms. The calculations generally work out as expected, but require complex and often tedious checks. The work I will present is the first part of a programme for tackling this problem in the case of cartesian closed bicategories, examples of which appear in categorical algebra, game semantics, and higher-dimensional category theory.

In this talk, I will construct a type theory for cartesian closed bicategories, thereby lifting the well-known correspondence between cartesian closed categories and the Simply-Typed Lambda Calculus to the bicategorical world. I will outline the principles underlying the construction of the type theory, and sketch a proof that it satisfies the required universal property. If time permits, I will describe some work in progress using this type theory to prove a coherence result for cartesian closed bicategories. This is joint work with Professor Marcelo Fiore.