Simon Castellan ; Pierre Clairambault ; Peter Dybjer - 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 - https://doi.org/10.23638/LMCS-13(4:22)2017
Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)Article

Authors: Simon Castellan ; Pierre Clairambault ; Peter Dybjer

    We show that a version of Martin-Löf 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öf type theory with one universe is undecidable.


    Volume: Volume 13, Issue 4
    Published on: November 30, 2017
    Accepted on: November 30, 2017
    Submitted on: November 30, 2017
    Keywords: Computer Science - Logic in Computer Science,F.4.1,F.3.2

    Consultation statistics

    This page has been seen 2008 times.
    This article's PDF has been downloaded 542 times.