At its current state of the art, ∞-category theory is challenging to explain even to specialists in closely related mathematical areas. Nevertheless, historical experience suggests that in, say, a century's time, we will routinely teach this material to undergraduates. This talk describes one dream about how this might come about --- under the assumption that 22nd century undergraduates have absorbed the background intuitions of homotopy type theory/univalent foundations. To illustrate the utility of this alternate foundational system, we'll share a new computer formalized proof of the ∞-categorical Yoneda lemma that reveals how close it is to the classical proof of the 1-categorical Yoneda lemma.