Path Spaces of Higher Inductive Types in Homotopy Type Theory

Kraus, Nicolai; von Raumer, Jakob

Abstract

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the truncation levels. This result makes it possible to reason directly about certain equality types and to streamline existing proofs by eliminating the necessity of auxiliary constructions. To demonstrate this, we give a very short argument for the calculation of the fundamental group of the circle (Licata and Shulman [1]), and for the fact that pushouts preserve embeddings. Further, our development suggests a higher version of the Seifert-van Kampen theorem, and the set-truncation operator maps it to the standard Seifert-van Kampen theorem (due to Favonia and Shulman [2]). We provide a formalization of the main technical results in the proof assistant Lean.

• Conference Name: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• Conference Location: Vancouver, BC, Canada
• Start Date: Jun 24, 2019
• End Date: Jun 27, 2019
• Acceptance Date: Mar 28, 2019
• Online Publication Date: Aug 5, 2019
• Publication Date: 2019-06
• Deposit Date: Jul 15, 2020
• Publicly Available Date: Aug 4, 2020
• Publisher: Institute of Electrical and Electronics Engineers
• Book Title: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
• ISBN: 978-1-7281-3609-7
• DOI: https://doi.org/10.1109/LICS.2019.8785661
• Keywords: Logic; Logic in Computer Science
• Public URL: https://nottingham-repository.worktribe.com/output/2461875
• Publisher URL: https://ieeexplore.ieee.org/document/8785661
• Additional Information: © 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.