We show that a version of Martin-Löf type theory with extensional identity, a unit type N1, Sigma, Pi, 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 then show that equality in this category is undecidable by reducing it to the undecidability of convertibility in combinatory logic.
@InProceedings{castellan_et_al:LIPIcs.TLCA.2015.138, author = {Castellan, Simon and Clairambault, Pierre and Dybjer, Peter}, title = {{Undecidability of Equality in the Free Locally Cartesian Closed Category}}, booktitle = {13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)}, pages = {138--152}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-87-3}, ISSN = {1868-8969}, year = {2015}, volume = {38}, editor = {Altenkirch, Thorsten}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138}, URN = {urn:nbn:de:0030-drops-51602}, doi = {10.4230/LIPIcs.TLCA.2015.138}, annote = {Keywords: Extensional type theory, locally cartesian closed categories, undecidab- ility} }
Feedback for Dagstuhl Publishing