  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 $BS_n$ of all $n$-element types to the type $BS_2$ of all
$2$-element types. Making use of the univalence axiom, we characterize
precisely when a pointed map $BS_n\to_\ast BS_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.
