HoTT
Overview
Homotopy Type Theory: univalent foundations combining type theory with homotopy theory. Propositions as types; identity as path. Built on Martin-Löf Type Theory (MLTT); Voevodsky (2006–) developed univalence.
Era: 2006–2013
Proposed at: Princeton, USA
Formal structure
Domain: Types A, B : Type; terms a : A; identity type Id_A(a, b)
HoTT layers MLTT with homotopy semantics; the Univalence principle (identity vs equivalence) is documented as its own framework entry.
Constraints: Constructive: no excluded middle for arbitrary types; path induction
Objective: Foundation for math; proofs are programs (Curry–Howard)