--- a/Symmetric.agda	Fri Aug 21 13:13:27 2020 +0900
+++ b/Symmetric.agda	Fri Aug 21 19:24:56 2020 +0900
@@ -154,13 +154,14 @@
 -- inductivley enmumerate permutations
 --    from n-1 length create n length inserting new element at position m
 
-eperm  : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
-eperm {0} {0} z≤n perm = pprep perm
-eperm {suc n} {0} z≤n perm = pprep perm
-eperm {n} {suc m} (s≤s m<n) perm = eperm1 (suc m) (≤-trans (s≤s (s≤s m<n)) lem0 ) where
-    eperm1 : (i : ℕ ) → suc i ≤ suc n  → Permutation (suc n)(suc n) 
-    eperm1 zero (s≤s z≤n) = pprep perm
-    eperm1 (suc i) (s≤s si≤n) = eperm1 i (≤-trans si≤n refl-≤s )  ∘ₚ psawpim {suc n} {i}  (s≤s si≤n)
+eperm  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
+eperm {_} {zero} _ = pid
+eperm {suc _} {suc zero} _ = pswap pid
+eperm {suc (suc n)} {suc m} (s≤s m<n) =  eperm1 (suc m) (suc (suc n)) lem0 where
+    eperm1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
+    eperm1 _ zero _ = pid
+    eperm1 zero _ _ = pid
+    eperm1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  eperm1 i j (≤-trans si≤n refl-≤s ) 
 
 
 plist  : {n  : ℕ} → Permutation n n → List ℕ
@@ -177,13 +178,30 @@
 testi03 = plist ((psawpim (n≤  4 {0}) ∘ₚ psawpim  (n≤ 3) ) ∘ₚ psawpim {4} {0}  (n≤ 2 ))      -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []
 ttt0 =  testi0 ∷ testi01 ∷ testi02 ∷ testi03 ∷ []
 
-et0 = eperm {4} {4} (n≤ 4 ) (pid {4}) -- (4 ∷ 0 ∷ 1 ∷ 2 ∷ 3 ∷ [])
-et1 = eperm {4} {3} (n≤ 3 ) (pid {4}) -- (0 ∷ 4 ∷ 1 ∷ 2 ∷ 3 ∷ [])
-et2 = eperm (n≤ 2 ) (pid {4}) -- (0 ∷ 1 ∷ 4 ∷ 2 ∷ 3 ∷ [])
-et3 = eperm (n≤ 1 ) (pid {4}) -- (0 ∷ 1 ∷ 2 ∷ 4 ∷ 3 ∷ [])
-et4 = eperm (n≤ 0 ) (pid {4}) -- (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
-et5 = eperm (n≤ 4 ) (eperm (n≤ 2) (pid {3})) -- (0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ [])
-ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷  plist et3 ∷ plist et5 ∷ [] 
+tt0 = plist (eperm {3} {0} (n≤ 0)) ∷ plist ( eperm {3} {1} (n≤ 1 )) ∷ plist ( eperm {3} {2} (n≤ 2 )) ∷ plist ( eperm {3} {3} (n≤ 3 )) ∷ [] 
+
+c0 = pid {2} -- pprep ( eperm {3} (n≤ 3) pid)
+-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
+ct0 = c0 ∘ₚ eperm {1} (n≤ 0 ) 
+ct1 = c0 ∘ₚ eperm {1} (n≤ 1 ) 
+ttt1 = plist ct0 ∷ plist ct1 ∷ [] 
+
+d0 = pid {3} -- pprep ( eperm {3} (n≤ 3) pid)
+-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
+dt0 = d0 ∘ₚ eperm {2} (n≤ 0 ) 
+dt1 = d0 ∘ₚ eperm {2} (n≤ 1 ) 
+dt2 = d0 ∘ₚ eperm {2} (n≤ 2 ) 
+ttt3 = plist dt0 ∷ plist dt1 ∷ plist dt2 ∷ [] 
+
+-- e0 = pid {4} -- eperm (n≤ 2) (eperm (n≤ 2) (eperm (n≤ 1) (pid {1})))
+e0 = pid {5} -- pprep ( eperm {3} (n≤ 3) pid)
+-- e0 =  pprep ( eperm {3} (n≤ 3) pid)
+et0 = e0 ∘ₚ eperm {4} {4} (n≤ 4 ) 
+et1 = e0 ∘ₚ eperm {4} {3} (n≤ 3 ) 
+et2 = e0 ∘ₚ eperm {4} (n≤ 2 ) 
+et3 = e0 ∘ₚ eperm {4} (n≤ 1 ) 
+et4 = e0 ∘ₚ eperm {4} (n≤ 0 ) 
+ttt2 = plist et0 ∷ plist et1 ∷ plist et2 ∷  plist et3 ∷ plist et4 ∷ [] 
 
 pls : (n : ℕ ) → List (List ℕ )
 pls n = Data.List.map plist (pls6 n) where
@@ -193,8 +211,8 @@
    lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
    lem2 i≤n = ≤-trans i≤n ( refl-≤s )
    pls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
-   pls4 zero n i≤n perm x = pprep perm ∷ x
-   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {suc i} i≤n perm ∷ x)
+   pls4 zero n i≤n perm x = (pprep perm ∘ₚ eperm i≤n ) ∷ x
+   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ eperm {n} {suc i} i≤n  ∷ x)
    pls5 :  ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n))  → List (Permutation (suc n) (suc n)) 
    pls5 n [] x = x
    pls5 n (h ∷ x) y = pls5  n x (pls4 n n lem0 h y)
@@ -202,4 +220,4 @@
    pls6 zero = pid ∷ []
    pls6 (suc n) =  pls5 (suc n) (pls6 n) []
    pls7 : List (List ℕ )
-   pls7 = Data.List.map plist (pls4 2 2 lem0 (eperm (n≤ 0 ) (pid {1})) (pls4 2 2 lem0 (eperm (n≤ 1 ) (pid {1})) [] ))
+   pls7 = Data.List.map plist (pls4 2 2 lem0 (eperm (n≤ 0 ) ) (pls4 2 2 lem0 (eperm (n≤ 1 ) ) [] ))