Mechanized reasoning has proved effective in avoiding serious mistakes in software and hardware, and yet remains unpopular in the practice of mathematics. My thesis is aimed at making mechanization easier so that more mathematicians can benefit from this technology. Particularly, I experimented with *higher-dimensional types,* an extension of ordinary types with a hierarchy of stacked relations, and managed to mechanize many important results from classical homotopy theory in the proof assistant Agda. My work thus suggests higher-dimensional types may help mechanize mathematical concepts.

Ki'hâihuà thuilí í'king ē'tàng pībián nńgthé kap ngē'thé tiong giâmtiōng ê tshò'ngōo, tsóng--sī tī sòoha̍k giánkiù si̍tbū iáu hántit iōng. Pún lūnbûn ê tsongtsí sī beh sú ki'hâihuà khah khuài hōo sòoha̍kka sú'iōng. Siôngsè lâi kóng, guá sú'iōng ko'uî luīhîng (higher-dimensional types), iā tsiūsī tī itpuann ê luīhîng tíngkuân ka'thiam to'kai'tsân ê kuanhē, tsiong kóotián tônglûn lílūn (classical homotopy theory) ê kuí'nā hāng tiōng'iàu ê sîngkó, tī tsìngbîng hú'tsōo kangkhū Agda lāi'té sūnlī ki'hâihuà. Guá ê giánkiù sîngkó hiánsī ko'uî luīhîng kiámtshái ē'tàng pangtsōo sòoha̍k khàiliām ê ki'hâihuà.

- The most updated PDF (recommended).
- The submitted, official PDF (containing the errata listed below).

- The latest code on GitHub. This may deviate from the text.
- The archived code on figshare which matches the text.

These errata were fixed in the updated PDF but not in the submitted (official) version.

- On page 48 of the text, "Because I proved this lemma," should be completely removed. To clarify, people had been working on these factorization problems before I proved it. (Found on 2017/04/02.)
- On page 83 of the text, two "h^0 2" should be "h^0(2)". Parentheses were missing. (Found on 2017/04/01.)

Minimalism with GitHub-like CSS (licensed under MIT).