Stacks project, from a homotopy type theory point-of-view (hPOV)
We aim to formalize the entire Stacks project tag by tag in Arend.
The purpose of this project is three-fold:
- Explore how hPOV affects algebraic geometry and related subjects;
- Provide the math community with a formally verified library on algebraic geometry;
- Provide the Arend community with "real-world" use cases, and try to find possible improvements.
This project is in its very early stage, so expect a lot of design/structural changes.