2026-07-25T21:47:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5160 2024-03-06T10:36:10Z ddc:004 open_access

Undecidability of Equality in the Free Locally Cartesian Closed Category Castellan, Simon Clairambault, Pierre Dybjer, Peter Extensional type theory locally cartesian closed categories undecidab- ility 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Simon Castellan and Pierre Clairambault and Peter Dybjer 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.138 urn:nbn:de:0030-drops-51602 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.138 eng https://creativecommons.org/licenses/by/3.0/legalcode