**A foundations of mathematics for the 21st century.**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!

#spnetwork #homotopytheory #ncategories #logic #foundations