Monday, October 3, 2016 - 12:00pm to 1:00pm
Location:Traffic21 Classroom 6501 Gates & Hillman Centers
Speaker:KUEN BANG (FAVONIA) HOU, Ph.D. Student http://www.cs.cmu.edu/~kuenbanh/
Following recent investigations of the use of homotopy type theory to give machine-checked proofs of constructions from homotopy theory, we constructed a mechanized proof of a result called the Blakers-Massey connectivity theorem, which relates the higher-dimensional loop structures of two spaces sharing a common part (represented by a pushout type, which is a generalization of a disjoint sum type) to those of the common part itself. This theorem gives important information about the pushout type, and has a number of useful corollaries, including the Freudenthal suspension theorem, which was used in previous formalizations. The proof is more direct than existing ones that apply in general category-theoretic settings for homotopy theory, and its mechanization is concise and high-level, due to novel combinations of ideas from homotopy theory and from type theory.
Due to the time limit, I will only explain the meaning of the main theorem, but will demonstrate how this theorem leads to the Freudenthal suspension theorem, an important corollary for understanding higher-dimensional loop structures of spheres.
This is an extended version of the talk of the same title given in LICS 2016, and will last about 25-30 minutes.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement.