3 ms·
This is interesting. What are the prerequisites to understand Univalent Foundations and how active is it?
by jeff76 8y ago
This is interesting. What are the prerequisites to understand Univalent Foundations and how active is it?
- bbeonx 8y agoLook into the Coq language, it is under active development and there is a lot of work going into it. Voevodsky was working in Coq, if I recall. As to how hard it is to learn, you will have to learn a pretty decent amount. It all depends on your background. If you know what the Curry Howard correspondence is, you are in relatively good shape. If you've never heard of lambda calculus or first order logic, you may have some more work cut out for you. Here is a nice article I read last night on explaining the move from set theory to type theory. It gets a bit technical but you might be able to get something from it. https://golem.ph.utexas.edu/category/2013/01/from_set_theory_to_type_theory.html https://golem.ph.utexas.edu/category/2013/01/from_set_theory...
- alimw 8y agoIf you're specifically interested in Univalent Foundations, just read the book. https://homotopytypetheory.org/book/ https://homotopytypetheory.org/book/