the1lab

the1lab/1lab

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

3 good first / help-wanted issues · Agda · last activity Aug 7, 2026

438 stars 95 forks 438 watchers Agda GNU Affero General Public License v3.0
agda homotopy-type-theory
View on GitHub Website
3 Open Issues Need Help Last updated: Aug 7, 2026

Open Issues Need Help

View All on GitHub
The universe of n-types is not an n-type 1 day ago
good first issue type-theory
the1lab/1lab
438

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Agda
#agda#homotopy-type-theory
Prove that all of our colimit diagrams are actually colimits 4 months ago
enhancement good first issue category-theory
the1lab/1lab
438

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Agda
#agda#homotopy-type-theory
Refactor Data.Vec to use a refinement type ala `Fin` about 1 year ago
enhancement good first issue
the1lab/1lab
438

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

Agda
#agda#homotopy-type-theory