Spatial Types
While modalities relate directly to the philosophical concerns of metaphysicians, it has been recognized recently by mathematicians that operators behaving similarly can be deployed to capture spatial concepts synthetically. Drawing on the important ideas of Lawvere on cohesion, it can be shown that a collection of entities behaves as spaces merely by partaking in an interlocking series of maps to and from some base collection. In simplest terms, the points of a space are held together cohesively. Combining the spatial modalities with the refined notion of identity is just what is needed in current fields of mathematical geometry and topology. While standard set-theoretic foundations have brought with them a decline of philosophical interest in what constitutes the geometric, versions of geometry in mathematics have burgeoned. Now we can use cohesive HoTT to revive the philosophy of geometry and say what is distinctive about our conceptions of space.