This article introduces basics of type theory, focusing on the algebraic side. The main references are the "Homotopy Type Theory" book.