By combining the univalence axiom with higher inductive types, it becomes possible to reproduce theorems of classical homotopy theory as formal results inside homotopy type theory. This sort of "synthetic homotopy theory" generally uses ideas from classical homotopy theory, but its methods and techniques are often different due to the differences between types and classical spaces - notably, that types have no "underlying sets". This minicourse will be an introduction to some of the ideas and methods of synthetic homotopy theory, some of its basic results, and how it differs from classical homotopy theory. I will assume some acquaintance, but not necessarily expertise, with basic ideas of homotopy type theory, such as equivalences, n-types, the univalence axiom, and higher inductive types, such as from reading the first few chapters of the Homotopy Type Theory book.