--- a/Symmetric.agda	Mon Aug 17 18:58:20 2020 +0900
+++ b/Symmetric.agda	Tue Aug 18 11:37:36 2020 +0900
@@ -10,8 +10,12 @@
 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)
-open import Relation.Binary.PropositionalEquality
+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 )
+open import nat
 
 f1 : Fin 3 → Fin 3
 f1 zero = suc (suc zero)
@@ -27,6 +31,14 @@
    lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1
    lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x }
 
+finpid : (n i : ℕ ) → i Data.Nat.< 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
+
 fid : {p : ℕ } → Fin p → Fin p
 fid x = x
 
@@ -83,4 +95,20 @@
            j ⟨$⟩ˡ q
            ∎ where open ≡-Reasoning
 
+perm0 : Permutation zero zero
+perm0 = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
 
+open import Relation.Nullary
+open import Data.Empty
+
+flist>0  : ( n : ℕ ) → n Data.Nat.> 0  → length (fpid n) ≡ n
+flist>0 (suc n) _ = fn (suc n) n a<sa  where
+   fn : (n i : ℕ ) → (i<n : i Data.Nat.< n ) → (length (finpid n i i<n)) ≡ suc i
+   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 = {!!}
+