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.