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 |
Related content
-
Research output
-
A type theory for cartesian closed bicategories: (Extended Abstract)
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution