--- a/Symmetric.agda	Tue Aug 18 11:37:36 2020 +0900
+++ b/Symmetric.agda	Tue Aug 18 15:58:15 2020 +0900
@@ -3,15 +3,15 @@
 open import Level hiding ( suc ; zero )
 open import Algebra
 open import Algebra.Structures
-open import Data.Fin
+open import Data.Fin hiding ( _<_  )
 open import Data.Product
 open import Data.Fin.Permutation
 open import Function hiding (id ; flip)
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
 open import Function.LeftInverse  using ( _LeftInverseOf_ )
 open import Function.Equality using (Π)
-open import Data.Nat using (ℕ; suc; zero; s≤s ; z≤n )
-open import Data.Nat.Properties using (<-trans)
+open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
+open import Data.Nat.Properties -- using (<-trans)
 open import Relation.Binary.PropositionalEquality 
 open import Data.List using (List; []; _∷_ ; length)
 open import Data.List.Relation.Binary.Permutation.Inductive renaming ( refl to irefl ; trans to itrans )
@@ -100,6 +100,8 @@
 
 open import Relation.Nullary
 open import Data.Empty
+open import  Relation.Binary.Core
+open import fin
 
 flist>0  : ( n : ℕ ) → n Data.Nat.> 0  → length (fpid n) ≡ n
 flist>0 (suc n) _ = fn (suc n) n a<sa  where
@@ -107,8 +109,30 @@
    fn (suc n) zero _ = refl
    fn (suc n) (suc i) (s≤s i<n) = cong (λ k → suc k ) (fn (suc n) i (<-trans i<n a<sa ))
 
-fperm  : {n : ℕ} → { x : List (Fin n) } → x ↭ fpid n → Permutation n n
-fperm {zero} {[]} _ = perm0
-fperm {suc n} {[]} y = {!!}
-fperm {suc n} {x ∷ x₁} y = {!!}
+fperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
+fperm {zero} ()
+fperm {suc n} {m} (s≤s m<n) perm = permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
+   p→ : Fin (suc (suc n)) → Fin (suc (suc n))
+   p→ x with <-cmp (toℕ x) m
+   p→ x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn))  where
+       x<sn : toℕ x < suc n
+       x<sn = <-trans a (s≤s m<n)
+   p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
+   p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
+   p← : Fin (suc (suc n)) → Fin (suc (suc n))
+   p← x with <-cmp (toℕ x) (suc (suc n))
+   p← x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
+       x<sn : toℕ x < suc n
+       x<sn = <-trans a ?
+   p← x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
+   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-<> c fin<n )
+   piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
+   piso← x with <-cmp (toℕ x) m
+   piso← x | tri< a ¬b ¬c = {!!}
+   piso← x | tri≈ ¬a b ¬c = {!!} where
+       lem4 : toℕ (fromℕ≤ (s≤s a<sa)) ≡ m → fromℕ≤ {!!} ≡ x 
+       lem4 = {!!}
+   piso← x | tri> ¬a ¬b c = {!!}
+   piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
+   piso→ = {!!}