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.