John Baez on Google+: It's here! For decades, mathematicians been dreaming of an approach to math where different proofs that x = y can be seen as different paths in a space. It's finally been made precise, thanks to Vladimir Voevodsky and a gang of mathematicians who holed up for a year at the Institute for Advanced Studies, at Princeton. I won't try to explain it, since that's what the book does. I'll just mention a few of the radical new features: * It includes set theory as a special case, but it's founded on more general things called 'types'. Types include sets, but also propositions. Proving a proposition amounts to constructing an element of a certain type. So, proofs are no longer 'outside' the mathematics being discussed, they're inside it just like everything else. * The logic is 'constructive', meaning that to prove something exists amounts to giving a procedure for constructing it. As a result, the whole system can be and is being computerized with the help of programs like COQ and AGDA. * Types can be seen as 'spaces', and their elements as 'points'. A proof that two elements of a type are equal can be seen as constructing a path between two points. Sets are just a special case: the '0-types', which have no interesting higher-dimensional aspect. There are also types that look like spheres and tori! Technically speaking, the branch of topology called homotopy theory is now a part of logic! That's why the subject is called homotopy type theory. * Types can also be seen as infinity-groupoids. Very roughly, these are structures with elements, isomorphisms between elements, isomorphisms between isomorphisms, and so on ad infinitum. So, a certain chunk of the important new branch of math called 'higher category theory' is now part of logic, too. * The most special contribution of Voevodsky is the univalence axiom. Very very roughly, this expands the concept of 'equality' so that it's just as general as the hitherto more flexible concept of 'isomorphism' - or, if you know some more fancy math, 'equivalence'. Mathematicians working on homotopy theory and higher category theory have known for decades that equality is too rigid a concept to be right - for certain applications. The univalence axiom updates our concept of equality so that it's good again! Since this is all about foundations, and it's all quite new, please don't ask me yet what its practical applications are. Ask me in a hundred years. For now, I can tell you that this is the 'upgrade' that the foundations of math has needed ever since the work of Grothendieck. It's truly 21-century math. It's also a book for the 21st century, because it's escaped the grip of expensive publishers! While it's 600 pages long, a hardback copy costs less than $27. Paperback costs less than $18, and an electronic copy is free! http://homotopytypetheory.org/book/