From 674aae49cde490bb1486f06d9bc6128c5ed476f2 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Tue, 19 Feb 2019 08:24:38 +0000
Subject: [PATCH] Groups lectures (#25)

---
 DecidableSet.agda          |  10 ++
 Groups/FreeGroups.agda     | 221 +++++++++++++++++++++++++++++++++----
 Groups/GeneratedGroup.agda | 116 +++++++++++++++++++
 Groups/GroupActions.agda   | 220 ++++++++++++++++++++++++++++++++----
 Groups/Groups.agda         |   8 --
 Groups/GroupsLemmas.agda   |   8 ++
 Groups/SymmetryGroups.agda |  22 ----
 Setoids/Lists.agda         |  59 ++++++++++
 8 files changed, 593 insertions(+), 71 deletions(-)
 create mode 100644 DecidableSet.agda
 create mode 100644 Groups/GeneratedGroup.agda
 create mode 100644 Setoids/Lists.agda

diff --git a/DecidableSet.agda b/DecidableSet.agda
new file mode 100644
index 0000000..37a7407
--- /dev/null
+++ b/DecidableSet.agda
@@ -0,0 +1,10 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import LogicalFormulae
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module DecidableSet where
+
+  record DecidableSet {a : _} (A : Set a) : Set a where
+    field
+      eq : (a b : A) → ((a ≡ b) || ((a ≡ b) → False))
diff --git a/Groups/FreeGroups.agda b/Groups/FreeGroups.agda
index 491d0be..64444be 100644
--- a/Groups/FreeGroups.agda
+++ b/Groups/FreeGroups.agda
@@ -1,32 +1,211 @@
 {-# OPTIONS --safe --warning=error #-}
 
 open import LogicalFormulae
-open import Setoids
+open import Setoids.Setoids
 open import Functions
 open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-open import Naturals
-open import FinSet
-open import Groups
+open import Numbers.Naturals
+open import Sets.FinSet
+open import Groups.GroupDefinition
+open import Groups.SymmetryGroups
+open import DecidableSet
 
-module FreeGroups where
+module Groups.FreeGroups where
   data FreeCompletion {a : _} (A : Set a) : Set a where
-    letter : A → FreeCompletion A
-    inv : A → FreeCompletion A
+    ofLetter : A → FreeCompletion A
+    ofInv : A → FreeCompletion A
 
-  data FreeGroup {a : _} (A : Set a) : Set a where
-    emptyWord : FreeGroup A
-    append : FreeCompletion A → FreeGroup A → FreeGroup A
+  freeInverse : {a : _} {A : Set a} (l : FreeCompletion A) → FreeCompletion A
+  freeInverse (ofLetter x) = ofInv x
+  freeInverse (ofInv x) = ofLetter x
 
-  reduceWord : {a : _} {A : Set a} → (FreeGroup {a} A) → FreeGroup A
-  reduceWord emptyWord = emptyWord
-  reduceWord (append (letter x) emptyWord) = append (letter x) emptyWord
-  reduceWord (append (letter x) (append (letter x1) w)) = append (letter x) (reduceWord (append (letter x1) w))
-  reduceWord (append (letter x) (append (inv x₁) w)) = {!!}
-  reduceWord (append (inv x) w) = {!!}
+  ofLetterInjective : {a : _} {A : Set a} {x y : A} → (ofLetter x ≡ ofLetter y) → x ≡ y
+  ofLetterInjective refl = refl
 
-  freeGroupSetoid : {a : _} (A : Set a) → Setoid A
-  Setoid._∼_ (freeGroupSetoid A) = {!!}
-  Setoid.eq (freeGroupSetoid A) = {!!}
+  ofInvInjective : {a : _} {A : Set a} {x y : A} → (ofInv x ≡ ofInv y) → x ≡ y
+  ofInvInjective refl = refl
 
-  freeGroup : {a : _} (A : Set a) → Group (freeGroupSetoid A) {!!}
-  freeGroup A = {!!}
+  decidableFreeCompletion : {a : _} {A : Set a} → DecidableSet A → DecidableSet (FreeCompletion A)
+  decidableFreeCompletion {A = A} record { eq = eq } = record { eq = pr }
+    where
+      pr : (a b : FreeCompletion A) → (a ≡ b) || (a ≡ b → False)
+      pr (ofLetter x) (ofLetter y) with eq x y
+      ... | inl refl = inl refl
+      ... | inr x!=y = inr λ p → x!=y (ofLetterInjective p)
+      pr (ofLetter x) (ofInv y) = inr λ ()
+      pr (ofInv x) (ofLetter y) = inr λ ()
+      pr (ofInv x) (ofInv y) with eq x y
+      ... | inl refl = inl refl
+      ... | inr x!=y = inr λ p → x!=y (ofInvInjective p)
+
+  freeCompletionEqual : {a : _} {A : Set a} (dec : DecidableSet A) (x y : FreeCompletion A) → Bool
+  freeCompletionEqual dec x y with DecidableSet.eq (decidableFreeCompletion dec) x y
+  freeCompletionEqual dec x y | inl x₁ = BoolTrue
+  freeCompletionEqual dec x y | inr x₁ = BoolFalse
+
+  freeCompletionEqualFalse : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → ((x ≡ y) → False) → (freeCompletionEqual dec x y) ≡ BoolFalse
+  freeCompletionEqualFalse dec {x = x} {y} x!=y with DecidableSet.eq (decidableFreeCompletion dec) x y
+  freeCompletionEqualFalse dec {x} {y} x!=y | inl x=y = exFalso (x!=y x=y)
+  freeCompletionEqualFalse dec {x} {y} x!=y | inr _ = refl
+
+  freeCompletionEqualFalse' : {a : _} {A : Set a} (dec : DecidableSet A) {x y : FreeCompletion A} → (freeCompletionEqual dec x y) ≡ BoolFalse → (x ≡ y) → False
+  freeCompletionEqualFalse' dec {x} {y} pr with DecidableSet.eq (decidableFreeCompletion dec) x y
+  freeCompletionEqualFalse' dec {x} {y} () | inl x₁
+  freeCompletionEqualFalse' dec {x} {y} pr | inr ans = ans
+
+  data ReducedWord {a : _} {A : Set a} (decA : DecidableSet A) : Set a
+  wordLength : {a : _} {A : Set a} {decA : DecidableSet A} → ReducedWord decA → ℕ
+  firstLetter : {a : _} {A : Set a} {decA : DecidableSet A} → (w : ReducedWord decA) → (0 <N wordLength w) → FreeCompletion A
+
+  data PrependIsValid {a : _} {A : Set a} (decA : DecidableSet A) (w : ReducedWord decA) (l : FreeCompletion A) : Set a where
+    wordEmpty : wordLength w ≡ 0 → PrependIsValid decA w l
+    wordEnding : (pr : 0 <N wordLength w) → (freeCompletionEqual decA l (freeInverse (firstLetter w pr)) ≡ BoolFalse) → PrependIsValid decA w l
+
+  data ReducedWord {a} {A} decA where
+    empty : ReducedWord decA
+    prependLetter : (letter : FreeCompletion A) → (w : ReducedWord decA) → PrependIsValid decA w letter → ReducedWord decA
+
+  firstLetter {a} {A} empty (le x ())
+  firstLetter {a} {A} (prependLetter letter w x) pr = letter
+
+  wordLength {a} {A} empty = 0
+  wordLength {a} {A} (prependLetter letter w pr) = succ (wordLength w)
+
+  data FreeGroupGenerators {a : _} (A : Set a) : Set a where
+    χ : A → FreeGroupGenerators A
+
+  prependLetterInjective : {a : _} {A : Set a} {decA : DecidableSet A} {x : FreeCompletion A} {w1 w2 : ReducedWord decA} {pr1 : PrependIsValid decA w1 x} {pr2 : PrependIsValid decA w2 x} → prependLetter x w1 pr1 ≡ prependLetter x w2 pr2 → w1 ≡ w2
+  prependLetterInjective {x = x} {w1} {.w1} {pr1} {.pr1} refl = refl
+
+  prependLetterInjective' : {a : _} {A : Set a} {decA : DecidableSet A} {x y : FreeCompletion A} {w1 w2 : ReducedWord decA} {pr1 : PrependIsValid decA w1 x} {pr2 : PrependIsValid decA w2 y} → prependLetter x w1 pr1 ≡ prependLetter y w2 pr2 → x ≡ y
+  prependLetterInjective' refl = refl
+
+  prependLetterRefl : {a : _} {A : Set a} {decA : DecidableSet A} {x : FreeCompletion A} {w : ReducedWord decA} → {pr1 pr2 : PrependIsValid decA w x} → prependLetter x w pr1 ≡ prependLetter x w pr2
+  prependLetterRefl {a} {A} {decA} {x} {empty} {wordEmpty refl} {wordEmpty refl} = refl
+  prependLetterRefl {a} {A} {decA} {x} {empty} {wordEmpty refl} {wordEnding (le x₁ ()) x₂}
+  prependLetterRefl {a} {A} {decA} {x} {empty} {wordEnding (le x₂ ()) x₁} {pr2}
+  prependLetterRefl {a} {A} {decA} {x} {prependLetter letter w x₁} {wordEmpty ()} {pr2}
+  prependLetterRefl {a} {A} {decA} {x} {prependLetter letter w x₁} {wordEnding pr x₂} {wordEmpty ()}
+  prependLetterRefl {a} {A} {decA} {x} {prependLetter letter w x₁} {wordEnding pr2 r2} {wordEnding pr1 r1} rewrite <NRefl pr1 (succIsPositive (wordLength w)) | <NRefl pr2 (succIsPositive (wordLength w)) | reflRefl r1 r2 = refl
+
+  badPrepend : {a : _} {A : Set a} {decA : DecidableSet A} {x : A} {w : ReducedWord decA} {pr : PrependIsValid decA w (ofInv x)} → (PrependIsValid decA (prependLetter (ofInv x) w pr) (ofLetter x)) → False
+  badPrepend (wordEmpty ())
+  badPrepend {decA = decA} {x = x} (wordEnding pr bad) with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofLetter x)
+  badPrepend {decA = decA} {x} (wordEnding pr ()) | inl x₁
+  badPrepend {decA = decA} {x} (wordEnding pr bad) | inr pr2 = pr2 refl
+
+  badPrepend' : {a : _} {A : Set a} {decA : DecidableSet A} {x : A} {w : ReducedWord decA} {pr : PrependIsValid decA w (ofLetter x)} → (PrependIsValid decA (prependLetter (ofLetter x) w pr) (ofInv x)) → False
+  badPrepend' (wordEmpty ())
+  badPrepend' {decA = decA} {x = x} (wordEnding pr x₁) with DecidableSet.eq (decidableFreeCompletion decA) (ofInv x) (ofInv x)
+  badPrepend' {decA = decA} {x} (wordEnding pr ()) | inl x₂
+  badPrepend' {decA = decA} {x} (wordEnding pr x₁) | inr pr2 = pr2 refl
+
+  freeGroupGenerators : {a : _} (A : Set a) (decA : DecidableSet A) (w : FreeGroupGenerators A) → SymmetryGroupElements (reflSetoid (ReducedWord decA))
+  freeGroupGenerators A decA (χ x) = sym {f = f} bij
+    where
+      open DecidableSet.DecidableSet decA
+      f : ReducedWord decA → ReducedWord decA
+      f empty = prependLetter (ofLetter x) empty (wordEmpty refl)
+      f (prependLetter (ofLetter startLetter) w pr) = prependLetter (ofLetter x) (prependLetter (ofLetter startLetter) w pr) (wordEnding (succIsPositive _) ans)
+        where
+          ans : freeCompletionEqual decA (ofLetter x) (ofInv startLetter) ≡ BoolFalse
+          ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
+          ... | bl = refl
+      f (prependLetter (ofInv startLetter) w pr) with DecidableSet.eq decA startLetter x
+      f (prependLetter (ofInv startLetter) w pr) | inl startLetter=x = w
+      f (prependLetter (ofInv startLetter) w pr) | inr startLetter!=x = prependLetter (ofLetter x) (prependLetter (ofInv startLetter) w pr) (wordEnding (succIsPositive _) ans)
+        where
+          ans : freeCompletionEqual decA (ofLetter x) (ofLetter startLetter) ≡ BoolFalse
+          ans with DecidableSet.eq (decidableFreeCompletion decA) (ofLetter x) (ofInv startLetter)
+          ans | bl with eq x startLetter
+          ans | bl | inl x=sl = exFalso (startLetter!=x (equalityCommutative x=sl))
+          ans | bl | inr x!=sl = refl
+      bij : SetoidBijection (reflSetoid (ReducedWord decA)) (reflSetoid (ReducedWord decA)) f
+      SetoidInjection.wellDefined (SetoidBijection.inj bij) x=y rewrite x=y = refl
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {empty} fx=fy = refl
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofLetter x₁) y pr1} ()
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy with DecidableSet.eq decA l x
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEmpty x₁)} () | inl l=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) empty (wordEnding (le x ()) x₁)} fx=fy | inl l=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEmpty ())} fx=fy | inl l=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofLetter x₂) y x₁) (wordEnding pr bad)} fx=fy | inl refl with ofLetterInjective (prependLetterInjective' fx=fy)
+      ... | l=x2 = exFalso ((freeCompletionEqualFalse' decA bad) (applyEquality ofInv l=x2))
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) (prependLetter (ofInv x₂) y x₁) pr1} () | inl l=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x with prependLetterInjective fx=fy
+      SetoidInjection.injective (SetoidBijection.inj bij) {empty} {prependLetter (ofInv l) y pr1} fx=fy | inr l!=x | ()
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy with prependLetterInjective fx=fy
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {empty} fx=fy | ()
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter x) w1 prX} {prependLetter (ofLetter y) w2 prY} fx=fy = prependLetterInjective fx=fy
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy with eq y x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) empty prY} () | inl y=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) prY} fx=fy | inl y=x with ofLetterInjective (prependLetterInjective' fx=fy)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEmpty ())} fx=fy | inl y=x | x=b
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofLetter b) w2 x₁) (wordEnding pr bad)} fx=fy | inl y=x | x=b rewrite x=b | y=x = exFalso (freeCompletionEqualFalse' decA bad refl)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x with prependLetterInjective' fx=fy
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) (prependLetter (ofInv b) w2 x₁) prY} fx=fy | inl y=x | ()
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofLetter a) w1 prX} {prependLetter (ofInv y) w2 prY} fx=fy | inr y!=x with prependLetterInjective fx=fy
+      ... | bl = bl
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} fx=fy with eq a x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {empty} () | inl a=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) prX} {empty} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEmpty ())} {empty} fx=fy | inl a=x | x2=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₂) w1 x₁) (wordEnding pr x3)} {empty} fx=fy | inl a=x | x2=x with freeCompletionEqualFalse' decA x3
+      ... | bl = exFalso (bl (applyEquality ofInv (transitivity a=x (equalityCommutative x2=x))))
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₂) w1 x₁) prX} {empty} () | inl a=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {empty} () | inr a!=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} fx=fy with eq a x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofLetter b) y x₂} () | inl a=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with ofLetterInjective (prependLetterInjective' fx=fy)
+      ... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x with prependLetterInjective' fx=fy
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofLetter b) y x₂} fx=fy | inl a=x | ()
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofLetter x₁) y x₂} () | inr a!=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv x₁) y x₂} fx=fy with eq a x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x with eq b x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inl b=x rewrite fx=fy | a=x | b=x = prependLetterRefl
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) empty prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofLetter x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} fx=fy | inl a=x | inr b!=x with ofLetterInjective (prependLetterInjective' fx=fy)
+      ... | x3=x rewrite a=x | x3=x = exFalso (badPrepend' prX)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) (prependLetter (ofInv x₃) w1 x₁) prX} {prependLetter (ofInv b) y x₂} () | inl a=x | inr b!=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x with eq b x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) empty x₂} () | inr a!=x | inl b=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofLetter x₃) y x₁) x2} fx=fy | inr a!=x | inl b=x with ofLetterInjective (prependLetterInjective' fx=fy)
+      ... | x3=x rewrite (equalityCommutative x3=x) | b=x = exFalso (badPrepend' x2)
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) (prependLetter (ofInv x₃) y x₁) x₂} () | inr a!=x | inl b=x
+      SetoidInjection.injective (SetoidBijection.inj bij) {prependLetter (ofInv a) w1 prX} {prependLetter (ofInv b) y x₂} fx=fy | inr a!=x | inr b!=x = prependLetterInjective fx=fy
+      SetoidSurjection.wellDefined (SetoidBijection.surj bij) x=y rewrite x=y = refl
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {empty} = prependLetter (ofInv x) empty (wordEmpty refl) , needed
+        where
+          needed : f (prependLetter (ofInv x) empty (wordEmpty refl)) ≡ empty
+          needed with DecidableSet.eq decA x x
+          needed | inl x₁ = refl
+          needed | inr x!=x = exFalso (x!=x refl)
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} with DecidableSet.eq decA x l
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEmpty refl)} | inl refl = empty , refl
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter x) empty (wordEnding (le x₂ ()) x₁)} | inl refl
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) empty pr} | inr x!=l = prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA (λ p → x!=l (ofInvInjective p)))) , needed
+        where
+          needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) empty pr) (wordEnding (succIsPositive 0) (freeCompletionEqualFalse decA {ofInv x} {ofInv l} λ p → x!=l (ofInvInjective p)))) ≡ prependLetter (ofLetter l) empty pr
+          needed with DecidableSet.eq decA x x
+          ... | inl _ = refl
+          ... | inr bad = exFalso (bad refl)
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} with DecidableSet.eq decA l x
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofLetter y) w pr2) pr} | inl l=x rewrite l=x = prependLetter (ofLetter y) w pr2 , prependLetterRefl
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr} | inl l=x = prependLetter (ofInv y) w pr2 , needed
+        where
+          needed : f (prependLetter (ofInv y) w pr2) ≡ prependLetter (ofLetter l) (prependLetter (ofInv y) w pr2) pr
+          needed with DecidableSet.eq decA y x
+          needed | inl y=x rewrite l=x | y=x = exFalso (badPrepend pr)
+          needed | inr y!=x rewrite l=x = prependLetterRefl
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofLetter l) (prependLetter letter w pr2) pr} | inr l!=x = prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA λ p → l!=x (ofInvInjective (equalityCommutative p)))) , needed
+        where
+          needed : f (prependLetter (ofInv x) (prependLetter (ofLetter l) (prependLetter letter w pr2) pr) (wordEnding (succIsPositive (succ (wordLength w))) (freeCompletionEqualFalse decA (λ p → l!=x (ofInvInjective (equalityCommutative p)))))) ≡ prependLetter (ofLetter l) (prependLetter letter w pr2) pr
+          needed with eq x x
+          needed | inl x₁ = refl
+          needed | inr x!=x = exFalso (x!=x refl)
+      SetoidSurjection.surjective (SetoidBijection.surj bij) {prependLetter (ofInv l) w pr} = prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive _) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ())) , needed
+        where
+          needed : f (prependLetter (ofInv x) (prependLetter (ofInv l) w pr) (wordEnding (succIsPositive (wordLength w)) (freeCompletionEqualFalse decA {ofInv x} {ofLetter l} λ ()))) ≡ (prependLetter (ofInv l) w pr)
+          needed with eq x x
+          needed | inl x₁ = refl
+          needed | inr x!=x = exFalso (x!=x refl)
diff --git a/Groups/GeneratedGroup.agda b/Groups/GeneratedGroup.agda
new file mode 100644
index 0000000..f83cd76
--- /dev/null
+++ b/Groups/GeneratedGroup.agda
@@ -0,0 +1,116 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import LogicalFormulae
+open import Setoids.Setoids
+open import Setoids.Lists
+open import Functions
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Numbers.Naturals
+open import Sets.FinSet
+open import Groups.GroupDefinition
+open import Lists
+open import Orders
+open import Groups.Groups
+
+module Groups.GeneratedGroup where
+  data FreeCompletion {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
+    ofLetter : A → FreeCompletion S
+    ofInv : A → FreeCompletion S
+
+  freeCompletionMap : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → FreeCompletion S → FreeCompletion T
+  freeCompletionMap f (ofLetter x) = ofLetter (f x)
+  freeCompletionMap f (ofInv x) = ofInv (f x)
+
+  freeInverse : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (l : FreeCompletion S) → FreeCompletion S
+  freeInverse (ofLetter x) = ofInv x
+  freeInverse (ofInv x) = ofLetter x
+
+  freeCompletionSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (FreeCompletion S)
+  (freeCompletionSetoid S Setoid.∼ ofLetter w) (ofLetter x) = Setoid._∼_ S w x
+  (freeCompletionSetoid S Setoid.∼ ofLetter w) (ofInv x) = False'
+  (freeCompletionSetoid S Setoid.∼ ofInv w) (ofLetter x) = False'
+  (freeCompletionSetoid S Setoid.∼ ofInv w) (ofInv x) = Setoid._∼_ S w x
+  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter x} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv x} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofInv x} ()
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofLetter x} ()
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} {ofLetter y} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofLetter x} {ofInv y} _ ()
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofLetter w} {ofInv x} {y} ()
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofLetter x} {y} ()
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} {ofLetter y} _ ()
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (freeCompletionSetoid S))) {ofInv w} {ofInv x} {ofInv y} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))
+
+  freeCompletionMapWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → ({x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)) → {x y : FreeCompletion S} → (Setoid._∼_ (freeCompletionSetoid S) x y) → (Setoid._∼_ (freeCompletionSetoid T) (freeCompletionMap f x) (freeCompletionMap f y))
+  freeCompletionMapWellDefined f fWD {ofLetter x} {ofLetter x₁} w1=w2 = fWD w1=w2
+  freeCompletionMapWellDefined f fWD {ofLetter x} {ofInv x₁} ()
+  freeCompletionMapWellDefined f fWD {ofInv x} {ofLetter x₁} ()
+  freeCompletionMapWellDefined f fWD {ofInv x} {ofInv x₁} w1=w2 = fWD w1=w2
+
+  record Word {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
+    field
+      word : List (FreeCompletion S)
+
+  wordSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (Word S)
+  (wordSetoid S Setoid.∼ record { word = word1 }) record { word = word2 } = Setoid._∼_ (listSetoid (freeCompletionSetoid S)) word1 word2
+  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (wordSetoid S))) {record { word = word }} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (listSetoid (freeCompletionSetoid S))))
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (wordSetoid S))) {record { word = word1 }} {record { word = word2 }} pr = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (listSetoid (freeCompletionSetoid S)))) pr
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (wordSetoid S))) {record { word = word1 }} {record { word = word2 }} {record { word = word3 }} pr1 pr2 = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (listSetoid (freeCompletionSetoid S)))) pr1 pr2
+
+  evalWord : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) (w : Word S) → A
+  evalWord G record { word = [] } = Group.identity G
+  evalWord {_+_ = _+_} G record { word = (ofLetter x :: w) } = x + evalWord G record { word = w }
+  evalWord {_+_ = _+_} G record { word = (ofInv x :: w) } = (Group.inverse G x) + evalWord G record { word = w }
+
+  mapWord : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) (w : Word S) → Word T
+  mapWord f record { word = word } = record { word = listMap (freeCompletionMap f) word }
+
+  subgroupSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Setoid (Word T)
+  Setoid._∼_ (subgroupSetoid {S = S} T G {f} fInj) w1 w2 = Setoid._∼_ S (evalWord G (mapWord f w1)) (evalWord G (mapWord f w2))
+  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (subgroupSetoid {S = S} T G {f} fInj))) = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))
+
+  evalWordWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} (G : Group S _+_) (w1 w2 : Word S) → Setoid._∼_ (wordSetoid S) w1 w2 → Setoid._∼_ S (evalWord G w1) (evalWord G w2)
+  evalWordWellDefined {S = S} G record { word = [] } record { word = [] } w1=w2 = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  evalWordWellDefined G record { word = [] } record { word = (x :: word) } ()
+  evalWordWellDefined {_+_ = _+_} G record { word = (x :: xs) } record { word = [] } ()
+  evalWordWellDefined {_+_ = _+_} G record { word = (ofLetter x :: xs) } record { word = (ofLetter y :: ys) } (x=y ,, snd) = Group.wellDefined G x=y (evalWordWellDefined G record { word = xs } record { word = ys } snd)
+  evalWordWellDefined {_+_ = _+_} G record { word = (ofLetter x :: xs) } record { word = (ofInv y :: ys) } (() ,, snd)
+  evalWordWellDefined {_+_ = _+_} G record { word = (ofInv x :: xs) } record { word = (ofLetter y :: ys) } (() ,, snd)
+  evalWordWellDefined {_+_ = _+_} G record { word = (ofInv x :: xs) } record { word = (ofInv y :: ys) } (x=y ,, snd) = Group.wellDefined G (inverseWellDefined G x=y) (evalWordWellDefined G record { word = xs } record { word = ys } snd)
+
+  mapWordWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} (f : A → B) → ({x y : A} → (Setoid._∼_ S x y) → (Setoid._∼_ T (f x) (f y))) → {w1 : Word S} {w2 : Word S} → Setoid._∼_ (wordSetoid S) w1 w2 → Setoid._∼_ (wordSetoid T) (mapWord f w1) (mapWord f w2)
+  mapWordWellDefined {S = S} {T = T} f fWD {w1} {w2} w1=w2 = p
+    where
+      p : listEquality (freeCompletionSetoid T) (listMap (freeCompletionMap {S = S} {T = T} f) (Word.word w1)) (listMap (freeCompletionMap f) (Word.word w2))
+      p = listEqualityRespectsMap (freeCompletionSetoid S) (freeCompletionSetoid T) (freeCompletionMap {S = S} {T} f) (λ {x} {y} → freeCompletionMapWellDefined {S = S} {T = T} f fWD {x} {y}) {w1 = Word.word w1} {w2 = Word.word w2} w1=w2
+
+  subgroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Word T → Word T → Word T
+  subgroupOp T G fInj record { word = word1 } record { word = word2 } = record { word = word1 ++ word2 }
+
+  generatedSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} (T : Setoid {b} {d} B) {_+_ : A → A → A} (G : Group S _+_) {f : B → A} (fInj : SetoidInjection T S f) → Group (subgroupSetoid T G fInj) (subgroupOp T G fInj)
+  Group.wellDefined (generatedSubgroup {S = S} T G {f = f} fInj) {record { word = w }} {record { word = x }} {record { word = y }} {record { word = z }} w=y x=z = need
+    where
+      need : Setoid._∼_ (subgroupSetoid T G fInj) (subgroupOp T G fInj (record { word = w }) (record { word = x })) (subgroupOp T G fInj (record { word = y }) (record { word = z }))
+      need = {!!}
+  Group.identity (generatedSubgroup T G fInj) = record { word = [] }
+  Group.inverse (generatedSubgroup T G fInj) record { word = word } = record { word = listMap freeInverse (listRev word) }
+  Group.multAssoc (generatedSubgroup T G fInj) = {!!}
+  Group.multIdentRight (generatedSubgroup {S = S} T G {f = f} fInj) {a = record { word = word }} = need
+    where
+      open Setoid S
+      open Group G
+      need : evalWord G (mapWord f (record { word = word ++ [] })) ∼ evalWord G (mapWord f record { word = word })
+      need = {!!}
+  Group.multIdentLeft (generatedSubgroup {S = S} T G {f = f} fInj) = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  Group.invLeft (generatedSubgroup {S = S} T G {f} fInj) {record { word = [] }} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+  Group.invLeft (generatedSubgroup {S = S} T G {f} fInj) {record { word = x :: word }} = need
+    where
+      open Setoid S
+      open Group G
+      need : Setoid._∼_ (subgroupSetoid T G fInj) (record { word = (listMap freeInverse (listRev (x :: word))) ++ (x :: word) }) (Group.identity (generatedSubgroup T G fInj))
+      need = {!!}
+  Group.invRight (generatedSubgroup T G fInj) = {!!}
diff --git a/Groups/GroupActions.agda b/Groups/GroupActions.agda
index f6113f4..cb968f3 100644
--- a/Groups/GroupActions.agda
+++ b/Groups/GroupActions.agda
@@ -7,7 +7,9 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Numbers.Naturals
 open import Sets.FinSet
 open import Groups.GroupDefinition
+open import Groups.GroupsLemmas
 open import Groups.Groups
+open import Groups.SymmetryGroups
 open import Groups.Groups2
 
 module Groups.GroupActions where
@@ -25,9 +27,8 @@ module Groups.GroupActions where
     trivialAction : {m n o p : _} {A : Set m} {S : Setoid {m} {o} A} {_·_ : A → A → A} {B : Set n} (G : Group S _·_) (X : Setoid {n} {p} B) → GroupAction G X
     trivialAction G X = record { action = λ _ x → x ; actionWellDefined1 = λ _ → reflexive ; actionWellDefined2 = λ wd1 → wd1 ; identityAction = reflexive ; associativeAction = reflexive }
       where
-        open Setoid X
-        open Equivalence eq
-        open Reflexive reflexiveEq
+        open Setoid X renaming (eq to setoidEq)
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq X))
 
     leftRegularAction : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} (G : Group S _·_) → GroupAction G S
     GroupAction.action (leftRegularAction {_·_ = _·_} G) g h = g · h
@@ -36,15 +37,14 @@ module Groups.GroupActions where
     GroupAction.actionWellDefined1 (leftRegularAction {S = S} G) eq1 = wellDefined eq1 reflexive
       where
         open Group G
-        open Setoid S
-        open Equivalence eq
-        open Reflexive reflexiveEq
+        open Setoid S renaming (eq to setoidEq)
+        open Equivalence setoidEq
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
     GroupAction.actionWellDefined2 (leftRegularAction {S = S} G) {g} {x} {y} eq1 = wellDefined reflexive eq1
       where
         open Group G
         open Setoid S
