Mathematicians usually have an analytic approach to the mathematical objects they want to study: this means that they understand these objects as being constructed from more basic ones. The most basic objects are sets, for example the set of natural numbers. These can be used to construct rational numbers, then real numbers, followed by surfaces and so on. As these constructions are being piled up on top of each other, contemporary mathematical objects get more and more complicated. This means mathematicians have more and more to learn to access a new field, and formalising mathematical arguments gets more and more challenging.
As a way to bypass this increasing complexity, we use a synthetic approach to the mathematical objects we want to study: this means that we aim to design formal languages where these objects are basic ones. Homotopy type theory is a synthetic approach to homotopy theory, which is a theory of geometric objects up to deformation. Our project combines homotopy type theory with other synthetic methods.
In algebraic geometry, polynomial equations are studied using methods from geometry and algebra. These two fields have many links, the most basic being the correspondence between a space and the algebra of functions from that space to a fixed ring. In the usual analytic approach, this correspondence is made one-to-one by using a complicated notion of space. In our synthetic approach, this correspondence is assumed one-to-one as an axiom. We were able to reproduce non-trivial basic algebraic geometry results with this synthetic approach, sometimes with new proofs.
The traditionhal approach to analysis starts with the notion of convergence of sequences of real numbers. It leads to the real numbers being given a topology, which is an abstract structure encoding this notion of convergence. In synthetic topology, every object, including the real numbers, is naturally endowed with an intrinsic topology. In our approach, this topology matches the canoncial topology.
This combines with synthetic homotopy theory to give us a shortcut to algebraic topology, which is the study of topological spaces up to deformation.
For more information on the project and references, visit the project website.