--- a/Symmetric.agda	Thu Aug 20 14:13:08 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 18:32:54 2020 +0900
@@ -122,17 +122,11 @@
    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 ) 
+n→m+n {n} {m} x = fromℕ≤ (≤-trans (fin<n {n} {x}) (x≤x+y {n} {m}) )
 
 m+n→m : {n m : ℕ } → (x : Fin (n + m)) → n ≤ toℕ x  →  Fin m
 m+n→m x n<x = reduce≥ x n<x
@@ -148,6 +142,12 @@
 lem00 : {n m : ℕ } → n ≡ m → n ≤ m
 lem00 refl = lem0
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
+lem01 : {n m : ℕ } → (x y : Fin n ) → {a : toℕ x < m } {b : toℕ y < m } → x ≡ y → a ≅ b
+lem01 zero zero refl = HE.refl
+lem01 (suc x) = {!!}
+
 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) 
@@ -161,12 +161,36 @@
    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)) )
-   
+
+   lem06 : {n m : ℕ } → (eq : n ≡ m ) → (x : Fin n)  → toℕ (raise m x) ≡ toℕ x
+   lem06 refl zero = {!!}
+   lem06 refl (suc x) = cong (λ k → suc k ) {!!} -- (lem06 refl x)
+
+   lem07 : {n m : ℕ } → (eq : n ≡ m ) → (x : Fin n)  → toℕ (cast eq x) ≡ toℕ x
+   lem07 refl zero = refl
+   lem07 refl (suc x) = cong (λ k → suc k ) (lem07 refl x)
+
+   lem05 : (x : Fin n ) →  toℕ (fromℕ≤ (≤-trans (fin<n {_} {x} ) (x≤x+y {n} {m})))  < n
+   lem05 x  = subst ( λ k → k < n ) (sym  (toℕ-fromℕ≤ _ )) fin<n
+
+   -- ff = fromℕ≤ (≤-trans (fin<n {_} {Inverse.from p Π.⟨$⟩ m+n→n x a} ) x≤x+y) 
    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 | tri< a ¬b ¬c = begin
+           p→ (fromℕ≤ (≤-trans (fin<n {_} {p  ⟨$⟩ʳ (m+n→n  x a)})  x≤x+y))
+        ≡⟨ {!!} ⟩
+           n→m+n (p  ⟨$⟩ˡ (m+n→n  (fromℕ≤ (≤-trans (fin<n {_} {Inverse.from p Π.⟨$⟩ m+n→n x a} ) x≤x+y) ) (lem05 _) ))
+        ≡⟨ {!!} ⟩
+           x 
+     ∎ where
+        open ≡-Reasoning 
+        lem8 : ( x : Fin (n + m)) → ( a : toℕ x < n ) → p→ x ≡ n→m+n (p  ⟨$⟩ˡ (m+n→n x a ))
+        lem8 x a with <-cmp (toℕ x ) n
+        lem8 x a | tri< a₁ ¬b ¬c = {!!}
+        lem8 x a | tri≈ ¬a b ¬c = {!!}
+        lem8 x a | 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→ = {!!}