Activity: Academic talk or presentation types › Invited talk

Invited speaker

8 May 2019

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.

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.

University of Leeds

ID: 122325267