Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the loop space of the suspension of A + 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.
|Title of host publication||Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)|
|Publisher||Association for Computing Machinery (ACM)|
|Publication status||Published - 9 Jul 2018|
|Event||Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018) - Oxford, United Kingdom|
Duration: 9 Jul 2018 → 12 Jul 2018
|Conference||Thirty-Third Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2018)|
|Period||9/07/18 → 12/07/18|