Tag Archives: Type Theory

Univalent Foundations of Mathematics

April 21, 2014Article2342 vuesEdit
In an effort to make mathematics more computable, a consortium of today's greatest mathematicians have laid out new foundations. Amazingly, they all lie upon one single axiom, called univalence. The goal of this axiom is to make formal mathematics more similar to informal mathematics. With univalence, our Arabic numbers aren't just like natural numbers; They are natural numbers. Univalence also has unforeseen and mesmerizing consequences.

Homotopy Type Theory and Higher Inductive Types

April 06, 2014Article2003 vuesEdit
In this article, we explore the possibilities allowed by higher inductive types. They enable a much more intuitive formalization of integers and new mind-blowing definitions of the (homotopical) circle and sphere.

Type Theory: A Modern Computable Paradigm for Math

March 20, 2014Article8264 vuesEdit
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!