-        open Equivalence eq
-        open Reflexive reflexiveEq
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
     GroupAction.identityAction (leftRegularAction G) = multIdentLeft
       where
         open Group G
@@ -52,17 +52,15 @@ module Groups.GroupActions where
       where
         open Group G
         open Setoid S
-        open Equivalence eq
-        open Symmetric symmetricEq
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
 
     conjugationAction : {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_·_ : A → A → A} → (G : Group S _·_) → GroupAction G S
     conjugationAction {S = S} {_·_ = _·_} G = record { action = λ g h → (g · h) · (inverse g) ; actionWellDefined1 = λ gh → wellDefined (wellDefined gh reflexive) (inverseWellDefined G gh) ; actionWellDefined2 = λ x~y → wellDefined (wellDefined reflexive x~y) reflexive ; identityAction = transitive (wellDefined reflexive (invIdentity G)) (transitive multIdentRight multIdentLeft)  ; associativeAction = λ {x} {g} {h} → transitive (wellDefined reflexive (invContravariant G)) (transitive multAssoc (wellDefined (fourWayAssoc' G) reflexive)) }
       where
         open Group G
         open Setoid S
-        open Equivalence eq
-        open Reflexive reflexiveEq
-        open Transitive transitiveEq
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq S))
 
     conjugationNormalSubgroupAction : {m n o p : _} {A : Set m} {B : Set o} {S : Setoid {m} {n} A} {T : Setoid {o} {p} B} {_·A_ : A → A → A} {_·B_ : B → B → B} → (G : Group S _·A_) → (H : Group T _·B_) → {underF : A → B} (f : GroupHom G H underF) → GroupAction G (quotientGroupSetoid G f)
     GroupAction.action (conjugationNormalSubgroupAction {_·A_ = _·A_} G H {f} fHom) a b = a ·A (b ·A (Group.inverse G a))
@@ -70,9 +68,8 @@ module Groups.GroupActions where
       where
         open Group G
         open Setoid T
-        open Equivalence (Setoid.eq T)
-        open Transitive transitiveEq
-        open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
         open Reflexive (Equivalence.reflexiveEq (Setoid.eq S))
         ans : f ((g ·A (x ·A (inverse g))) ·A inverse (h ·A (x ·A inverse h))) ∼ Group.identity H
         ans = transitive (GroupHom.wellDefined fHom (transferToRight'' G (Group.wellDefined G g~h (Group.wellDefined G reflexive (inverseWellDefined G g~h))))) (imageOfIdentityIsIdentity fHom)
@@ -80,8 +77,7 @@ module Groups.GroupActions where
       where
         open Group G
         open Setoid T
-        open Equivalence (Setoid.eq T)
-        open Transitive transitiveEq
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
         open Transitive (Equivalence.transitiveEq (Setoid.eq S)) renaming (transitive to transitiveG)
         open Symmetric (Equivalence.symmetricEq (Setoid.eq S))
         open Symmetric (Equivalence.symmetricEq (Setoid.eq T)) renaming (symmetric to symmetricH)
@@ -124,8 +120,7 @@ module Groups.GroupActions where
         open Group G
         open Setoid S
         open Setoid T renaming (_∼_ to _∼T_)
-        open Equivalence (Setoid.eq T)
-        open Transitive transitiveEq
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
         i : Setoid._∼_ S (x ·A inverse identity) x
         i = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) (wellDefined (Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))) (invIdentity G)) multIdentRight
         h : identity ·A (x ·A inverse identity) ∼ x
