Back to Search Start Over

UNDECIDABILITY OF EQUALITY IN THE FREE LOCALLY CARTESIAN CLOSED CATEGORY (EXTENDED VERSION).

Authors :
CASTELLAN, SIMON
CLAIRAMBAULT, PIERRE
DYBJER, PETER
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