We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of synthetic homotopy theory. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with $0$-connected, pointed $1$-types. Many of our results are formalized as part of the agda-unimath library.

翻译：我们刻画了同伦类型论（HoTT）中的单射同态为纤维化无环映射，并在综合同伦理论框架下发展了无环映射与无环类型的类型论处理方法。通过将群识别为$0$-连通、带点$1$-类型，我们给出了群论中的实例与应用，例如希格曼群的无环性。我们的许多结果已形式化并纳入agda-unimath库中。