@@ -146,3 +141,188 @@ module Groups.GroupActions where
         ans : f (((g ·A h) ·A (x ·A inverse (g ·A h))) ·A inverse ((g ·A ((h ·A (x ·A inverse h)) ·A inverse g)))) ∼T Group.identity H
         ans = transitiveH (GroupHom.wellDefined fHom (transferToRight'' G (transitiveG (symmetricG multAssoc) (Group.wellDefined G reflexive (transitiveG (wellDefined reflexive (transitiveG (wellDefined reflexive (invContravariant G)) multAssoc)) multAssoc))))) (imageOfIdentityIsIdentity fHom)
 
+    actionPermutation : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} → (action : GroupAction G T) → (g : A) → SymmetryGroupElements T
+    actionPermutation {B = B} {T = T} {_+_ = _+_} {G = G} action g = sym {f = λ x → (GroupAction.action action g x)} (record { inj = record { injective = inj ; wellDefined = GroupAction.actionWellDefined2 action } ; surj = record { surjective = surj ; wellDefined = GroupAction.actionWellDefined2 action } })
+      where
+        open Setoid T
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        open Group G
+        inj : {x y : B} → (Setoid._∼_ T (GroupAction.action action g x) (GroupAction.action action g y)) → Setoid._∼_ T x y
+        inj {x} {y} gx=gy = transitive (symmetric (GroupAction.identityAction action)) (transitive (transitive (symmetric (GroupAction.actionWellDefined1 action (invLeft {g}))) (transitive (transitive (GroupAction.associativeAction action) (transitive (GroupAction.actionWellDefined2 action gx=gy) (symmetric (GroupAction.associativeAction action)))) (GroupAction.actionWellDefined1 action (invLeft {g})))) (GroupAction.identityAction action))
+        surj : {x : B} → Sg B (λ a → GroupAction.action action g a ∼ x)
+        surj {x} = GroupAction.action action (inverse g) x , transitive (symmetric (GroupAction.associativeAction action)) (transitive (GroupAction.actionWellDefined1 action invRight) (GroupAction.identityAction action))
+
+    actionPermutationMapIsHom : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) → GroupHom G (symmetricGroup T) (actionPermutation action)
+    GroupHom.groupHom (actionPermutationMapIsHom {T = T} action) = ExtensionallyEqual.eq λ {z} → GroupAction.associativeAction action
+      where
+        open Setoid T
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+    GroupHom.wellDefined (actionPermutationMapIsHom action) x=y = ExtensionallyEqual.eq λ {z} → GroupAction.actionWellDefined1 action x=y
+
+    data Stabiliser {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) : Set (a ⊔ b ⊔ c ⊔ d) where
+      stab : (g : A) → Setoid._∼_ T (GroupAction.action action g x) x → Stabiliser action x
+
+    stabiliserSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Setoid (Stabiliser action x)
+    Setoid._∼_ (stabiliserSetoid {S = S} action x) (stab g gx=x) (stab h hx=x) = Setoid._∼_ S g h
+    Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (stabiliserSetoid {S = S} action x))) {stab g _} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+    Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (stabiliserSetoid {S = S} action x))) {stab g _} {stab h _} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S))
+    Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (stabiliserSetoid {S = S} action x))) {stab g _} {stab h _} {stab i _} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S))
+
+    stabiliserGroupOp : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Stabiliser action x → Stabiliser action x → Stabiliser action x
+    stabiliserGroupOp {T = T} {_+_ = _+_} action (stab p px=x) (stab q qx=x) = stab (p + q) (transitive (GroupAction.associativeAction action) (transitive (GroupAction.actionWellDefined2 action qx=x) px=x))
+      where
+        open Setoid T
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+
+    stabiliserGroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Group (stabiliserSetoid action x) (stabiliserGroupOp action)
+    Group.wellDefined (stabiliserGroup {T = T} {G = G} action {x}) {stab m mx=x} {stab n nx=x} {stab r rx=x} {stab s sx=x} m=r n=s = Group.wellDefined G m=r n=s
+      where
+        open Setoid T
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+    Group.identity (stabiliserGroup {G = G} action) = stab (Group.identity G) (GroupAction.identityAction action)
+    Group.inverse (stabiliserGroup {T = T} {_+_ = _+_} {G = G} action {x}) (stab g gx=x) = stab (Group.inverse G g) (transitive {_} {GroupAction.action action ((inverse g) + g) x} (symmetric (transitive (GroupAction.associativeAction action) (GroupAction.actionWellDefined2 action gx=x))) (transitive (GroupAction.actionWellDefined1 action invLeft) (GroupAction.identityAction action)))
+      where
+        open Group G
+        open Setoid T
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+    Group.multAssoc (stabiliserGroup {G = G} action) {stab m mx=x} {stab n nx=x} {stab o ox=x} = Group.multAssoc G
+    Group.multIdentRight (stabiliserGroup {G = G} action) {stab m mx=x} = Group.multIdentRight G
+    Group.multIdentLeft (stabiliserGroup {G = G} action) {stab m mx=x }= Group.multIdentLeft G
+    Group.invLeft (stabiliserGroup {G = G} action) {stab m mx=x} = Group.invLeft G
+    Group.invRight (stabiliserGroup {G = G} action) {stab m mx=x} = Group.invRight G
+
+    stabiliserInjection : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Stabiliser action x → A
+    stabiliserInjection action (stab g gx=x) = g
+
+    stabiliserInjectionIsHom : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → GroupHom (stabiliserGroup action {x}) G (stabiliserInjection action {x})
+    GroupHom.groupHom (stabiliserInjectionIsHom {S = S} action) {stab g gx=x} {stab h hx=x} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S))
+    GroupHom.wellDefined (stabiliserInjectionIsHom action) {stab g gx=x} {stab h hx=x} g=h = g=h
+
+    stabiliserIsSubgroup : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) {x : B} → Subgroup G (stabiliserGroup action) (stabiliserInjectionIsHom action {x})
+    SetoidInjection.wellDefined (Subgroup.fInj (stabiliserIsSubgroup action)) {stab g gx=x} {stab h hx=x} g=h = g=h
+    SetoidInjection.injective (Subgroup.fInj (stabiliserIsSubgroup action)) {stab g gx=x} {stab h hx=x} g=h = g=h
+
+    orbitStabiliserEquivRel1 : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Rel A
+    orbitStabiliserEquivRel1 {T = T} action x g1 g2 = Setoid._∼_ T (GroupAction.action action g1 x) (GroupAction.action action g2 x)
+
+    orbitStabiliserEquivRel2 : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Rel A
+    orbitStabiliserEquivRel2 {T = T} {_+_ = _+_} {G = G} action x g1 g2 = Setoid._∼_ T (GroupAction.action action ((Group.inverse G g2) + g1) x) x
+
+    osEquivRel1Equiv : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Equivalence (orbitStabiliserEquivRel1 action x)
+    Reflexive.reflexive (Equivalence.reflexiveEq (osEquivRel1Equiv {T = T} action x)) {a} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+    Symmetric.symmetric (Equivalence.symmetricEq (osEquivRel1Equiv {T = T} action x)) {a} {b} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq T))
+    Transitive.transitive (Equivalence.transitiveEq (osEquivRel1Equiv {T = T} action x)) {a} {b} {c} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq T))
+
+    osEquivRel2Equiv : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Equivalence (orbitStabiliserEquivRel2 action x)
+    Reflexive.reflexive (Equivalence.reflexiveEq (osEquivRel2Equiv {T = T} {G = G} action x)) = transitive (GroupAction.actionWellDefined1 action (Group.invLeft G)) (GroupAction.identityAction action)
+      where
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+    Symmetric.symmetric (Equivalence.symmetricEq (osEquivRel2Equiv {S = S} {T = T} {_+_ = _+_} {G = G} gAction x)) {b} {c} b=c = need
+      where
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq S)) renaming (symmetric to symmetricS)
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq S)) renaming (transitive to transitiveS)
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq S)) renaming (reflexive to reflexiveS)
+        open Setoid T
+        open GroupAction gAction
+        open Group G
+        have : action ((inverse c) + b) x ∼ x
+        have = b=c
+        p : action (inverse (inverse b + c)) x ∼ x
+        p = transitive (actionWellDefined1 (transitiveS (invContravariant G) (Group.wellDefined G reflexiveS (invInv G)))) have
+        q : action ((inverse b) + c) (action (inverse (inverse b + c)) x) ∼ action ((inverse b) + c) x
+        q = actionWellDefined2 p
+        r : action (((inverse b) + c) + (inverse (inverse b + c))) x ∼ action ((inverse b) + c) x
+        r = transitive associativeAction q
+        s : action identity x ∼ action ((inverse b) + c) x
+        s = transitive (actionWellDefined1 (symmetricS invRight)) r
+        need : action ((inverse b) + c) x ∼ x
+        need = symmetric (transitive (symmetric identityAction) s)
+    Transitive.transitive (Equivalence.transitiveEq (osEquivRel2Equiv {S = S} {T = T} {_+_ = _+_} {G = G} gAction x)) {a} {b} {c} a=b b=c = need
+      where
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq S)) renaming (symmetric to symmetricS)
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq S)) renaming (transitive to transitiveS)
+        open Reflexive (Equivalence.reflexiveEq (Setoid.eq S)) renaming (reflexive to reflexiveS)
+        open Setoid T
+        open GroupAction gAction
+        open Group G
+        have1 : action ((inverse c) + b) x ∼ x
+        have1 = b=c
+        have2 : action ((inverse b) + a) x ∼ x
+        have2 = a=b
+        p : action ((inverse c) + b) (action (inverse b + a) x) ∼ x
+        p = transitive (actionWellDefined2 have2) have1
+        q : action ((inverse c + b) + (inverse b + a)) x ∼ x
+        q = transitive associativeAction p
+        need : action ((inverse c) + a) x ∼ x
+        need = transitive (actionWellDefined1 (transitiveS (wellDefined reflexiveS (transitiveS (symmetricS multIdentLeft) (wellDefined (symmetricS invRight) reflexiveS))) (fourWayAssoc G))) q
+
+    osEquivRelsEqual' : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) {g h : A} → (orbitStabiliserEquivRel2 action x) g h → (orbitStabiliserEquivRel1 action x) g h
+    osEquivRelsEqual' {S = S} {T = T} {_+_ = _+_} {G = G} action x {g} {h} g=h = need
+      where
+        open Setoid T
+        open Group G
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq S)) renaming (symmetric to symmetricS)
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        have : (GroupAction.action action ((inverse h) + g) x) ∼ x
+        have = g=h
+        p : (GroupAction.action action (inverse h) (GroupAction.action action g x)) ∼ x
+        p = transitive (symmetric (GroupAction.associativeAction action)) have
+        q : (GroupAction.action action h (GroupAction.action action (inverse h) (GroupAction.action action g x))) ∼ GroupAction.action action h x
+        q = GroupAction.actionWellDefined2 action p
+        r : (GroupAction.action action (h + inverse h) (GroupAction.action action g x)) ∼ GroupAction.action action h x
+        r = transitive (GroupAction.associativeAction action) q
+        s : (GroupAction.action action identity (GroupAction.action action g x)) ∼ GroupAction.action action h x
+        s = transitive (GroupAction.actionWellDefined1 action (symmetricS (Group.invRight G))) r
+        need : (GroupAction.action action g x) ∼ (GroupAction.action action h x)
+        need = transitive (symmetric (GroupAction.identityAction action)) s
+
+    osEquivRelsEqual : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) {g h : A} → (orbitStabiliserEquivRel1 action x) g h → (orbitStabiliserEquivRel2 action x) g h
+    osEquivRelsEqual {T = T} {_+_ = _+_} {G = G} action x {g} {h} g=h = need
+      where
+        open Setoid T
+        open Group G
+        open Symmetric (Equivalence.symmetricEq (Setoid.eq T))
+        open Transitive (Equivalence.transitiveEq (Setoid.eq T))
+        have : (GroupAction.action action g x) ∼ (GroupAction.action action h x)
+        have = g=h
+        p : GroupAction.action action (inverse h) (GroupAction.action action g x) ∼ GroupAction.action action (inverse h) (GroupAction.action action h x)
+        p = GroupAction.actionWellDefined2 action have
+        need : (GroupAction.action action ((inverse h) + g) x) ∼ x
+        need = transitive (GroupAction.associativeAction action) (transitive p (transitive (symmetric (GroupAction.associativeAction action)) (transitive (GroupAction.actionWellDefined1 action (Group.invLeft G)) (GroupAction.identityAction action))))
+
+    data Orbit {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) : Set (a ⊔ b ⊔ c ⊔ d) where
+      orbitElt : (g : A) → Orbit action x
+
+    orbitSetoid : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → Setoid (Orbit action x)
+    Setoid._∼_ (orbitSetoid {T = T} action x) (orbitElt a) (orbitElt b) = Setoid._∼_ T (GroupAction.action action a x) (GroupAction.action action b x)
+    Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (orbitSetoid {T = T} action x))) {orbitElt g} = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq T))
+    Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (orbitSetoid {T = T} action x))) {orbitElt g} {orbitElt h} = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq T))
+    Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (orbitSetoid {T = T} action x))) {orbitElt g} {orbitElt h} {orbitElt i} = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq T))
+
+    orbitStabiliserBijection : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → A → ((Stabiliser action x) && Orbit action x)
+    orbitStabiliserBijection action x g = stab {!g!} {!!} ,, orbitElt g
+
+    osBijWellDefined : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → {r s : A} → (Setoid._∼_ S r s) → Setoid._∼_ (directSumSetoid (stabiliserSetoid action x) (orbitSetoid action x)) (orbitStabiliserBijection action x r) (orbitStabiliserBijection action x s)
+    _&&_.fst (osBijWellDefined action x r~s) = {!!}
+    _&&_.snd (osBijWellDefined action x r~s) = GroupAction.actionWellDefined1 action r~s
+
+    orbitStabiliserTheorem : {a b c d : _} {A : Set a} {B : Set b} {S : Setoid {a} {c} A} {T : Setoid {b} {d} B} {_+_ : A → A → A} {G : Group S _+_} (action : GroupAction G T) (x : B) → SetoidBijection S (directSumSetoid (stabiliserSetoid action x) (orbitSetoid action x)) (orbitStabiliserBijection action x)
+    SetoidInjection.wellDefined (SetoidBijection.inj (orbitStabiliserTheorem {S = S} action x)) = osBijWellDefined action x
+    SetoidInjection.injective (SetoidBijection.inj (orbitStabiliserTheorem {S = S} action x)) {g} {h} (fst ,, gx=hx) = {!!}
+    SetoidSurjection.wellDefined (SetoidBijection.surj (orbitStabiliserTheorem action x)) = osBijWellDefined action x
+    SetoidSurjection.surjective (SetoidBijection.surj (orbitStabiliserTheorem action x)) {stab g gx=x ,, orbitElt h} = h , ({!!} ,, {!!})
diff --git a/Groups/Groups.agda b/Groups/Groups.agda
index c28ea6f..5e19ef9 100644
--- a/Groups/Groups.agda
+++ b/Groups/Groups.agda
@@ -58,14 +58,6 @@ module Groups.Groups where
       m : y ∼ z · e
       m = transitive l (wellDefined ~refl invRight)
 
