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

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 familie…