alt Hacker NewsMakes me sad that the homotopical foundation people never got their shit together and now formalization is so mature but it's still done in set theoretic foundations.
Replies
HappyPanacea • today at 12:06 AM
The stronger AI become the easier it should be to develop and move to alternative foundations.
we are moving forward steadily :) https://github.com/marcinjangrzybowski/cubical-bis/blob/inte... (see table in the middle of doc) mind, that it is fully constructive implementation, you can get arbitrary precision aproximation to every real expression. for now WIP, but soon will be aviable in cubical-library :) also our related TYPES2026 presentation: https://types2026.cse.chalmers.se/slides/51.pdf