The fundamental theorem of category theory is the Yoneda lemma, which in its simplest form identifies natural transformations between represented functors with morphisms between the representing objects. The ∞-categorical Yoneda lemma is surprisingly hard to prove — at least in the traditional set-based foundations of mathematics. In this talk we’ll describe the experience of developing ∞-category theory in an alternate foundation system based on homotopy type theory, in which constructions determined up to a contractible space of choices are genuinely “well-defined” and elementwise mappings are automatically homotopically-coherently functorial. In this setting the proof the ∞-categorical Yoneda lemma is arguably easier than the 1-categorical Yoneda lemma. We’ll end by posing the question as to whether similar foundations would be useful for other “higher structures." This is based on joint work with Mike Shulman and involves computer formalizations written in collaboration with Nikolai Kudasov and Jonathan Weinberger.