Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)

TL;DR

This paper demonstrates that equality in a certain type-theoretic framework and its corresponding free locally cartesian closed category is undecidable, linking type theory and category theory through a reduction to combinatory logic.

Contribution

It establishes the undecidability of equality in a specific extensional type theory and its free category, connecting type-theoretic and categorical undecidability results.

Findings

Equality in the free locally cartesian closed category is undecidable.

Reduces equality undecidability to combinatory logic convertibility.

Shows similar undecidability for extensional Martin-Löf type theory with one universe.

Abstract

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.