--- a/Symmetric.agda	Tue Aug 18 23:21:03 2020 +0900
+++ b/Symmetric.agda	Tue Aug 18 23:39:31 2020 +0900
@@ -31,7 +31,7 @@
    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 : (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) 
 
@@ -103,12 +103,15 @@
 open import  Relation.Binary.Core
 open import fin
 
-flist>0  : ( n : ℕ ) → n Data.Nat.> 0  → length (fpid n) ≡ n
+flist>0  : ( n : ℕ ) → n > 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 : (n i : ℕ ) → (i<n : i < 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 ))
 
+perm→all : { n : ℕ } → (perm : Permutation n n ) → (f : Fin n ) → ¬ ( ( g : Fin n) → ¬ (perm ⟨$⟩ʳ f ≡ g ))
+perm→all  = {!!}
+
 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
@@ -130,39 +133,6 @@
      lemma i refl x | tri≈ ¬a b ¬c = fromℕ≤ (s≤s (s≤s m<n))
      lemma i refl 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 refl ¬c = begin
-          p← ( fromℕ≤ a<sa )
-       ≡⟨ lem4 refl ⟩
-          fromℕ≤ (s≤s (s≤s m<n))
-       ≡⟨ {!!} ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            lem4 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {suc n} a<sa  → p← x ≡ fromℕ≤ (s≤s (s≤s m<n))
-            lem4 {x} refl with <-cmp (toℕ x) (suc n)
-            lem4  refl | tri< a ¬b ¬c = {!!}
-            lem4  refl | tri≈ ¬a b ¬c = refl
-            lem4  refl | tri> ¬a ¬b c = {!!}
-   piso← x | tri> ¬a ¬b c = {!!}
+   piso← x = {!!}
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ x = lemma2 (suc n) refl x where
-     lemma2 : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-     lemma2 i refl x with <-cmp (toℕ x)  i
-     lemma2 i refl x | tri< a ¬b ¬c = {!!}
-     lemma2 i refl x | tri≈ ¬a b ¬c = begin
-          p→ (fromℕ≤ (s≤s (s≤s m<n)))
-       ≡⟨ lem5 refl ⟩
-          fromℕ≤ a<sa
-       ≡⟨ {!!}  ⟩
-          x
-       ∎  where
-            open ≡-Reasoning
-            lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n))  → p→ x ≡ fromℕ≤ a<sa
-            lem5 refl with <-cmp (toℕ x) m
-            lem5 refl | tri< a ¬b ¬c = {!!}
-            lem5 refl | tri≈ ¬a refl ¬c = refl
-            lem5 refl | tri> ¬a ¬b c = {!!}
-     lemma2 i refl x | tri> ¬a ¬b c = {!!}
-
+   piso→ x = {!!}