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.
The language is also known as Tâiuân’uē (Taiwanese). See the thesis appendix for more details on the typesetting of its writing.
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à.
@phdthesis{favonia-as:thesis,
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}
}These bugs were present even in the most updated PDF:
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.)
On page 34, apf should have be apB. (Reported on 2022/07/31 by Perry Hart.)
On page 45, Lemma 3.1.3, A is m-connected, not m-type, and similarly for B. In the type of α, “f(b0)” should be replaced by “g(b0)”. (Reported on 2018/08/26 by Tim Baumann.)
On page 49, in the formula after “constancy condition is given by applying identification elimination”, the “fst(s0)” at the end of the first line should have been “fst(s1)”, and the “snd(s0)” on the second line should be “snd(s1).” (Reported on 2021/02/11 by Perry Hart.)
On page 52, Line -5, “F(a)” should have been “F’(a)”. (Reported on 2021/02/11 by Perry Hart.)
On page 53, Line 1, “F(a)” should have been “F’(a)”. (Reported on 2021/02/11 by Perry Hart.)
On page 60, the “pc” at the end of the type of “refl − reflAA” should have been “α”. Similarly, the “pc” at the end of the type of “refl − reflAB” should have been “β”. (Reported on 2021/02/11 by Perry Hart.)
On page 67, line 5, the pushout type is messed up. It is the same type described above but typeset badly. (Reported on 2018/09/04 by Tim Baumann.)
On page 68, Equation (3.3), “left(b1)” should be replace by “right(b1)” on both sides. (Reported on 2018/08/26 by Tim Baumann.)
On page 101, line -2, (a : A) → X a should have been (a : A) → X a → …
(Reported before 2021/02 by Perry Hart.)
On page 112, line -6 (the last Agda code snippet), (r : bmleft a₀ == bmright b₀) in the type of blackers-massey should be removed. The correct type is
blakers-massey : ∀ {a₀ b₀} → has-conn-fibers (m +2+ n) (bmglue {a₀} {b₀})(Reported on 2021/02/07 by Perry Hart.)
On page 121, Section A.2, “a great varieties of” should be “a great variety of.” (Reported before 2019/08 by Carlo Angiuli.)
These errata were fixed in the updated PDF but not in the submitted (official) version:
This page was made with GitHub-like CSS (licensed under MIT and modified by me).