Towards Modular Mathematics

Abstract: Synthetic Reasoning is a style of mathematics based on axiomatic theories that aim to capture the fundamental and essential structures in a particular subject. Such theories are often type theories with intended interpretations inside structured categories such as toposes.

But theorycrafting is currently an artisanal job, that requires analysis and synthesis from scratch for every theory that will be created. A formal (and categorical) toolkit for manipulating these theories could aid the synthetic mathematician in their endeavors, just as a toolbox can help any artisan in their craft.

Modular mathematics is mathematics based on these formal theories that capture a way of Synthetic Reasoning in particular fields, and can then be combined and compared. In this talk, I will present work in progress towards a framework for such modular mathematics. Universal Logic will be our guide for the capabilities that such a framework should provide, including translation between, and combinations of theories. I will present a formal theory called MMT (introduced by Florian Rabe) that follows such a guide. I will then present three formal approaches to the definition of the fundamental group, each following a distinct style: a purely categorical, a syntactical-categorical, and a purely syntactical one; all in order to explore some possible ways to do Modular Mathematics.

category theory

Audience: researchers in the topic

Em-Cats