open import Level hiding ( suc ; zero )
open import Algebra
module Solvable {n m : Level} (G : Group n m ) where

open import Data.Unit
open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
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 ⊔ 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 ]  )
  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-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 
     dervied-length : ℕ
     end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε