You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Tim Hosgood (May 16 2022 at 21:58):This Wednesday (the 18th of May) at 16:00 UTC
Juan F. Meleiro (Universidade de São Paulo) — Towards Modular Mathematics
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.
Zoom: https://topos-institute.zoom.us/j/86201468397?pwd=L0NER3FCOFZpTHRWMWVVMEZ5ckJoZz09
YouTube: https://www.youtube.com/watch?v=kQIloPijGaw