GROUPOЇD INTERNSHIP PROGRAM

Sponsorship Call for Submissions

This page is dedicated to the Groupoid Infinity student sponsorship. Groupoid Infinity is a group of mathematicians who develop the cubical base library for all main cubical type checkers (cubicaltt, Arend, Agda, Lean, Anders), 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 following literature: UDC 51.

Our proposal is following. We want to provide $200/month budged to volunteers porting terms to Anders theorem prover from cubicaltt and Agda.

Your responsibility will be to provide coverage of necessary math foundations contributed to Anders base library, formalize it in cubical type checkers and provide pull request to Github repository. 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