Homotopy type theory is a young field at the interface between mathematics, logic, and computer science. It studies a variety of connections between algebraic topology (more precisely, homotopy theory) and dependent type theory (a class of formal systems extensively studied in logic and computer science).  In this talk I will focus on the aspect of homotopy type theory called "synthetic homotopy theory", whose aim is to use the language of dependent type theory in order to study homotopy theory. I will introduce the main concepts and show various examples of theorems from homotopy theory that we can prove in this setting.