From 0bd8be2c604726340c8d08732d05b93d5de44a98 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Fri, 14 Feb 2025 19:04:12 +0530
Subject: [PATCH 1/8] Theory of Symmetric Groups

---
 Cubical/Algebra/SymmetricGroup.agda | 88 ++++++++++++++++++++++++-----
 1 file changed, 75 insertions(+), 13 deletions(-)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index aa4395f7d4..e3498ab606 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -5,22 +5,84 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Data.Sigma
-open import Cubical.Data.Nat using (ℕ ; suc ; zero)
-open import Cubical.Data.Fin using (Fin ; isSetFin)
-open import Cubical.Data.Empty
-open import Cubical.Relation.Nullary using (¬_)
+open import Cubical.Data.Nat
+open import Cubical.Data.SumFin
+open import Cubical.Data.Empty as Empty
+open import Cubical.Data.Bool
+open import Cubical.Data.Unit
 
 open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Bool
+open import Cubical.Algebra.Group.Instances.Unit
 
-private
-  variable
-    ℓ : Level
+private variable
+  ℓ ℓ' : Level
+  X Y : Type ℓ
 
-Symmetric-Group : (X : Type ℓ) → isSet X → Group ℓ
-Symmetric-Group X isSetX = makeGroup (idEquiv X) compEquiv invEquiv (isOfHLevel≃ 2 isSetX isSetX)
-  compEquiv-assoc compEquivEquivId compEquivIdEquiv invEquiv-is-rinv invEquiv-is-linv
+SymGroup : (X : Type ℓ) → isSet X → Group ℓ
+SymGroup X isSetX = makeGroup {G = X ≃ X} (idEquiv X) compEquiv invEquiv
+  (isOfHLevel≃ 2 isSetX isSetX)
+  compEquiv-assoc
+  compEquivEquivId
+  compEquivIdEquiv
+  invEquiv-is-rinv
+  invEquiv-is-linv
 
--- Finite symmetrics groups
+FinSymGroup : ℕ → Group₀
+FinSymGroup n = SymGroup (Fin n) isSetFin
 
-Sym : ℕ → Group _
-Sym n = Symmetric-Group (Fin n) isSetFin
+Sym0≃1 : GroupEquiv (FinSymGroup 0) UnitGroup₀
+Sym0≃1 = contrGroupEquivUnit $ inhProp→isContr (idEquiv _) $
+         isOfHLevel≃ 1 isProp⊥ isProp⊥
+
+Sym0≡1 : FinSymGroup 0 ≡ UnitGroup₀
+Sym0≡1 = uaGroup Sym0≃1
+
+Sym1≃1 : GroupEquiv (FinSymGroup 1) UnitGroup₀
+Sym1≃1 = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrSumFin1 isContrSumFin1
+
+Sym1≡1 : FinSymGroup 1 ≡ UnitGroup₀
+Sym1≡1 = uaGroup Sym1≃1
+
+Sym2≃Bool : GroupEquiv (FinSymGroup 2) BoolGroup
+Sym2≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $ 
+  Fin 2 ≃ Fin 2 Iso⟨ equivCompIso SumFin2≃Bool SumFin2≃Bool ⟩
+  Bool ≃ Bool   Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool   Iso⟨ invIso reflectIso ⟩
+  Bool          ∎Iso
+  where open BoolReflection
+
+Sym2≡Bool : FinSymGroup 2 ≡ BoolGroup
+Sym2≡Bool = uaGroup Sym2≃Bool
+
+SymUnit≃Unit : GroupEquiv (SymGroup Unit isSetUnit) UnitGroup₀
+SymUnit≃Unit = contrGroupEquivUnit $ isOfHLevel≃ 0 isContrUnit isContrUnit
+
+SymUnit≡Unit : SymGroup Unit isSetUnit ≡ UnitGroup₀
+SymUnit≡Unit = uaGroup SymUnit≃Unit
+
+SymBool≃Bool : GroupEquiv (SymGroup Bool isSetBool) BoolGroup
+SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $ invIso $
+  Bool        Iso⟨ reflectIso ⟩
+  Bool ≡ Bool Iso⟨ univalenceIso ⟩
+  Bool ≃ Bool ∎Iso
+  where open BoolReflection
+
+SymBool≡Bool : SymGroup Bool isSetBool ≡ BoolGroup
+SymBool≡Bool = uaGroup SymBool≃Bool
+
+module _ (n : ℕ) where
+  open import Cubical.Data.Fin.LehmerCode using (factorial)
+
+  ⟨Sym⟩≃factorial : ⟨ FinSymGroup n ⟩ ≃ Fin (factorial n)
+  ⟨Sym⟩≃factorial = SumFin≃≃ n
+
+  ⟨Sym⟩≡factorial : ⟨ FinSymGroup n ⟩ ≡ Fin (factorial n)
+  ⟨Sym⟩≡factorial = ua ⟨Sym⟩≃factorial
+
+Sym-cong-≃ : ∀ isSetX isSetY → X ≃ Y → GroupEquiv (SymGroup X isSetX) (SymGroup Y isSetY)
+Sym-cong-≃ isSetX isSetY e .fst = equivComp e e
+Sym-cong-≃ isSetX isSetY e .snd = makeIsGroupHom λ g h → sym $ equivEq $ funExt λ x → cong (e .fst ∘ h .fst) (retEq e _)

