Back to Search
Start Over
UNDECIDABILITY OF EQUALITY IN THE FREE LOCALLY CARTESIAN CLOSED CATEGORY (EXTENDED VERSION).
- Source :
- Logical Methods in Computer Science (LMCS); 2017, Vol. 13 Issue 4, p1-38, 38p
- Publication Year :
- 2017
-
Abstract
- We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N<subscript>1</subscript>, Σ-types, Π-types, 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 show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic. Essentially the same construction also shows a slightly strengthened form of the result that equality in extensional Martin-Löf type theory with one universe is undecidable. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 18605974
- Volume :
- 13
- Issue :
- 4
- Database :
- Complementary Index
- Journal :
- Logical Methods in Computer Science (LMCS)
- Publication Type :
- Academic Journal
- Accession number :
- 126992514
- Full Text :
- https://doi.org/10.23638/LMCS-13(4:22)2017