Homotopy type theory (HoTT)

Layer 0 — Mathematicsin the logic subtree

Martin-Löf intensional type theory + univalence axiom (Voevodsky): equivalence ≃ equality. Types as ∞-groupoids; constructive foundation.