Syntax and Semantics for Martin-Lof Type Theory and Homotopy Type Theory

An overview of the core syntax of Martin-L"of type theory (MLTT) and its semantics in homotopy type theory (HoTT).

Note: This is a chapter in the author's forthcoming book {\em Probability, Intuition, and Common Sense}.