Download from here.
This note explores the application of cubical type theory to lay the basics of homotopy theory in a synthetic fashion. It's still a work in progress... Currently, only available in 简体中文.
- Finish the main parts
This work is licensed under a Creative Commons Attribution-NonCommercial-ShareAlike 4.0 International License.
