@conference{17a7cb9db61447b2833839d007cd1f0b,
title = "A type theory for cartesian closed bicategories",
abstract = "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 {\textquoteleft}up to isomorphism{\textquoteright} 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.",
author = "Philip Saville and Marcelo Fiore",
year = "2019",
month = jul,
day = "9",
language = "English",
note = "Category Theory 2019, CT 2019 ; Conference date: 07-07-2019 Through 13-07-2019",
url = "http://conferences.inf.ed.ac.uk/ct2019/",
}