4 ms·
I thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher induc
by kmicklas 12y ago
I thought this was more or less solved with the recent developments on the cubical sets models? There is even a toy interpreter with univalence and higher inductives:
https://github.com/simhu/cubical https://github.com/simhu/cubical
- jonsterling 12y agoThey've done a lot of good work, but it's not quite done yet. The original conjecture has not been answered in the affirmative, and there are also further questions...