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...
