hStacks

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:

1. Explore how hPOV affects algebraic geometry and related subjects;
2. Provide the math community with a formally verified library on algebraic geometry;
3. 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.