Martin Escardo, 3rd November 2023.

The symmetric group on a set X, namely the group of automorphisms on X
under composition with the identity automorphism as the unit.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt

module Groups.Symmetric (fe : Fun-Ext) where

open import Groups.Type
open import MLTT.Spartan
open import UF.Sets
open import UF.Equiv
open import UF.Equiv-FunExt

private
 fe' : FunExt
 fe' ๐“ค ๐“ฅ = fe {๐“ค} {๐“ฅ}

symmetric-group : (X : ๐“ค ฬ‡ ) โ†’ is-set X โ†’ Group ๐“ค
symmetric-group X X-is-set =
 Aut X ,
 _โ—_ ,
 โ‰ƒ-is-set fe X-is-set ,
 (ฮป ๐•— ๐•˜ ๐•™ โ†’ (โ‰ƒ-assoc fe' ๐•— ๐•˜ ๐•™)โปยน) ,
 ๐•š๐•• ,
 โ‰ƒ-refl-left fe' ,
 โ‰ƒ-refl-right fe' ,
 (ฮป ๐•— โ†’ โ‰ƒ-sym ๐•— , โ‰ƒ-sym-left-inverse fe' ๐•— , โ‰ƒ-sym-right-inverse fe' ๐•—)

\end{code}