/sci/ - Science & Math

>>12596413
I got just the thing for you

Should I read it /sci/?

>>11539096

This is a really great book to read if you've never touched type theory before because it challenges your understanding of math.

Something that I think few mathematicians realize is that ZF set theory is obsolete as a foundation for mathematics. Although ZF set theory can not be replaced by Martin-Lof type theory because it's not as useful for many practical purposes, TT is much more theoretically appealing.

The main advantage is that proofs and theorems are actually objects within martin-lof type theory. You were taught "In set theory everything is a set," but if you ask "what is a proof?" the answer is "not a set." Type theory solves this problem. Proofs and theorems are objects in type theory.

H O T T
O
T
T

What do I need to know to be able to work through this book?

homotopies

>>6605153
Computer science has deep connections to set theory and mathematical logic, and other foundational systems such as type theory.
Homotopy type theory is an important new foundational system with very close ties to computer science - particularly in proof assistance and automated proof checking. As the name suggests, this theory combines type theory with algebraic topology - particularly abstract, categorical homotopy theory.
You can't be working on the HoTTest new topic in computational proof assistance without a deep understanding of Quillen's theory of model categories.

Some time ago I starter reading HoTT but it seemed too difficult for me so I dropped it. I can say that I didn't understand most of the introduction. Should I try again harder? Is it worth it? Would I get any useful knowledge from it? What do I need to know in order to understand this book?