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.