--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sym4.agda	Fri Aug 28 11:05:45 2020 +0900
@@ -0,0 +1,70 @@
+open import Level hiding ( suc ; zero )
+open import Algebra
+module sym4 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 hiding (_∘ₚ_)
+
+infixr  200 _∘ₚ_
+_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
+
+sym4solvable : solvable (Symmetric 4)
+solvable.dervied-length sym4solvable = 3
+solvable.end sym4solvable x d = solved1 x {!!} where
+
+   open import Data.List using ( List ; [] ; _∷_ )
+
+   open Solvable (Symmetric 4)
+   -- open Group (Symmetric 2) using (_⁻¹)
+
+   p0 :  FL→perm ((# 0) :: ((# 0) :: ((# 0) :: ((# 0 ) :: f0)))) =p= pid
+   p0 = {!!} -- record { peq = p00 } where
+
+   open _=p=_
+
+   -- Klien
+   --
+   --  1                     (1,2),(3,4)           (1,3),(2,4)           (1,4),(2,3)
+   --  0 ∷ 1 ∷ 2 ∷ 3 ∷ [] ,  1 ∷ 0 ∷ 3 ∷ 2 ∷ [] ,  2 ∷ 3 ∷ 0 ∷ 1 ∷ [] ,  3 ∷ 2 ∷ 1 ∷ 0 ∷ [] ,  
+
+
+   data Klein : (x : Permutation 4 4 ) → Set where
+       kid : Klein pid
+       ka  : Klein (pswap (pswap pid))
+       kb  : Klein (pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) )
+       kc  : Klein (pins (n≤ 3)  ∘ₚ  pins (n≤ 2) ∘ₚ pswap (pid {2}))
+
+   a0 =  pid {4}
+   a1 =  pswap (pswap (pid {0}))
+   a2 =  pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) 
+   a3 =  pins (n≤ 3)  ∘ₚ  pins (n≤ 2) ∘ₚ pswap (pid {2})
+
+   --   1 0  
+   --   2 1 0 
+   --   3 2 1 0
+
+   k1 : { x :  Permutation 4 4 } → Klein x → List ℕ
+   k1 {x} kid = plist x
+   k1 {x} ka = plist x
+   k1 {x} kb = plist x
+   k1 {x} kc = plist x
+
+   k2 = k1 kid ∷ k1 ka ∷ k1 kb ∷ k1 kc ∷ []
+   k3 = plist  (a1  ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3)  ∷ plist (a2 ∘ₚ a1 ) ∷  []
+   
+   solved1 :  (x : Permutation 4 4) →  Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid
+   solved1 = {!!}