Delooping the sign homomorphism in univalent mathematics

Abstract

In univalent mathematics there are at least two equivalent ways to present the category of groups. Groups presented in their usual algebraic form are called abstract groups, and groups presented as pointed connected $1$-types are called concrete groups. Since these two descriptions of the category of groups are equivalent, we find that every algebraic group corresponds uniquely to a concrete group -- its delooping -- and that each abstract group homomorphisms corresponds uniquely to a pointed map between concrete groups. The $n$-th abstract symmetric group $S_n$ of all bijections $[n]\simeq [n]$, for instance, corresponds to the concrete group of all $n$-element types. The sign homomorphism from $S_n$ to $S_2$ should therefore correspond to a pointed map from the type $B{S}_n$ of all $n$-element types to the type $B{S}_2$ of all $2$-element types. Making use of the univalence axiom, we characterize precisely when a pointed map $B{S}_n{\to }_{\ast }B{S}_2$ is a delooping of the sign homomorphism. Then we proceed to give several constructions of the delooping of the sign homomorphism. Notably, the construction following a method of Cartier can be given without reference to the sign homomorphism. Our results are formalized in the agda-unimath library.