In 2013, three dozens of today's brightest minds have just laid out new foundation of mathematics after a year of collective effort. This new paradigm better fits both informal and computationally-checkable mathematics. There is little doubt that it will fundamentally change our perspective on rigorous knowledge, and it could be that, in a few decades, the book they published turns out to be the bedrock of all mathematics, and, by extension, all human knowledge! Have a primer of this upcoming revolution, with this article on type theory, the theory that the book builds upon!