--- a/src/Gutil0.agda	Sat Sep 02 12:06:39 2023 +0900
+++ b/src/Gutil0.agda	Sat Sep 02 14:44:32 2023 +0900
@@ -62,6 +62,7 @@
        P : Carrier  → Set (Level.suc c ⊔ d) 
        Pε : P ε
        P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
+       P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
        P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
        -- gN ≈ Ng
        Pcomm : {a b : Carrier  }  → P a  →  P ( b ∙  ( a  ∙ b ⁻¹ ) )

--- a/src/Solvable.agda	Sat Sep 02 12:06:39 2023 +0900
+++ b/src/Solvable.agda	Sat Sep 02 14:44:32 2023 +0900
@@ -135,27 +135,25 @@
     b ∙ ([ g , h ] ∙ b ⁻¹) ∎
 Pcomm {a} {b} (suc i) (ccong f=a pa) = ccong (∙-cong grefl (∙-cong f=a grefl)) (Pcomm {_} {b} (suc i) pa)
 
-comp : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i b → deriving i (a ∙ b)
-comp {a} {b} zero (lift tt) (lift tt) = lift tt
-comp  (suc i) (comm {a} {b} pa pb) (comm {c} {d} pc pd) = ccong cc1 ( comm (comp i pa pb) (comp i pc pd) ) where
-   cc1 : [ a ∙ b , c ∙ d ] ≈ [ a , b ] ∙ [ c , d ]
-   cc1 = begin
-     [ a ∙ b , c ∙ d ] ≈⟨ grefl ⟩
-     (a ∙ b) ⁻¹ ∙ (c ∙ d) ⁻¹ ∙ (a ∙ b) ∙ (c ∙ d) ≈⟨ ∙-cong (∙-cong (∙-cong (sym (lemma5 _ _)) (sym (lemma5 _ _)) ) grefl) grefl ⟩
-     (b ⁻¹ ∙ a ⁻¹) ∙ (d ⁻¹ ∙ c ⁻¹) ∙ (a ∙ b) ∙ (c ∙ d) ≈⟨ ? ⟩
-     (a ⁻¹ ∙ b ⁻¹ ∙ (b  ∙ a )) ∙ ((b ⁻¹ ∙ a ⁻¹) ∙ (d ⁻¹ ∙ c ⁻¹) ∙ (a ∙ b) ∙ (c ∙ d)) ≈⟨ ? ⟩
-     a ⁻¹ ∙ b ⁻¹ ∙ a ∙ b ∙ (c ⁻¹ ∙ d ⁻¹ ∙ c ∙ d ) ≈⟨ grefl ⟩
-     [ a , b ] ∙ [ c , d ] ∎
-comp (suc i) (comm a pa) (ccong g=b pb) = ccong (∙-cong grefl g=b ) (comp (suc i)  (comm a pa) pb  )
-comp {a}  (suc i) (ccong f=a pa) (comm b pb) = ccong (∙-cong f=a grefl ) (comp (suc i)  pa (comm b pb) )
-comp {a} {b} (suc i) (ccong f=a pa) (ccong g=b pb) = ccong (∙-cong f=a g=b) (comp (suc i)  pa pb )
+-- a proudct of commutators may not be a commutator
+-- so we have to use finite products of commutators
+
+data iCommutator (i : ℕ) : (j : ℕ) → Carrier → Set (Level.suc n ⊔ m) where
+  iunit : (a : Carrier) → deriving i a  →  iCommutator i zero a
+  icom : (j : ℕ) → {a b : Carrier} → deriving i a → iCommutator i j b → iCommutator i (suc j) (a ∙ b)
+
+record IC (i : ℕ ) (ica : Carrier) : Set (Level.suc n ⊔ m) where
+  field 
+     icn : ℕ
+     icc : iCommutator i icn ica
 
 CommGroup : (i : ℕ) → NormalSubGroup G 
 CommGroup i = record {
-     P = deriving i
-   ; Pε = deriving-ε
-   ; P⁻¹ =  λ a pa → deriving-inv pa
-   ; P∙ = comp i
+     P = IC i
+   ; Pε = record { icn = 0; icc = iunit ε ? }
+   ; P⁻¹ =  λ a pa → ?
+   ; P≈ = ?
+   ; P∙ = ?
    ; Pcomm = ?
  }