Structural Foundations with annotated toc of 3 great books with numerous links to related nlab content:
noncommutative geometry (general flavour)
group theory (including generalizations)
gebras (co(al)gebras, bi/Hopf-algebr-as/oids…)
mathematical analysis
based on plain type theory/set theory:
based on dependent type theory/homotopy type theory:
For monoidal category theory:
projects for formalization of mathematics with proof assistants:
Archive of Formal Proofs (using Isabelle)
ForMath project (using Coq)
UniMath project (using Coq)
Xena project (using Lean)
Historical projects that died out: