Reference resource for mathematics done in Homotopy Type Theory
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory. Unlike the HoTT book, the 1lab is not a “linear” resource: Concepts are presented as a directed graph, with links indicating dependencies.
| System | Target | Derivation | Build status |
|---|---|---|---|
| x86_64-linux | /gnu/store/36yqsb1z2r3ypbrcimvmiwja642lk34m-agda-1lab-0.0-3.afcf848.drv | ||
| i686-linux | /gnu/store/chxrfswcgas135jhg97nn3mcbynkn390-agda-1lab-0.0-3.afcf848.drv | ||
| aarch64-linux | /gnu/store/gpbd1lr0agzzm29p8qm5fw634bam0ix7-agda-1lab-0.0-3.afcf848.drv |
| Linter | Message | Location |
|---|---|---|
| No lint warnings ✓ | ||