--- a/PermGroup.agda	Sun Aug 16 16:03:23 2020 +0900
+++ b/PermGroup.agda	Sun Aug 16 19:50:43 2020 +0900
@@ -1,4 +1,4 @@
-module PermAbel where
+module PermGroup where
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -53,8 +53,8 @@
 ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y  → y =p= z →  x =p= z
 peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
 
-pgroup : ℕ → Group  Level.zero Level.zero
-pgroup p = record {
+Pgroup : ℕ → Group  Level.zero Level.zero
+Pgroup p = record {
       Carrier        = Permutation p p
     ; _≈_            = _=p=_
     ; _∙_            = _∘ₚ_
@@ -77,13 +77,10 @@
        passoc x y z = record { peq = λ q → refl }
        p-inv : {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
        p-inv {i} {j} i=j q = begin
-              i ⟨$⟩ˡ q
-           ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
-              i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q ))
-           ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
-              i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q ))
-           ≡⟨ inverseˡ i  ⟩
-              j ⟨$⟩ˡ q
+           i ⟨$⟩ˡ q                      ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j)  )  ⟩
+           i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k  →  i ⟨$⟩ˡ k) (sym (peq i=j _ ))  ⟩
+           i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i  ⟩
+           j ⟨$⟩ˡ q
            ∎ where open ≡-Reasoning
 
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Solvable.agda	Sun Aug 16 19:50:43 2020 +0900
@@ -0,0 +1,27 @@
+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 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
+  uni  : Commutator P ε
+  gen  : (f g h : Carrier) → P g → P h  → Commutator P f → Commutator P ( f ∙ [ g , h ]  )
+
+deriving : ( i : ℕ ) → Carrier → Set (Level.suc n)
+deriving 0 x = Lift (Level.suc n) ⊤
+deriving (suc i) x = Commutator (deriving i) x 
+
+record Solvable : Set (Level.suc n ⊔ m) where
+  field 
+     dervied-length : ℕ
+     end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε