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

Marcelo Fiore, Philip Saville

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

Abstract

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)
Pages1-13
Number of pages13
ISBN (Electronic)978-1-7281-3608
ISBN (Print)978-1-7281-3609-7
DOIs
Publication statusPublished - 5 Aug 2019
EventThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science - Vancouver, Canada
Duration: 24 Jun 201927 Jun 2019
http://lics.siglog.org/lics19/index.php

Conference

ConferenceThirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated titleLICS 2019
Country/TerritoryCanada
CityVancouver
Period24/06/1927/06/19
Internet address

Keywords

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

Fingerprint

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