Homotopy Type Theory is a new area of research, combining ideas from topology, dependent type theory, mathematical logic and theoretical computer science. Martin-Löf introduced his dependent type theory in the 1970's. Hofmann and Streicher realized in 1998 that it has an interpretation in groupoids, which was the first hint of the higher-dimensional structure implicit in the theory. The connection between Martin-Löf's type theory and homotopy theory was first recognized around 2008, independently by Voevodsky and Warren. This discovery marks the birth of the field of Homotopy Type Theory, which has since been studied by many researchers around the world.