-    identityIsUnique : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → (e : A) → ((b : A) → (Setoid._∼_ S (b · e) b)) → (Setoid._∼_ S e (Group.identity G))
-    identityIsUnique {S = S} {_·_} g thing fb = transitive (symmetric multIdentLeft) (fb e)
-      where
-        open Group g renaming (inverse to _^-1) renaming (identity to e)
-        open Setoid S
-        open Transitive (Equivalence.transitiveEq eq)
-        open Symmetric (Equivalence.symmetricEq eq)
-
     replaceGroupOp : {l m : _} {A : Set l} {S : Setoid {l} {m} A} {_·_ : A → A → A} → (G : Group S _·_) → {a b c d w x y z : A} → (Setoid._∼_ S a c) → (Setoid._∼_ S b d) → (Setoid._∼_ S w y) → (Setoid._∼_ S x z) → Setoid._∼_ S (a · b) (w · x) → Setoid._∼_ S (c · d) (y · z)
     replaceGroupOp {S = S} {_·_} G a~c b~d w~y x~z pr = transitive (symmetric (wellDefined a~c b~d)) (transitive pr (wellDefined w~y x~z))
       where
diff --git a/Groups/GroupsLemmas.agda b/Groups/GroupsLemmas.agda
index 224913c..4b236c9 100644
--- a/Groups/GroupsLemmas.agda
+++ b/Groups/GroupsLemmas.agda
@@ -33,3 +33,11 @@ module Groups.GroupsLemmas where
       open Equivalence eq
       open Symmetric symmetricEq
       open Transitive transitiveEq
