LIPIcs.TLCA.2015.138.pdf
- Filesize: 469 kB
- 15 pages
Document
Undecidability of Equality in the Free Locally Cartesian Closed Category
Authors
-
Part of:
Volume:
13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Typed Lambda Calculi and Applications (TLCA) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-06-15
Cite AsGet BibTex
Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TLCA.2015.138
https://doi.org/10.4230/LIPIcs.TLCA.2015.138
Abstract
We show that a version of Martin-Löf type theory with extensional identity, a unit type N1, Sigma, Pi, and a base type is a free category with families (supporting these type formers) both in a 1- and a 2-categorical sense. It follows that the underlying category of contexts is a free locally cartesian closed category in a 2-categorical sense because of a previously proved biequivalence. We then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
Keywords
- Extensional type theory
- locally cartesian closed categories
- undecidab- ility
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads