Undecidability of Equality in the Free Locally Cartesian Closed Category

Simon Castellan, Pierre Clairambault, Peter Dybjer. Undecidability of Equality in the Free Locally Cartesian Closed Category. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland. Volume 38 of LIPIcs, pages 138-152, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. [doi]

@inproceedings{CastellanCD15,
  title = {Undecidability of Equality in the Free Locally Cartesian Closed Category},
  author = {Simon Castellan and Pierre Clairambault and Peter Dybjer},
  year = {2015},
  doi = {10.4230/LIPIcs.TLCA.2015.138},
  url = {http://dx.doi.org/10.4230/LIPIcs.TLCA.2015.138},
  researchr = {https://researchr.org/publication/CastellanCD15},
  cites = {0},
  citedby = {0},
  pages = {138-152},
  booktitle = {13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015, Warsaw, Poland},
  editor = {Thorsten Altenkirch},
  volume = {38},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-87-3},
}