A type theory for cartesian closed bicategories

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.