The mathematician Alexander Borovik speaks of the importance of the 'vertical unity' of mathematics. By this he means to draw our attention to the fact that many sophisticated mathematical concepts, even those introduced at the cutting-edge of research, have their roots in our most basic conceptualisations of the world. If this is so, we might expect any truly fundamental mathematical language to detect such structural commonalities. It is reasonable to suppose then that the lack of philosophical interest in such vertical (...) unity is related to the prominence given by philosophers to languages which do not express well such relations. In this chapter, I suggest that we look beyond set theory to the newly emerging homotopy type theory, which makes plain what there is in common between very simple aspects of logic, arithmetic and geometry and much more sophisticated concepts. (shrink)