Relative full completeness for bicategorical cartesian closed structure

Philip Saville, Marcelo Fiore

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

Abstract

The glueing construction, defined as a certain comma category, is an important tool for reasoning about type theories, logics, and programming languages. Here we extend the construction to accommodate ‘2-dimensional theories’ of types, terms between types, and rewrites between terms. Taking bicategories as the semantic framework for such systems, we define the glueing bicategory and establish a bicategorical version of the well-known construction of cartesian closed structure on a glueing category. As an application, we show that free finite-product bicategories are fully complete relative to free cartesian closed bicategories, thereby establishing that the higher-order equational theory of
rewriting in the simply-typed lambda calculus is a conservative extension
of the algebraic equational theory of rewriting in the fragment with finite
products only.
Original languageEnglish
Title of host publicationFoundations of Software Science and Computation Structures
Subtitle of host publicationInternational Conference on Foundations of Software Science and Computation Structures FoSSaCS 2020
PublisherSpringer
Number of pages22
ISBN (Electronic)978-3-030-45231-5
ISBN (Print)978-3-030-45230-8
DOIs
Publication statusPublished - 17 Apr 2020
Event23rd International Conference on Foundations of Software Science and Computation Structures - Dublin, Ireland
Duration: 25 Apr 202030 Apr 2020
Conference number: 23
https://etaps.org/2020/fossacs

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
Volume12077
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference23rd International Conference on Foundations of Software Science and Computation Structures
Abbreviated titleFoSSaCS 2020
CountryIreland
CityDublin
Period25/04/2030/04/20
Internet address

Keywords

  • glueing
  • bicategories
  • cartesian closure
  • relative full completeness
  • rewriting
  • type theory
  • conservative extension

Fingerprint Dive into the research topics of 'Relative full completeness for bicategorical cartesian closed structure'. Together they form a unique fingerprint.

Cite this