the1lab / 1lab

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
https://1lab.dev
GNU Affero General Public License v3.0
334 stars 63 forks source link

chore: add page for tracking Borceux progress #402

Closed TOTBWF closed 1 month ago

TOTBWF commented 2 months ago

Description

Adds a page for tracking progress on Borceux. Somewhat surprisingly, we are already 34% of the way done!

Checklist

Before submitting a merge request, please check the items below:

If your change affects many files without adding substantial content, and you don't want your name to appear on those pages (for example, treewide refactorings or reformattings), start the commit message and PR title with chore:.

Lavenza commented 2 months ago

Pull request preview

plt-amy commented 1 month ago

@TOTBWF can you add a mention of the Borceux page to the index? Under the HoTT and Elephant pages