| Summary: | Given a type A in homotopy type theory (HoTT), we can define the free ∞-group on A as the 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). Equivalently, we can take the loop space of the suspension of A + 1. 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 [20, 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.
|
|---|