## 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.

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 language | English |
---|---|

Title of host publication | Foundations of Software Science and Computation Structures |

Subtitle of host publication | International Conference on Foundations of Software Science and Computation Structures FoSSaCS 2020 |

Publisher | Springer |

Number of pages | 22 |

ISBN (Electronic) | 978-3-030-45231-5 |

ISBN (Print) | 978-3-030-45230-8 |

DOIs | |

Publication status | Published - 17 Apr 2020 |

Event | 23rd International Conference on Foundations of Software Science and Computation Structures - Dublin, Ireland Duration: 25 Apr 2020 → 30 Apr 2020 Conference number: 23 https://etaps.org/2020/fossacs |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer, Cham |

Volume | 12077 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Conference

Conference | 23rd International Conference on Foundations of Software Science and Computation Structures |
---|---|

Abbreviated title | FoSSaCS 2020 |

Country | Ireland |

City | Dublin |

Period | 25/04/20 → 30/04/20 |

Internet address |

## Keywords

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