一句话：在同伦类型论中研究自由高阶群 F(A) 何时为集合，证明其基本群平凡，即 ||F(A)||₁ 是集合。
给定类型 A，在同伦类型论（HoTT）中可将 A 上的自由 ∞-群定义为 A+1 的悬挂的环路空间；等价地，它也可定义为高阶归纳类型 F(A)，其构造子包括 unit: F(A) 与 cons: A → F(A) → F(A)，并满足每个 cons(a) 是 F(A) 上的自等价。若 A 是集合（即满足唯一恒等证明原则），论文关注 F(A) 是否也是集合，该问题与 HoTT 书 [22, Ex. 8.2] 中的开放问题密切相关。作者给出该问题的一个近似回答：F(A) 的基本群平凡，即其 1-截断 ||F(A)||₁ 是集合。
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.