Homotopy type theory + univalence (Voevodsky)

Layer 0 — Mathematicsin the proof-theory subtree

Voevodsky 2010-13 / HoTT-Book 2013. Type-theory with homotopical-interpretation. Univalence-axiom: equivalent-types are equal. Foundational alternative to ZFC.