I am only a beginner in the field of type theory, and I'm wondering if the community could point me out a few open problems in the field. I have a good background in logic, in particular, proof theory and I have a reasonable knowledge on category theory. While I am interested in homotopy type theory, I'd like to receive answers that point to flavors of type theory other than HoTT because open problems in HoTT are not difficult to find on the web (problems in HoTT are still welcome though). This is my very first question in this site so please feel free to edit, point mistakes and criticize my question.


Thank you for your attention!



Open problems in type theory
Thierry Coquand has a list of open problems, based on Vladimir Voevodsky's research on Dependent Type Theory. Scroll to the end of this [presentation.](https://web.archive.org/web/20190518164032/https://eutypes.cs.ru.nl/eutypes_pmwiki/uploads/Meetings/Coquand.pdf)


And I presume you know the HoTT open problem list at [nLab](https://ncatlab.org/nlab/show/open+problems+in+homotopy+type+theory).


