We'll begin by asking innocent questions; we'll confront the wildness of our assumptions; we'll build mathematics by abstacting epistemological principles in place of grand metaphysical assumptions; and we'll find out that the stuff of reason is space.
We'll abstract human judgement and find that, "it's full of stars."
Homotopy Type Theory is a new foundations for mathematics. HoTT synthesizes the intuitionism of Brouwer, Martin Lof's type theory ( a formal syntax for constructive mathematical reasoning ), Voevodsky's "construction" of a "small universe", Kant's contaposition of analytic and synthetic reason, and the Yoneda Lemma.
An Idiosyncratic Introduction to Homotopy Type Theory and Synthetic Algebraic Topology