A type theory for cartesian closed bicategories: (Extended Abstract)

Marcelo Fiore, Philip Saville

Research output: Chapter in Book/Report/Conference proceedingConference contribution


We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal property, thereby lifting the Curry-Howard-Lambek correspondence to the bicategorical setting. Our approach is principled and practical.

Weak substitution structure is constructed using a bicategorification of the notion of abstract clone from universal algebra, and the rules for products and exponentials are synthesised from semantic considerations. The result is a type theory that employs a novel combination of 2-dimensional type theory and explicit substitution, and directly generalises the Simply-Typed Lambda Calculus. This work is the first step in a programme aimed at proving coherence for cartesian closed bicategories.
Original languageEnglish
Title of host publication2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
Subtitle of host publication24-27 June 2019 - Vancouver
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages13
ISBN (Electronic)978-1-7281-3608
ISBN (Print)978-1-7281-3609-7
Publication statusPublished - 5 Aug 2019
EventThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019


ConferenceThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2019
Internet address


  • typed lambda calculus
  • higher category theory
  • Curry-Howard-Lambek correspondence
  • cartesian closed bicategories


Dive into the research topics of 'A type theory for cartesian closed bicategories: (Extended Abstract)'. Together they form a unique fingerprint.
  • A type theory for cartesian closed bicategories

    Saville, P. & Fiore, M., 9 Jul 2019. 1 p.

    Research output: Contribution to conferenceAbstract

    Open Access

Cite this