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 higherdimensional
category theory.
In this talk I will construct a type theory for cartesian closed
bicategories, thereby lifting the wellknown correspondence between
cartesian closed categories and the SimplyTyped 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 
Related content

Research output

A type theory for cartesian closed bicategories: (Extended Abstract)
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution