In the Univalent Foundations of mathematics spatial notions like “point” and “path” are primitive, rather than derived, and all of mathematics is encoded in terms of them. A Homotopy Type Theory is any formal system which realizes this idea. In this paper I will focus on the question of whether a Homotopy Type Theory can be justified intuitively as a theory of shapes in the same way that ZFC can be justified intuitively as a theory of collections. I first clarify (...) what such an “intuitive justification” should be by distinguishing between formal and pre-formal “meaning explanations” in the vein of Martin-Löf. I then go on to develop a pre-formal meaning explanation for HoTT in terms of primitive spatial notions like “shape”, “path” etc. (shrink)

In a paper published in 1939, Ernest Nagel described the role that projective duality had played in the reformulation of mathematical understanding through the turn of the nineteenth century, claiming that the discovery of the principle of duality had freed mathematicians from the belief that their task was to describe intuitive elements. While instances of duality in mathematics have increased enormously through the twentieth century, philosophers since Nagel have paid little attention to the phenomenon. In this paper I will argue (...) that a reassessment is overdue. Something beyond doubt is that category theory has an enormous amount to say on the subject, for example, in terms of arrow reversal, dualising objects and adjunctions. These developments have coincided with changes in our understanding of identity and structure within mathematics. While it transpires that physicists have employed the term ‘duality’ in ways which do not always coincide with those of mathematicians, analysis of the latter should still prove very useful to philosophers of physics. Consequently, category theory presents itself as an extremely important language for the philosophy of physics. (shrink)