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.
And I presume you know the HoTT open problem list at nLab.
Carlo Beenakker
- 188.2k
- 18
- 448
- 651