--- a/Symmetric.agda	Thu Aug 20 18:32:54 2020 +0900
+++ b/Symmetric.agda	Thu Aug 20 19:20:56 2020 +0900
@@ -142,57 +142,29 @@
 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) 
-   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)  ))
+pconcat {0} {m} p q = q
+pconcat {suc n} {m} p q = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+   p→ : Fin (suc n + m) → Fin (suc n + m) 
+   p→ x = p00  x n {!!} where
+      p00 : {i : ℕ} (x : Fin i ) ( y : ℕ ) → y < suc n → Fin (suc n + m )
+      p00 zero zero y<sn = n→m+n (p  ⟨$⟩ˡ (fromℕ≤ {!!} ))
+      p00 zero (suc y) y<sn = n→m+n (p  ⟨$⟩ˡ (fromℕ≤ {!!} ))
+      p00 (suc x) zero y<sn = m→m+n (q  ⟨$⟩ˡ x)
+      p00 (suc x)(suc y) y<sn = {!!}
 
-   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)) )
-
-   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)
+   p← : Fin (suc n + m) → Fin (suc n + m) 
+   p← 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
+   piso← : (x : Fin (suc n + m) ) → p→ ( p← x ) ≡ x
+   piso← x = {!!}
 
-   -- 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 = 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→ : (x : Fin (suc n + m) ) → p← ( p→ x ) ≡ x
    piso→ = {!!}