+
+  identityIsUnique : {a b : _} → {A : Set a} → {S : Setoid {a} {b} A} → {_·_ : A → A → A} → (G : Group S _·_) → (e : A) → ((b : A) → (Setoid._∼_ S (b · e) b)) → (Setoid._∼_ S e (Group.identity G))
+  identityIsUnique {S = S} {_·_} g thing fb = transitive (symmetric multIdentLeft) (fb e)
+    where
+      open Group g renaming (inverse to _^-1) renaming (identity to e)
+      open Setoid S
+      open Transitive (Equivalence.transitiveEq eq)
+      open Symmetric (Equivalence.symmetricEq eq)
diff --git a/Groups/SymmetryGroups.agda b/Groups/SymmetryGroups.agda
index 2560637..dd31d6a 100644
--- a/Groups/SymmetryGroups.agda
+++ b/Groups/SymmetryGroups.agda
@@ -8,7 +8,6 @@ open import Numbers.Naturals
 open import Sets.FinSet
 open import Groups.Groups
 open import Groups.GroupDefinition
-open import Groups.GroupActions
 
 module Groups.SymmetryGroups where
   data SymmetryGroupElements {a b : _} {A : Set a} (S : Setoid {a} {b} A) : Set (a ⊔ b) where
@@ -67,24 +66,3 @@ module Groups.SymmetryGroups where
   Group.multIdentLeft (symmetricGroup A) {sym {f} bijF} = ExtensionallyEqual.eq λ {x} → Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq A))
   Group.invLeft (symmetricGroup S) {x} = symmetricGroupInvIsLeft S {x}
   Group.invRight (symmetricGroup S) {x} = symmetricGroupInvIsRight S {x}
