In this general survey talk, we will describe an approach to doing homotopy theory within Univalent Foundations. Whereas classical homotopy theory may be described as "analytic", our approach is synthetic in the sense that, in ``homotopy type theory", homotopical concepts such as points, paths, and homotopies are basic notions. This term, we have used this synthetic approach to give computer-checked proofs of a number of basic theorems of homotopy theory, and we will discuss examples such as homotopy groups of spheres, the Hopf fibration, and the Freudenthal Suspension theorem. Another interesting aspect of the synthetic approach is that it has led to new proofs of these results, which are often shorter and more abstract than the classical proofs, and can be applied in settings other than topological spaces, such as Quillen model categories and oo-topoi. The talk presumes no prior knowledge of homotopy type theory, and is intended for a general mathematical audience.