2 ms·
HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely c
by Mond_ 1y ago
HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. HoTT isn't even remotely close to being accepted as a reasonable standard, and it's kind of a non-starter for most people.
This is a bit like asking the developers of a Javascript framework why they they didn't write a framework for Elm or Haskell.
- zozbot234 1y ago> HoTT is a highly technical, highly niche topic and it doesn't make sense to tackle two ambitious projects at the same time like this. It's also a bit of a controversial topic in formalized mathematics. See the following relevant comments by Kevin Buzzard (an expert in Lean and also in the sort of abstract nonsense that might arguably benefit directly from HoTT) - Links courtesy of https://ncatlab.org/nlab/show/Kevin+Buzzard https://ncatlab.org/nlab/show/Kevin+Buzzard * Is HoTT the way to do mathematics? (2020) https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf https://www.cl.cam.ac.uk/events/owls/slides/buzzard.pdf ("Nobody knows because nobody tried") * Grothendieck's use of equality (2024) https://arxiv.org/abs/2405.10387 https://arxiv.org/abs/2405.10387 - Discussed here https://news.ycombinator.com/item?id=40414404 https://news.ycombinator.com/item?id=40414404