Name
Title | ||
|---|---|---|
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version). |
Abstract | ||
|---|---|---|
We show that a version of Martin-Lof type theory with an extensional identity type former I, a unit type N-1, Sigma-types, Pi-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-Lof type theory with one universe is undecidable. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.23638/LMCS-13(4:22)2017 | LOGICAL METHODS IN COMPUTER SCIENCE |
Keywords | Field | DocType |
Extensional Type Theory,Undecidability,Locally Cartesian Closed Categories | Complete category,Discrete mathematics,Enriched category,Opposite category,Closed category,2-category,Concrete category,Cartesian closed category,Category of sets,Mathematics | Journal |
Volume | Issue | ISSN |
13 | 4 | 1860-5974 |
Citations | PageRank | References |
1 | 0.37 | 4 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Simon Castellan | 1 | 27 | 5.82 |
| Pierre Clairambault | 2 | 68 | 13.25 |
| Peter Dybjer | 3 | 540 | 76.99 |