--- a/Solvable.agda	Mon Aug 24 14:50:27 2020 +0900
+++ b/Solvable.agda	Mon Aug 24 18:55:37 2020 +0900
@@ -28,7 +28,7 @@
 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
 deriving (suc i) x = Commutator (deriving i) x 
 
-record Solvable : Set (Level.suc n ⊔ m) where
+record solvable : Set (Level.suc n ⊔ m) where
   field 
      dervied-length : ℕ
      end : (x : Carrier ) → deriving dervied-length x →  x ≈ ε  

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym5.agda	Mon Aug 24 18:55:37 2020 +0900
@@ -0,0 +1,89 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym5 where
+
+open import Symmetric 
+open import Data.Unit
+open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
+open import Function
+open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
+open import Relation.Nullary
+open import Data.Empty
+open import Data.Product
+
+open import Gutil 
+open import Putil 
+open import Solvable using (solvable)
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+open import Data.Fin
+open import Data.Fin.Permutation
+
+sym4solvable : solvable (Symmetric 2)
+solvable.dervied-length sym4solvable = 1
+solvable.end sym4solvable x d = solved x d where
+
+   open Solvable (Symmetric 2)
+   -- open Group (Symmetric 2) using (_⁻¹)
+
+   s2 :  ( g : Permutation 2 2 ) → g =p= pinv g 
+   s2 g = record { peq = λ q → s2lem q } where
+      s2lem : (q : Fin 2) → (g ⟨$⟩ʳ q) ≡ (pinv g ⟨$⟩ʳ q)
+      s2lem zero with g ⟨$⟩ʳ zero | inspect  (_⟨$⟩ʳ_ g ) zero
+      s2lem zero | zero | record { eq = e1 }  = begin
+             zero
+          ≡⟨ sym (inverseˡ g ) ⟩
+             g ⟨$⟩ˡ ( g ⟨$⟩ʳ zero )
+          ≡⟨ cong ( λ k →  g ⟨$⟩ˡ k ) e1 ⟩
+             g ⟨$⟩ˡ zero
+          ≡⟨⟩
+             pinv g ⟨$⟩ʳ zero
+          ∎ where open ≡-Reasoning
+      s2lem zero | suc zero | record { eq = e2 }  = begin
+             suc zero
+          ≡⟨ {!!} ⟩
+             g ⟨$⟩ʳ zero
+          ≡⟨ {!!} ⟩
+             g ⟨$⟩ˡ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ zero ))
+          ≡⟨ {!!} ⟩
+             g ⟨$⟩ˡ zero
+          ≡⟨⟩
+             pinv g ⟨$⟩ʳ zero
+          ∎ where open ≡-Reasoning
+      s2lem (suc zero) = {!!} 
+
+   sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
+   sym2lem0 g h q with perm→FL g | perm→FL h
+   sym2lem0 g h q | zero :: (zero :: f0) | zero :: (zero :: f0) = {!!}
+   sym2lem0 g h q | zero :: (zero :: f0) | suc zero :: (zero :: f0) = {!!}
+   sym2lem0 g h q | suc zero :: (zero :: f0) | zero :: (zero :: f0) = {!!}
+   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = {!!}
+   solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
+   solved x uni = prefl
+   solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  } 
+   solved x (gen {f} {g} d d₁) with solved f d | solved g d₁
+   ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where
+      genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q
+      genlem q = begin
+             g ⟨$⟩ʳ ( f ⟨$⟩ʳ q )
+          ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩
+             f ⟨$⟩ʳ q 
+          ≡⟨ f=e q ⟩
+             q
+          ∎ where open ≡-Reasoning
+   solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
+   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
+      cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
+      cc q = begin
+             x ⟨$⟩ʳ q
+          ≡⟨ sym (f=g q) ⟩
+             f ⟨$⟩ʳ q
+          ≡⟨ f=e q ⟩
+             q
+          ∎ where open ≡-Reasoning
+
+¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+¬sym5solvable sol = {!!}
+
+
+