# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1597829000 -32400
# Node ID a986f22cde8421445e933760c54b6026287274c3
# Parent  5b299203acf0efc1cd23582c98b8dafcea74b053
...

diff -r 5b299203acf0 -r a986f22cde84 Symmetric.agda
--- a/Symmetric.agda	Wed Aug 19 16:37:59 2020 +0900
+++ b/Symmetric.agda	Wed Aug 19 18:23:20 2020 +0900
@@ -73,7 +73,7 @@
            j ⟨$⟩ˡ q
            ∎ where open ≡-Reasoning
 
-perm0 : Permutation zero zero
+perm0 : {n : ℕ } → Permutation n n 
 perm0 = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
 
 open import Relation.Nullary
@@ -81,6 +81,60 @@
 open import  Relation.Binary.Core
 open import fin
 
+fperm0  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
+fperm0 {n} perm =  permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = {!!} } where
+   p→ : Fin (suc n) → Fin (suc n)
+   p→ x with <-cmp (toℕ x) n
+   p→ x | tri< a ¬b ¬c = fin+1 ( perm  ⟨$⟩ˡ ( fromℕ≤ a ))
+   p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
+   p→ x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
+   
+   p← : Fin (suc n) → Fin (suc n)     
+   p← x with <-cmp (toℕ x) n
+   p← x | tri< a ¬b ¬c = fin+1 ( perm  ⟨$⟩ʳ ( fromℕ≤ a ))
+   p← x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
+   p← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
+
+   piso← : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
+   piso← x with <-cmp (toℕ x) n
+   piso← x | tri< a ¬b ¬c = begin  
+          p← ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ a)) ) 
+       ≡⟨ {!!}  ⟩
+          fin+1 ( perm  ⟨$⟩ʳ ( perm  ⟨$⟩ˡ  ( fromℕ≤ a )) )
+       ≡⟨ cong (λ k → fin+1 k ) ( inverseʳ perm )  ⟩
+          fin+1 (fromℕ≤ a) 
+       ≡⟨ {!!}  ⟩
+           x
+       ∎ where
+         open ≡-Reasoning
+   piso← x | tri≈ ¬a b ¬c = begin
+          p← ( fromℕ≤ a<sa )
+       ≡⟨ {!!}  ⟩
+           x
+       ∎ where open ≡-Reasoning
+   piso← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
+
+fswap  : {n m : ℕ } → suc m < n → Permutation n n 
+fswap {n} {m} n<m   = permutation p→ p→ record { left-inverse-of = piso← ; right-inverse-of =  piso←} where
+   p→ : Fin n → Fin (n)
+   p→ x with <-cmp (toℕ x) m
+   p→ x | tri< a ¬b ¬c = x
+   p→ x | tri≈ ¬a b ¬c = fromℕ≤ {suc m} {n} n<m
+   p→ x | tri> ¬a ¬b c with <-cmp (toℕ x) (suc m)
+   p→ x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = x
+   p→ x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = fromℕ≤ {m} {n} (<-trans a<sa n<m)
+   p→ x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = x
+   
+   piso← : (x : Fin (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 ¬b c with <-cmp (toℕ x) (suc m)
+   piso← x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = {!!}
+   piso← x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}
+   piso← x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!}
+
+
 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