We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
UNDECIDABILITY OF EQUALITY IN THE FREE LOCALLY CARTESIAN CLOSED CATEGORY (EXTENDED VERSION).
- Authors
CASTELLAN, SIMON; CLAIRAMBAULT, PIERRE; DYBJER, PETER
- Abstract
We show that a version of Martin-Löf type theory with an extensional identity type former I, a unit type N1, Σ-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.
- Subjects
ANALYTIC geometry; CARTESIAN coordinates; CURRENCY convertibility; COMBINATORY logic; NONCLASSICAL mathematical logic
- Publication
Logical Methods in Computer Science (LMCS), 2017, Vol 13, Issue 4, p1
- ISSN
1860-5974
- Publication type
Article
- DOI
10.23638/LMCS-13(4:22)2017