-
-  actionInducesHom : {a b c d : _} {A : Set a} {S : Setoid {a} {c} A} {_+_ : A → A → A} {G : Group S _+_} {B : Set b} {X : Setoid {b} {d} B} → (GroupAction G X) → A → SymmetryGroupElements X
-  actionInducesHom {S = S} {_+_ = _+_} {G = G} {X = X} action f = sym {f = GroupAction.action action f} bij
-    where
-      bij : SetoidBijection X X (GroupAction.action action f)
-      SetoidInjection.wellDefined (SetoidBijection.inj bij) = GroupAction.actionWellDefined2 action
-      SetoidInjection.injective (SetoidBijection.inj bij) {x} {y} fx=fy = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) {x} {GroupAction.action action ((Group.inverse G f) + f) x} (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq X)) (GroupAction.identityAction action)) (GroupAction.actionWellDefined1 action (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) (Group.invLeft G)))) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) {_} {GroupAction.action action (Group.inverse G f + f) y} (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (GroupAction.associativeAction action) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (GroupAction.actionWellDefined2 action fx=fy) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq X)) (GroupAction.associativeAction action)))) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (GroupAction.actionWellDefined1 action (Group.invLeft G)) (GroupAction.identityAction action)))
-      SetoidSurjection.wellDefined (SetoidBijection.surj bij) = GroupAction.actionWellDefined2 action
-      SetoidSurjection.surjective (SetoidBijection.surj bij) {x} = GroupAction.action action (Group.inverse G f) x , Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq X)) (GroupAction.associativeAction action)) (Transitive.transitive (Equivalence.transitiveEq (Setoid.eq X)) (GroupAction.actionWellDefined1 action (Group.invRight G)) (GroupAction.identityAction action))
-
-  actionInducesHomIsHom : {a b c d : _} {A : Set a} {S : Setoid {a} {c} A} {_+_ : A → A → A} {G : Group S _+_} {B : Set b} {X : Setoid {b} {d} B} → (action : GroupAction G X) → GroupHom G (symmetricGroup X) (actionInducesHom action)
-  GroupHom.groupHom (actionInducesHomIsHom {X = X} action) {s1} {s2} = eq associativeAction
-    where
-      open Setoid X renaming (eq to setoidEq)
-      open Transitive (Equivalence.transitiveEq (Setoid.eq X))
-      open Reflexive (Equivalence.reflexiveEq (Setoid.eq X))
-      open Symmetric (Equivalence.symmetricEq (Setoid.eq X))
-      open GroupAction action
-  GroupHom.wellDefined (actionInducesHomIsHom action) {s1} {s2} s1=s2 = eq (actionWellDefined1 s1=s2)
-    where
-      open GroupAction action
diff --git a/Setoids/Lists.agda b/Setoids/Lists.agda
new file mode 100644
index 0000000..50ef785
--- /dev/null
+++ b/Setoids/Lists.agda
@@ -0,0 +1,59 @@
+{-# OPTIONS --safe --warning=error #-}
+
+open import LogicalFormulae
+open import Numbers.Naturals
+open import Lists
+open import Setoids.Setoids
+open import Functions
+
+module Setoids.Lists where
+  listEquality : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Rel {a} {b} (List A)
+  listEquality S [] [] = True'
+  listEquality S [] (x :: w2) = False'
+  listEquality S (x :: w1) [] = False'
+  listEquality S (x :: w1) (y :: w2) = (Setoid._∼_ S x y) && listEquality S w1 w2
+
+  listEqualityReflexive : {a b : _} {A : Set a} (S : Setoid {a} {b} A) (w : List A) → listEquality S w w
+  listEqualityReflexive S [] = record {}
+  listEqualityReflexive S (x :: w) = Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq S)) ,, listEqualityReflexive S w
+
+  listEqualitySymmetric : {a b : _} {A : Set a} (S : Setoid {a} {b} A) {w1 w2 : List A} → listEquality S w1 w2 → listEquality S w2 w1
+  listEqualitySymmetric S {w1 = []} {[]} pr = record {}
+  listEqualitySymmetric S {[]} {x :: xs} ()
+  listEqualitySymmetric S {x :: xs} {[]} ()
+  listEqualitySymmetric S {w1 = x :: w1} {y :: w2} (pr1 ,, pr2) = Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq S)) pr1 ,, listEqualitySymmetric S pr2
+
+  listEqualityTransitive : {a b : _} {A : Set a} (S : Setoid {a} {b} A) {w1 w2 w3 : List A} → listEquality S w1 w2 → listEquality S w2 w3 → listEquality S w1 w3
+  listEqualityTransitive S {w1 = []} {[]} {[]} w1=w2 w2=w3 = record {}
+  listEqualityTransitive S {w1 = []} {[]} {x :: xs} w1=w2 ()
+  listEqualityTransitive S {w1 = []} {x :: xs} {w3} () w2=w3
+  listEqualityTransitive S {w1 = x :: w1} {[]} {w3} () w2=w3
+  listEqualityTransitive S {w1 = x :: w1} {y :: ys} {[]} w1=w2 ()
+  listEqualityTransitive S {w1 = x :: w1} {y :: w2} {z :: w3} (pr1 ,, pr2) (pr3 ,, pr4) = Transitive.transitive (Equivalence.transitiveEq (Setoid.eq S)) pr1 pr3 ,, listEqualityTransitive S pr2 pr4
+
+  listEqualityRespectsMap : {a b c d : _} {A : Set a} {B : Set b} (S : Setoid {a} {c} A) (T : Setoid {b} {d} B) (f : A → B) (fWD : {x y : A} → Setoid._∼_ S x y → Setoid._∼_ T (f x) (f y)) → {w1 w2 : List A} (w1=w2 : listEquality S w1 w2) → listEquality T (listMap f w1) (listMap f w2)
+  listEqualityRespectsMap S T f fWD {[]} {[]} w1=w2 = record {}
+  listEqualityRespectsMap S T f fWD {[]} {x :: w2} ()
+  listEqualityRespectsMap S T f fWD {x :: w1} {[]} ()
+  listEqualityRespectsMap S T f fWD {x :: w1} {y :: w2} (x=y ,, w1=w2) = fWD x=y ,, listEqualityRespectsMap S T f fWD {w1} {w2} w1=w2
+
+  listSetoid : {a b : _} {A : Set a} (S : Setoid {a} {b} A) → Setoid (List A)
+  Setoid._∼_ (listSetoid S) word1 word2 = listEquality S word1 word2
+  Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (listSetoid S))) {word} = listEqualityReflexive S word
+  Symmetric.symmetric (Equivalence.symmetricEq (Setoid.eq (listSetoid S))) pr = listEqualitySymmetric S pr
+  Transitive.transitive (Equivalence.transitiveEq (Setoid.eq (listSetoid S))) pr1 pr2 = listEqualityTransitive S pr1 pr2
+
+  consWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} (xs : List A) {x y : A} (x=y : Setoid._∼_ S x y) → Setoid._∼_ (listSetoid S) (x :: xs) (y :: xs)
+  consWellDefined {S = S} xs x=y = x=y ,, Reflexive.reflexive (Equivalence.reflexiveEq (Setoid.eq (listSetoid S)))
+
+  appendWellDefined : {a b : _} {A : Set a} {S : Setoid {a} {b} A} {xs ys as bs : List A} (xs=as : Setoid._∼_ (listSetoid S) xs as) → (ys=bs : Setoid._∼_ (listSetoid S) ys bs) → Setoid._∼_ (listSetoid S) (xs ++ ys) (as ++ bs)
+  appendWellDefined {S = S} {[]} {[]} {[]} {[]} record {} record {} = record {}
+  appendWellDefined {S = S} {[]} {[]} {[]} {x :: bs} record {} ()
+  appendWellDefined {S = S} {[]} {x :: ys} {[]} {[]} record {} ys=bs = ys=bs
+  appendWellDefined {S = S} {[]} {x :: ys} {[]} {x₁ :: bs} record {} ys=bs = ys=bs
+  appendWellDefined {S = S} {[]} {ys} {x :: as} {bs} () ys=bs
+  appendWellDefined {S = S} {x :: xs} {ys} {[]} {bs} () ys=bs
+  appendWellDefined {S = S} {x :: xs} {[]} {x₁ :: as} {[]} xs=as record {} = _&&_.fst xs=as ,, identityOfIndiscernablesRight (xs ++ []) (as) (as ++ []) (listEquality S) (identityOfIndiscernablesLeft xs as (xs ++ []) (listEquality S) (_&&_.snd xs=as) (equalityCommutative (appendEmptyList xs))) (equalityCommutative (appendEmptyList as))
+  appendWellDefined {S = S} {x :: xs} {[]} {x₁ :: as} {x₂ :: bs} xs=as ()
+  appendWellDefined {S = S} {x :: xs} {x₂ :: ys} {x₁ :: as} {[]} xs=as ()
+  appendWellDefined {S = S} {x :: xs} {x₂ :: ys} {x₁ :: as} {x₃ :: bs} (fst ,, snd) ys=bs = fst ,, appendWellDefined snd ys=bs