4 ms·
Homotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins
by jkhdigital 5y ago
Homotopy type theory is just that: https://www.ias.edu/ideas/2014/voevodsky-origins https://www.ias.edu/ideas/2014/voevodsky-origins
- deadbeef57 5y agoHomotopy type theory (HoTT) can mean several things: it's a new foundation of mathematics that was developed from the start with computer-formalization in mind. But you can also work on HoTT without ever touching a computer. Conversely, there are many ways to do computer-formalization of mathematics, without every doing anything with HoTT.