This sequence of posts is an introduction to Martin-Löf dependent type theory, based on the book Homotopy Type Theory (usually called HoTT), but without the homotopy part. These posts describe how to set up type theory as an alternative foundation of mathematics, in place of set theory.

Prior knowledge of set theory is required.