A type theory for cartesian closed bicategories

Description

Invited talk for the Proofs, Constructions and Computations Seminar, University of Leeds.

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 property. 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.

Period	8 May 2019
Held at	University of Leeds, United Kingdom