Martin-Löf type theory

Layer 0 — Mathematicsin the proof-theory subtree

Martin-Löf 1972-84 intuitionistic type theory: dependent + inductive types + universe-polymorphism + identity-types. Foundation of Coq + Agda + Lean proof-assistants.