--- a/Solvable.agda	Sun Aug 16 19:50:43 2020 +0900
+++ b/Solvable.agda	Sun Aug 16 22:08:46 2020 +0900
@@ -7,19 +7,36 @@
 open import Data.Nat using (ℕ; suc; zero)
 open import Relation.Nullary
 open import Data.Empty
+open import Data.Product
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
 
 open Group G
 
 [_,_] :  Carrier   → Carrier   → Carrier  
 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
 
-data Commutator (P : Carrier → Set (Level.suc n)) : (f : Carrier) → Set (Level.suc n) where
+data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
   uni  : Commutator P ε
-  gen  : (f g h : Carrier) → P g → P h  → Commutator P f → Commutator P ( f ∙ [ g , h ]  )
+  gen  : {f g h : Carrier} → P g → P h  → Commutator P f → Commutator P ( f ∙ [ g , h ]  )
+  ccong  : {f g  : Carrier} → f ≈ g → Commutator P f → Commutator P g
+
+deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
+deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
+deriving (suc i) x = Commutator (deriving i) x 
+
+-- deriving stage is closed on multiplication and inversion
 
-deriving : ( i : ℕ ) → Carrier → Set (Level.suc n)
-deriving 0 x = Lift (Level.suc n) ⊤
-deriving (suc i) x = Commutator (deriving i) x 
+deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y  → deriving i ( x ∙ y )
+deriving-mul {zero} {x} {y} (lift tt) (lift tt) = lift tt
+deriving-mul {suc i} {ε} {ε} uni uni = ccong (Algebra.Group.sym G (proj₁ identity ε)) uni 
+deriving-mul {suc i} {ε} {_} uni (gen x x₁ iy) = ccong (Algebra.Group.sym G (proj₁ identity _)) (gen x x₁ iy)
+deriving-mul {suc i} {_} {ε} (gen x x₁ ix) uni = ccong (Algebra.Group.sym G (proj₂ identity _)) (gen x x₁ ix)
+deriving-mul {suc i} {_} {_} (gen x x₁ ix) (gen x₂ x₃ iy) = ccong {!!} (gen x₂ x₃ (gen x x₁ iy))
+deriving-mul {suc i} {_} {_} _ _ = {!!}
+
+deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
+deriving-inv {i} {x} ix = ?
 
 record Solvable : Set (Level.suc n ⊔ m) where
   field