Castellan, Simon and Clairambault, Pierre and Dybjer, Peter - Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)

lmcs:4113 - Logical Methods in Computer Science, November 30, 2017, Volume 13, Issue 4
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)

Authors: Castellan, Simon and Clairambault, Pierre and Dybjer, Peter

We show that a version of Martin-L\"of type theory with an extensional identity type former I, a unit type N1 , 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-L\"of type theory with one universe is undecidable.


Source : oai:arXiv.org:1504.03995
DOI : DOI:10.23638/LMCS-13(4:22)2017
Volume: Volume 13, Issue 4
Published on: November 30, 2017
Submitted on: November 30, 2017
Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.2


Share

Browsing statistics

This page has been seen 39 times.
This article's PDF has been downloaded 18 times.