Free Higher Groups in Homotopy Type Theory

Kraus, Nicolai; Altenkirch, Thorsten

Abstract

© 2018 ACM. Given a type A in homotopy type theory (HoTT), we can define the free∞-group onA as the loop space of the suspension ofA+1. Equivalently, this free higher group can be defined as a higher inductive type F(A) with constructors unit : F(A), cons : A → F(A) → F(A), and conditions saying that every cons(a) is an auto-equivalence on F(A). Assuming that A is a set (i.e. satisfies the principle of unique identity proofs), we are interested in the question whether F(A) is a set as well, which is very much related to an open problem in the HoTT book [22, Ex. 8.2]. We show an approximation to the question, namely that the fundamental groups of F(A) are trivial, i.e. that ||F(A)||1 is a set.

Citation

Kraus, N., & Altenkirch, T. (2018). Free Higher Groups in Homotopy Type Theory. In LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (599-608). https://doi.org/10.1145/3209108.3209183

• Presentation Conference Type: Edited Proceedings
• Conference Name: LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
• Start Date: Jul 9, 2018
• End Date: Jul 12, 2018
• Acceptance Date: Mar 31, 2018
• Online Publication Date: Jul 9, 2018
• Publication Date: Jul 9, 2018
• Deposit Date: Apr 18, 2018
• Publicly Available Date: Jul 9, 2018
• Electronic ISSN: 1043-6871
• Publisher: Association for Computing Machinery (ACM)
• Peer Reviewed: Peer Reviewed
• Volume: 2018-July
• Pages: 599-608
• Book Title: LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science
• ISBN: 9781450355834
• DOI: https://doi.org/10.1145/3209108.3209183
• Keywords: Logic in Computer Science
• Public URL: https://nottingham-repository.worktribe.com/output/923128
• Publisher URL: https://dl.acm.org/citation.cfm?id=3209183
• Contract Date: Apr 18, 2018