# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597766446 -32400
# Node ID 270b28c9615488a3fb49bb208cb4c35d83e66cec
# Parent  65e6c97a03cd523bab0f0c3a0f8dbd9c131845c3
...

diff -r 65e6c97a03cd -r 270b28c96154 Symmetric.agda
--- a/Symmetric.agda	Tue Aug 18 23:39:31 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 01:00:46 2020 +0900
@@ -3,9 +3,10 @@
 open import Level hiding ( suc ; zero )
 open import Algebra
 open import Algebra.Structures
-open import Data.Fin hiding ( _<_  )
+open import Data.Fin hiding ( _<_  ; _≤_ )
 open import Data.Product
 open import Data.Fin.Permutation
+open import Data.Fin.Properties renaming ( <-cmp  to fcmp ; <-trans to ftrans )
 open import Function hiding (id ; flip)
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
 open import Function.LeftInverse  using ( _LeftInverseOf_ )
@@ -109,8 +110,12 @@
    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  = {!!}
+record Pincl (i j : ℕ ) (p→i : Fin j → Fin j) : Set (Level.suc Level.zero ) where
+   field
+     p←i     :  Fin j  → Fin j
+     piso←i  : ( x : Fin j ) → (i≤x : i ≤ toℕ x) → p←i ( p→i x) i≤x ≡ x
+     piso→i  : ( x : Fin j ) → (i≤x : i ≤ toℕ x) → p→i ( p←i i≤x x) ≡ x
+      
 
 fperm  : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
 fperm {zero} ()
@@ -123,15 +128,18 @@
    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)) (suc (suc n)) p→ 
+   pincl = pincl1 (suc n) ? ?  where
+     pincl1 : (i : ℕ ) → i < suc (suc n)  → Pincl i → Pincl (suc i)
+     pincl1 0 = ?
+
    p← : Fin (suc (suc n)) → Fin (suc (suc n))
-   p← x = lemma (suc n) refl x where
-     lemma : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → Fin (suc (suc n))
-     lemma i refl x with <-cmp (toℕ x) i
-     lemma i refl x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn))  where
-       x<sn : toℕ x < suc n
-       x<sn = a
-     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 )
+   p← x = find (fromℕ≤ a<sa) where
+       find : (y : Fin (suc (suc n))) → Fin (suc (suc n))
+       find y with fcmp x ( p→ y )
+       find y | tri< a ¬b ¬c = {!!}
+       find y | tri≈ ¬a b ¬c = y
+       find y | tri> ¬a ¬b c = {!!}
    piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
    piso← x = {!!}
    piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x