单值数学中对符号同态的去环化

在单值数学中，至少有两种等价的方式来呈现群范畴。以通常代数形式给出的群称为抽象群，而以带点连通 $1$-型给出的群称为具体群。由于群范畴的这两种描述是等价的，我们发现每个代数群都唯一对应于一个具体群——它的去环化（delooping）——并且每个抽象群同态都唯一对应于具体群之间的带点映射。例如，所有双射 $[n]\simeq [n]$ 的第 $n$ 个抽象对称群 $S_n$ 对应于所有 $n$ 元素类型的具群。因此，从 $S_n$ 到 $S_2$ 的符号同态应对应于从所有 $n$ 元素类型的类型 $BS_n$ 到所有 $2$ 元素类型的类型 $BS_2$ 的带点映射。利用单值公理，我们精确刻画了何时一个带点映射 $BS_n\to_\ast BS_2$ 是符号同态的去环化。随后我们给出符号同态去环化的几种构造。值得注意的是，遵循 Cartier 方法的一种构造可在不引用符号同态的情况下给出。我们的结果已在 agda-unimath 库中实现形式化。