Higher-Dimensional Types in the Mechanization of Homotopy Theory

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à.

Important Notes on (Lack of) Attribution

  1. Many fundamental concepts, such as h-levels, should have been more explicitly attributed to Professor Vladimir Voevodsky. One should be aware that Voevodsky’s contribution is much greater than the impression given by the text.
  2. The English translation of the Diamond Sūtra cited in Appendix B should have been explicitly attributed to Professor Paul Harrison.




  author = {Kuen-Bang {Hou (Favonia)}},
  title = {Higher-Dimensional Types in the Mechanization of Homotopy Theory},
  school = {Carnegie Mellon University},
  year = 2017,
  month = feb,
  url = {https://favonia.org/thesis}

Known Errata

These errata were present even in the most updated PDF:

  1. On page 18, the sentence “this principle can be traced back to the universe extension for the groupoid model constructed by Martin Hofmann and Thomas Streicher” turned out to be a historic accident. In a now-public private exchange, Vladimir Voevodsky stated “I was not inspired by it. In fact I tried several times to understand what they are saying and never could.” (Clarified on 2019/01/27 by me.)
  2. On page 45, Lemma 3.1.3, A is m-connected, not m-type, and similarly for B. In the type of , f(b_0) should be replaced by g(b_0). (Found on 2018/08/26 by Tim Baumann.)
  3. On page 67, line 5, the pushout type is messed up. It is the same type described above but typeset badly. (Found on 2018/9/4 by Tim Baumann.)
  4. On page 68, Equation (3.3), left(b_1) should be replace by right(b_1) on both sides. (Found on 2018/08/26 by Tim Baumann.)

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

  1. On page 7 of the text, remark 1.5.2 has been rewritten for clarity. The old text is correct but confusing. (Fixed on 2017/10/25 and 2017/11/24.)
  2. On page 38 of the text, “diagram” was misspelled as “dimagram”. (Fixed on 2017/06/29.)
  3. 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. (Fixed on 2017/04/02.)
  4. On page 83 of the text, two “h^0 2” should be “h^0(2)”. Parentheses were missing. (Fixed on 2017/04/01.)


This page was made with GitHub-like CSS (licensed under MIT and modified by me).