Undecidability of Equality in the Free Locally Cartesian Closed Category

Castellan, Simon; Clairambault, Pierre; Dybjer, Peter

doi:10.4230/LIPIcs.TLCA.2015.138

Document

Undecidability of Equality in the Free Locally Cartesian Closed Category

Authors Simon Castellan, Pierre Clairambault, Peter Dybjer

Part of: Volume: 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015)
Part of: Series: Leibniz International Proceedings in Informatics (LIPIcs)
Part of: Conference: International Conference on Typed Lambda Calculi and Applications (TLCA)
License: Creative Commons Attribution 3.0 Unported license
Publication Date: 2015-06-15

PDF

File

PDF

LIPIcs.TLCA.2015.138.pdf

Filesize: 469 kB
15 pages

Document Identifiers

DOI: 10.4230/LIPIcs.TLCA.2015.138
URN: urn:nbn:de:0030-drops-51602

Subject Classification

Keywords

Extensional type theory
locally cartesian closed categories
undecidab- ility

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

Abstract

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.

Cite As Get BibTex

Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 138-152, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.138

Author Details

Simon Castellan

Pierre Clairambault

Peter Dybjer

Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail