Kaposi, Ambrus ;
Huber, Simon ;
Sattler, Christian
Gluing for Type Theory
Abstract
The relationship between categorical gluing and proofs using the logical relation technique is folklore. In this paper we work out this relationship for Martin-Löf type theory and show that parametricity and canonicity arise as special cases of gluing. The input of gluing is two models of type theory and a pseudomorphism between them and the output is a displayed model over the first model. A pseudomorphism preserves the categorical structure strictly, the empty context and context extension up to isomorphism, and there are no conditions on preservation of type formers. We look at three examples of pseudomorphisms: the identity on the syntax, the interpretation into the set model and the global section functor. Gluing along these result in syntactic parametricity, semantic parametricity and canonicity, respectively.
BibTeX - Entry
@InProceedings{kaposi_et_al:LIPIcs:2019:10532,
author = {Ambrus Kaposi and Simon Huber and Christian Sattler},
title = {{Gluing for Type Theory}},
booktitle = {4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
pages = {25:1--25:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-107-8},
ISSN = {1868-8969},
year = {2019},
volume = {131},
editor = {Herman Geuvers},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10532},
URN = {urn:nbn:de:0030-drops-105323},
doi = {10.4230/LIPIcs.FSCD.2019.25},
annote = {Keywords: Martin-L{\"o}f type theory, logical relations, parametricity, canonicity, quotient inductive types}
}
|
Keywords: |
|
Martin-Löf type theory, logical relations, parametricity, canonicity, quotient inductive types |
|
Seminar: |
|
4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)
|
|
Issue date: |
|
2019 |
|
Date of publication: |
|
2019 |
2019
