NCATLAB and GROUPOЇD

Sponsorship Call for Submissions

This page is dedicated to the ncatlab collaboration project. Groupoid Infinity is a group of mathematicians who develop the cubical base library to all main cubical type checkers (cubicaltt, Arend, Agda, Lean), the home page of the project is cubical.systems.

The main aim is to provide formal HoTT foundations for contemporary math and have fun. Some parts are so new that we need a help of strong mathematicians. Our areas of interests are: Sheaf Theory, Infinity Category Theory, Differential Geometry, Cohesive Type Theory, Algebraic Geometry, Homology, and Cohomology Theory, Geometric Type Theory. Our community is mostly guided by outdated [Russian literature] instagram.com/groupoid.space.

Our proposal is following. We want to provide $400/month budged to volunteers helping us clarify topics that are not yet presented at ncatlab or topics that need to be clarified in the direction of our interests. We are talking about the very foundations, not the Fields Medal caliber. E.g. we lack de Rham cohomology based formal foundation of classical calculus, for the first year graduate students. But you can pick any topic from our area of interests.

Your responsibility will be to provide coverage of necessary math foundations contributed to ncatlab, so we can grab this information and formalize it in cubical type checkers. Please consider this as an art project, despite the cutting edge mathematics we are dealing with. Our main motivation is to spread contemporary math around the world and to help students who want to deal with cubical type checkers. As a side effect, we are expecting you to have fun as we do along the way.

Best regards
Namdak Tonpa
    Mail: [email protected]
    Telegram: t.me/tonpa