Homotopy Types

A further innovation is the introduction of an intensional type theory. Here one need not reduce equivalence to mere identity. How two entities are the same tells us more than whether they are the same. This is explained by the homotopical aspect of HoTT, where types are taken to resemble spaces of points, paths, paths between paths, and so on. This allows us to rethink Russell’s definite descriptions. Mathematicians use a ‘generalized the’ in situations where it appears that they might be talking about a multiplicity of instances, but there is essentially a unique instance. Taken together with the ‘univalence axiom’ there results a language in which anything that can be said of a type can be said of an equivalent type. This allows homotopy type theory to become the language of choice for a structuralist, avoiding the need for any kind of abstraction away from multiple instantiations.

Modal Types

Modal logic flourished throughout the twentieth century. Kripke provided a semantics in terms of possible world recognized by mathematicians to be an example of varying sets. This allows a formulation in terms of monads generated by adjunctions. Modal homotopy type theory adds the radical idea that modalities apply to all types, not just propositions, so as to make sense of possible steps and necessary ingredients. The proximity is shown between the structures discovered by modal logicians and common ideas in mathematics of stability under variation. We can then reformulate many ideas in current philosophical metaphysical uses of modal logic, such as rigid designators, counterparts, the de re/de dicto distinction, and so on. Worlds are understood as extended contexts, allowing a formulation of counterfactuals. A form of temporal logic is also easily generated in the same vein.

Dependent Types

Type theory regards individuals as belonging to a specific type. In computer science type-checking measures ensure that a program will compute properly. We see typing in everyday speech too, when a ‘Who?’ question expects a person. To define a type, it is necessary to specify when two elements are equal. Such concerns with sorts and identity are at stake in metaphysics. A dependent type occurs where one type is parametrized by elements of another. The two related constructions of dependent sum and dependent product appear in natural language and modern mathematics. In logic, these constructions amount to the quantifiers central to Russell’s logic. Dependent types are formulated in terms of contexts constructed in an order, showing how some concepts presuppose others. There are strong resonances with the ideas of Collingwood. With the notion of dependency, we can now analyse event types properly, demonstrating their difference from object types.

A Path to a New Logic

This chapter explains how modal homotopy type theory combines ideas from two currents of thought: type theory and category theory. Despite what might appear to be rather different philosophical starting points, there has emerged an intrinsically structuralist language of great interest to computer scientists, mathematicians and physicists. This in itself should be enough to interest philosophers in the language, but further motivation is provided by addressing some of the kinds of objection raised to formalization in philosophy; in particular, those from ordinary language philosophy which emphasize the elasticity and context-dependence of natural language. We see that several of their concerns, such as that the definitional and descriptive uses of ‘is’ are conflated in logic, are addressed by the type theory. The prospect is then presented of an opportunity to use the new language to explore key issues in philosophy of mathematics, philosophy of language and metaphysics.

Conclusion

An appraisal is given of the achievements of modal homotopy type theory as described through the earlier chapters, and of the future prospects of this new logic. This is carried out in terms of the constraints exerted on its users by the formalism, and of the expressive freedom it allows. In particular, the power of combining the component parts – types, dependency, homotopy, modality – is emphasised.

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.