--- a/Symmetric.agda	Thu Aug 20 12:17:08 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 14:13:08 2020 +0900
@@ -4,7 +4,7 @@
 open import Algebra
 open import Algebra.Structures
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ )
-open import Data.Fin.Properties hiding ( <-cmp ; <-trans ; ≤-trans )
+open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
 open import Data.Product
 open import Data.Fin.Permutation
 open import Function hiding (id ; flip)
@@ -80,6 +80,8 @@
 
 -- An inductive construction of permutation
 
+-- we already have refl and trans
+
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
 pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
    p→ : Fin (suc n) → Fin (suc n)
@@ -120,6 +122,56 @@
    piso→ (suc zero) = refl
    piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 
 
+Finnm : {n m : ℕ } → Fin (n + m) ≡ Fin (m + n)
+Finnm {n} {m} =  cong (λ k → Fin k ) (+-comm n _ )
+
+Finnmconv : {n m : ℕ } → Fin (m + n) →  Fin (n + m)
+Finnmconv {n} {m} x = subst (λ k → Fin k ) (+-comm m _) x
+
+m+n→n : {n m : ℕ } → (x : Fin (n + m)) → toℕ x < n  →  Fin n
+m+n→n x x<n = fromℕ≤ x<n
+
+n→m+n : {n m : ℕ } → (x : Fin n) →  Fin (n + m)
+n→m+n {n} {m} x = Finnmconv {n} {m} (raise m x ) 
+
+m+n→m : {n m : ℕ } → (x : Fin (n + m)) → n ≤ toℕ x  →  Fin m
+m+n→m x n<x = reduce≥ x n<x
+
+m→m+n : {n m : ℕ } → (x : Fin m) →  Fin (n + m)
+m→m+n {zero} {m} x = x
+m→m+n {suc n} {m} x = suc (m→m+n x)
+
+lem0 : {n : ℕ } → n ≤ n
+lem0 {zero} = z≤n
+lem0 {suc n} = s≤s lem0
+
+lem00 : {n m : ℕ } → n ≡ m → n ≤ m
+lem00 refl = lem0
+
+pconcat  : {n m : ℕ }  → Permutation n n → Permutation m m → Permutation (n + m) (n + m)
+pconcat {n} {m} p q = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+   p→ : Fin (n + m) → Fin (n + m) 
+   p→ x with <-cmp (toℕ x ) n
+   p→ x | tri< a ¬b ¬c = n→m+n (p  ⟨$⟩ˡ (m+n→n  x a ))
+   p→ x | tri≈ ¬a b ¬c = m→m+n (q  ⟨$⟩ˡ (m+n→m x (lem00 (sym b)) ) )
+   p→ x | tri> ¬a ¬b c = m→m+n (q  ⟨$⟩ˡ (m+n→m x (≤to< c)  ))
+
+   p← : Fin (n + m) → Fin (n + m) 
+   p← x with <-cmp (toℕ x ) n
+   p← x | tri< a ¬b ¬c = n→m+n (p  ⟨$⟩ʳ (m+n→n  x a ))
+   p← x | tri≈ ¬a b ¬c = m→m+n (q  ⟨$⟩ʳ (m+n→m x (lem00 (sym b)))) 
+   p← x | tri> ¬a ¬b c = m→m+n (q  ⟨$⟩ʳ (m+n→m x (≤to< c)) )
+   
+   piso← : (x : Fin (n + m) ) → p→ ( p← x ) ≡ x
+   piso← x with <-cmp (toℕ x ) n
+   piso← x | tri< a ¬b ¬c = ?
+   piso← x | tri≈ ¬a b ¬c = ?
+   piso← x | tri> ¬a ¬b c = ?
+
+   piso→ : (x : Fin (n + m) ) → p← ( p→ x ) ≡ x
+   piso→ = {!!}
+
+
 -- enumeration
 
 psawpn : {n m : ℕ} → suc m < n → Permutation n n
@@ -132,13 +184,13 @@
    pfill1 0 _ perm = perm
    pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
 
-eperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
-eperm {zero} ()
-eperm {n} {0} (s≤s z≤n) perm = pprep perm
+eperm  : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
+eperm {0} {0} z≤n perm = pid
+eperm {suc n} {0} z≤n perm = pprep perm
 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where
     lemm3 : 2 + m ≤ suc n
-    lemm3 = ≤-trans (s≤s m<n) refl-≤s
-    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n)
+    lemm3 = s≤s (s≤s m<n)
+    eperm1 : (m i : ℕ ) → i + m ≤ suc n  → Permutation i i → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
     eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw )  -- i + zero ≤ suc (suc n) → i ≤ suc (suc n)
     eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where
        lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
@@ -149,15 +201,6 @@
           suc n
         ∎   where open  ≤-Reasoning
 
-
-finpid : (n i : ℕ ) → i < n → List (Fin n)
-finpid (suc n) zero _ = fromℕ≤ {zero} (s≤s z≤n) ∷ []
-finpid (suc n) (suc i) (s≤s lt) = fromℕ≤ (s≤s lt) ∷ finpid (suc n) i (<-trans lt a<sa) 
-
-fpid : (n : ℕ ) → List (Fin n)
-fpid 0 = []
-fpid (suc j) = finpid (suc j) j a<sa where
-
 plist  : {n  : ℕ} → Permutation n n → List ℕ
 plist {0} perm = []
 plist {suc j} perm = plist1 j a<sa where
@@ -166,12 +209,16 @@
     plist1  zero _           = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
     plist1  (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt)))         ∷ plist1  i (<-trans lt a<sa) 
 
+test0 = plist (eperm {1} {0} z≤n pid)
+test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
-test10 = plist (eperm {2} {0} ( s≤s z≤n)  pid)
-test11 = plist (eperm {2} {0} ( s≤s z≤n)  (eperm {1} {0} (s≤s z≤n) pid))
-test20 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) pid)
-test21 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) (eperm {1} {0} (s≤s z≤n) pid))
-test3 =  test10  ∷ test11 ∷ test20 ∷ test21 ∷ []
+test11 = plist (eperm {2} {0} z≤n             (eperm {1} {0}  z≤n pid))
+test12 = plist (eperm {2} {0} z≤n             (eperm {1} {1}  (s≤s z≤n)  pid))
+test21 = plist (eperm {2} {1} (s≤s z≤n)       (eperm {1} {0}  z≤n pid))
+test22 = plist (eperm {2} {1} (s≤s z≤n)       (eperm {1} {1}  (s≤s z≤n)  pid))
+test23 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {0}  z≤n  pid))
+test24 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {1}  (s≤s z≤n)  pid))
+test3 =  test11  ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
 
 NL : (n : ℕ ) → Set
 NL 0 = ℕ
@@ -179,9 +226,6 @@
 
 pls : (n : ℕ ) → List (List ℕ )
 pls n = Data.List.map plist (pls6 n) where
-   lem0 : {n : ℕ } → n ≤ n
-   lem0 {zero} = z≤n
-   lem0 {suc n} = s≤s lem0
    lem1 : {i n : ℕ } → i ≤ n → i < suc n
    lem1 z≤n = s≤s z≤n
    lem1 (s≤s lt) = s≤s (lem1 lt)
@@ -189,7 +233,7 @@
    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 = pid ∷ x
-   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} i≤n perm ∷ x)
+   pls4 (suc i) n i≤n  perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} (≤-trans refl-≤s i≤n ) perm ∷ 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)