From a48ba5ccd76f10c851326218d5b9a733531eb722 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Fri, 14 Feb 2025 20:47:15 +0530
Subject: [PATCH 2/8] Removed a trailing whitespace

---
 Cubical/Algebra/SymmetricGroup.agda | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index e3498ab606..52e622844b 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -35,8 +35,7 @@ FinSymGroup : ℕ → Group₀
 FinSymGroup n = SymGroup (Fin n) isSetFin
 
 Sym0≃1 : GroupEquiv (FinSymGroup 0) UnitGroup₀
-Sym0≃1 = contrGroupEquivUnit $ inhProp→isContr (idEquiv _) $
-         isOfHLevel≃ 1 isProp⊥ isProp⊥
+Sym0≃1 = contrGroupEquivUnit $ inhProp→isContr (idEquiv _) $ isOfHLevel≃ 1 isProp⊥ isProp⊥
 
 Sym0≡1 : FinSymGroup 0 ≡ UnitGroup₀
 Sym0≡1 = uaGroup Sym0≃1
@@ -48,7 +47,7 @@ Sym1≡1 : FinSymGroup 1 ≡ UnitGroup₀
 Sym1≡1 = uaGroup Sym1≃1
 
 Sym2≃Bool : GroupEquiv (FinSymGroup 2) BoolGroup
-Sym2≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $ 
+Sym2≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
   Fin 2 ≃ Fin 2 Iso⟨ equivCompIso SumFin2≃Bool SumFin2≃Bool ⟩
   Bool ≃ Bool   Iso⟨ invIso univalenceIso ⟩
   Bool ≡ Bool   Iso⟨ invIso reflectIso ⟩
@@ -65,10 +64,10 @@ SymUnit≡Unit : SymGroup Unit isSetUnit ≡ UnitGroup₀
 SymUnit≡Unit = uaGroup SymUnit≃Unit
 
 SymBool≃Bool : GroupEquiv (SymGroup Bool isSetBool) BoolGroup
-SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $ invIso $
-  Bool        Iso⟨ reflectIso ⟩
-  Bool ≡ Bool Iso⟨ univalenceIso ⟩
-  Bool ≃ Bool ∎Iso
+SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
+  Bool ≃ Bool Iso⟨ invIso reflectIso ⟩
+  Bool ≡ Bool Iso⟨ invIso univalenceIso ⟩
+  Bool        ∎Iso
   where open BoolReflection
 
 SymBool≡Bool : SymGroup Bool isSetBool ≡ BoolGroup

From b98c453cf06be1777836fbd958d1d8a4f68899be Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Fri, 14 Feb 2025 21:18:04 +0530
Subject: [PATCH 3/8] Imported `_$_`

---
 Cubical/Algebra/SymmetricGroup.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index 52e622844b..e14ee4d388 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -4,6 +4,7 @@ module Cubical.Algebra.SymmetricGroup where
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Function
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
 open import Cubical.Data.SumFin

