--- a/Symmetric.agda	Tue Aug 18 23:21:03 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 11:28:10 2020 +0900
@@ -14,31 +14,8 @@
 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)
-f1 (suc zero) = zero
-f1 (suc (suc zero)) = suc zero
-
-lemma1  : Permutation 3 3
-lemma1  = permutation f1 ( f1 ∘ f1 ) lemma2 where
-   lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x
-   lemma3 zero = refl
-   lemma3 (suc zero) = refl
-   lemma3 (suc (suc zero)) = refl
-   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
 
@@ -103,12 +80,6 @@
 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
-   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 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
@@ -132,6 +103,7 @@
    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 = {!!}
    piso← x | tri≈ ¬a refl ¬c = begin
           p← ( fromℕ≤ a<sa )
        ≡⟨ lem4 refl ⟩
@@ -145,12 +117,12 @@
             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 : 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 = {!!}
      lemma2 i refl x | tri≈ ¬a b ¬c = begin
           p→ (fromℕ≤ (s≤s (s≤s m<n)))
        ≡⟨ lem5 refl ⟩
@@ -162,7 +134,6 @@
             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 refl ¬c = {!!}
             lem5 refl | tri> ¬a ¬b c = {!!}
-     lemma2 i refl x | tri> ¬a ¬b c = {!!}