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 : 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