Recall the well-known declaration of Hegel in the Philosophy of Right proclaiming that the moment of understanding takes place after achievements of practice.
When Philosophy paints its grey in grey then has a form of life grown old. By philisophy’s grey in grey it cannot be rejuvenated but only understood. The Owl of Minerva spreads its wings only with the falling of the dusk.
Perhaps the vast body of literature in philosophy of mathematics on old subjects such as arithmetic, real analysis, and set theory is a testimony to the truth of this declaration. However, there is a peculiar case that should not go unnoticed here. There has been two revolutions in the foundations of algebraic topology and algebraic geometry in the 20th century: the first is the advent of categories, functors and natural transformations by Eilenberg and Mac Lane in their quest to provide a foundational setting for homological algebra. The second is the formalization of schemes, the most fundamental objects of study of modern algebraic geometry. The history of development of this formalization is quite interesting and complicated and an excellent potential case study for this project. Chevalley in 1956 defined the notion of scheme based on earlier work of Weil and Zariski. There were improvements on Chevalley definition notably by Nagata. However, this definition was totally transformed into a more abstract and sufficiently general definition by A. Grothendieck in 1958. Work of Grothendieck involved novel and extensive use of category theory in algebraic geometry and advent of topoi as generalized spaces. Grothendieck’s vision on stacks and higher stacks in À la poursuite des champs paved the way for emergence of new fields of derived and homotopical algebraic geometry as formalized By Toen & Vezzosi, and later via different approach by Lurie.
Of course category theory is now an indispensable branch of mathematics that has found widespread use both in the foundation and practices of different branches of mathematics, physics, and theory of computations in computing sciences. To mention only a few, one can look into plethora of research work in use of category theoretic reasoning in algebraic geometry and arithmetic geometry, categorical algebras in logic and homotopy theory, co-algebras in formalization of non-deterministic systems, operadic and higher categorical methods in abstract homotopy theory and algebraic topology, string and surface diagrams in quantum theory, application of higher categorical structures in quantum field theory (such as celebrated cobordism theorem), functorial semantics in the study of natural languages semantics, monads in functional programming languages, and the list goes on and on.
Despite all these seismic shifts in the geography of structural mathematics which is now almost a century old, however, category theory and higher category theory have remained severely under-represented in the philosophy of mathematics. The oddity here is that philosophy of mathematics has for the most part been stuck with philosophy of set theory. Perhaps the peculiarity of this situation is more brazen if one contrasts it to the parallel situation in the philosophy of modern physics where revolutionary fields of modern physics such as quantum physics, general relativity, string theory, and quantum gravity are subject matter of mainstream philosophical studies.
I agree with Paul Feyerabend in his epistemological anarchism that in order to understand the processes of growth of knowledge philosophers of science should be receptive to ideas from the most disparate and apparently far-flung domains. Having this in mind, I will give a brief historical survey of modern foundational approaches to structural mathematics such as category theory, topos theory and univalent foundation. The following is written from a specific point of view, namely
There are often novel ways of understanding both at the level of informal practice and at the level of formal theories generated by the interplay between informal theories of structural mathematics and their modern formalization.
In what follows I will also reflect on the question
what does it mean to see a structure as a formalization of a mathematical theory?