A type theory for cartesian closed bicategories

Philip Saville, Marcelo Fiore

Research output: Contribution to conferenceAbstract

Abstract / Description of output

I will introduce an internal language for cartesian closed bicategories, explainingits underlying design principles. Firstly, I will begin with a type theory for bicategories synthesised from a bicategorification of the notion of abstract clone from universal algebra. The result is a 2-dimensional type theory (in the style of Hilken) with aform of explicit substitution capturing an ‘up to isomorphism’ composition operation. Next, I shall show how semantic considerations give rise to the addition of product andexponential type structures. The resulting type theory generalises the Simply-Typed Lambda Calculus and its syntactic models satisfy a suitable 2-dimensional freeness universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. If time permits, I will conclude by sketching a bicategorical generalisation of the categorical normalisation-by-evaluation argument of Fiore to prove a conjectured coherence result for cartesian closed bicategories.
Original languageEnglish
Number of pages1
Publication statusPublished - 9 Jul 2019
EventCategory Theory 2019 - University of Edinburgh, Edinburgh, United Kingdom
Duration: 7 Jul 201913 Jul 2019


WorkshopCategory Theory 2019
Abbreviated titleCT 2019
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'A type theory for cartesian closed bicategories'. Together they form a unique fingerprint.

Cite this