From 6f9840cc6ad0e6904f09a501514b92bffd7ccd9b Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 15 Feb 2025 09:59:12 +0530
Subject: [PATCH 4/8] Forgot to import from `Cubical.Foundations.Isomorphism`

---
 Cubical/Algebra/SymmetricGroup.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index e14ee4d388..be792898ae 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -5,6 +5,7 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Function
+open import Cubical.Foundations.Isomorphism
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
 open import Cubical.Data.SumFin

From 23e3fe1ade45c6ce55274e9b7b48578ce973b14a Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 15 Feb 2025 10:05:23 +0530
Subject: [PATCH 5/8] Forgot to import univalence

---
 Cubical/Algebra/SymmetricGroup.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index be792898ae..ae40da8799 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -6,6 +6,7 @@ open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
 open import Cubical.Data.SumFin

From e77c237be3678266942a24234502572ff56ec71d Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 15 Feb 2025 10:21:12 +0530
Subject: [PATCH 6/8] Compatibility with #1184

`LehmerCode` no longer exports `factorial`
---
 Cubical/Algebra/SymmetricGroup.agda | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index ae40da8799..9e579af436 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -77,12 +77,11 @@ SymBool≡Bool : SymGroup Bool isSetBool ≡ BoolGroup
 SymBool≡Bool = uaGroup SymBool≃Bool
 
 module _ (n : ℕ) where
-  open import Cubical.Data.Fin.LehmerCode using (factorial)
 
-  ⟨Sym⟩≃factorial : ⟨ FinSymGroup n ⟩ ≃ Fin (factorial n)
+  ⟨Sym⟩≃factorial : ⟨ FinSymGroup n ⟩ ≃ Fin (n !)
   ⟨Sym⟩≃factorial = SumFin≃≃ n
 
-  ⟨Sym⟩≡factorial : ⟨ FinSymGroup n ⟩ ≡ Fin (factorial n)
+  ⟨Sym⟩≡factorial : ⟨ FinSymGroup n ⟩ ≡ Fin (n !)
   ⟨Sym⟩≡factorial = ua ⟨Sym⟩≃factorial
 
 Sym-cong-≃ : ∀ isSetX isSetY → X ≃ Y → GroupEquiv (SymGroup X isSetX) (SymGroup Y isSetY)

From 5d6f1681d7adc2c106865d239e1e0d42933756db Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 15 Feb 2025 10:32:38 +0530
Subject: [PATCH 7/8] import `Foundations.Structure`

---
 Cubical/Algebra/SymmetricGroup.agda | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index 9e579af436..1da142ceb6 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -7,6 +7,7 @@ open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
 open import Cubical.Foundations.Univalence
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Sigma
 open import Cubical.Data.Nat
 open import Cubical.Data.SumFin

From 3d93853099ee3f67e27e42d1718faa460a5e4f01 Mon Sep 17 00:00:00 2001
From: anshwad10 <109362320+anshwad10@users.noreply.github.com>
Date: Sat, 15 Feb 2025 10:45:58 +0530
Subject: [PATCH 8/8] fix

---
 Cubical/Algebra/SymmetricGroup.agda | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cubical/Algebra/SymmetricGroup.agda b/Cubical/Algebra/SymmetricGroup.agda
index 1da142ceb6..d5a94fcf90 100644
--- a/Cubical/Algebra/SymmetricGroup.agda
+++ b/Cubical/Algebra/SymmetricGroup.agda
@@ -69,8 +69,8 @@ SymUnit≡Unit = uaGroup SymUnit≃Unit
 
 SymBool≃Bool : GroupEquiv (SymGroup Bool isSetBool) BoolGroup
 SymBool≃Bool = GroupIso→GroupEquiv $ invGroupIso $ ≅Bool $
-  Bool ≃ Bool Iso⟨ invIso reflectIso ⟩
-  Bool ≡ Bool Iso⟨ invIso univalenceIso ⟩
+  Bool ≃ Bool Iso⟨ invIso univalenceIso ⟩
+  Bool ≡ Bool Iso⟨ invIso reflectIso ⟩
   Bool        ∎Iso
   where open BoolReflection