--- a/Symmetric.agda	Wed Aug 19 08:50:17 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 09:14:29 2020 +0900
@@ -15,30 +15,9 @@
 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 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 < 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
+open import logic
 
 fid : {p : ℕ } → Fin p → Fin p
 fid x = x
@@ -104,19 +83,6 @@
 open import  Relation.Binary.Core
 open import fin
 
-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 < 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 ))
-
-record Pincl (i j : ℕ ) (p→i : Fin (suc (suc j)) → Fin (suc (suc j))) : Set (Level.suc Level.zero ) where
-   field
-     p←i     : (x : Fin (suc (suc j)) )    → (i≤x : toℕ x < i )       → Fin (suc (suc j))
-     piso←i  : ( x : Fin (suc (suc j)) )   → (i≤x : toℕ (p→i x) < i ) → p←i (p→i x) i≤x   ≡ x
-     piso→i  : ( x : Fin (suc (suc j)) )   → (i≤x : toℕ x < i )       → p→i ( p←i x i≤x ) ≡ x
-      
-
 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
@@ -128,24 +94,15 @@
    p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
    p→ x | tri> ¬a ¬b c =  fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s  )))
 
-   pincl : Pincl (suc (suc n)) n p→ 
-   pincl = pincl1 (suc (suc n)) where
-     pincl1 : (i : ℕ ) → Pincl i n p→ 
-     pincl1 0  = record { p←i = λ x () ; piso←i = λ x () ; piso→i = λ x () }
-     pincl1 (suc i) = pincl2 (fromℕ≤ a<sa ) where
-         pincl2 : (y : Fin (suc (suc n))) → Pincl (suc i) n p→
-         pincl2 zero = {!!}
-         pincl2 (suc y) = {!!}
-         
-     -- with pincl1 i 
-     -- ... | p = record { p←i = λ x i<x → p1 x i<x  ; piso←i = λ x i<x →  {!!} ; piso→i = λ x i<x → {!!} } where
-     --     j = n
-     --     p1 :  (x : Fin (suc (suc j)) )    → (i≤x : toℕ x < suc i )       → Fin (suc (suc j))
-     --     p1 x i≤x = {!!}
+   pincl :  (Fin (suc (suc n)) → Fin (suc (suc n)))
+       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p←i (p→ x)   ≡ x )
+       ∧ (( p←i : Fin (suc (suc n)) → Fin (suc (suc n))) →  (x : Fin (suc (suc n)) ) → p→ (p←i x)   ≡ x )
+   pincl = {!!}
 
+   open _∧_
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x = Pincl.p←i pincl x fin<n
+   p← = proj1 pincl
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
-   piso← x = Pincl.piso←i pincl  x fin<n
+   piso← = proj1 (proj2 pincl) p←
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
-   piso→ x = Pincl.piso→i pincl x fin<n
+   piso→ = proj2 (proj2 pincl) p←