# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598671638 -32400
# Node ID 4efab088abd069a1978583f07a9f207780e96fbc
# Parent  4cae99fadd61ee78e0e50e03d287fcd814d6574f
...

diff -r 4cae99fadd61 -r 4efab088abd0 Putil.agda
--- a/Putil.agda	Sat Aug 29 12:06:57 2020 +0900
+++ b/Putil.agda	Sat Aug 29 12:27:18 2020 +0900
@@ -124,21 +124,21 @@
 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ []    plist ( pins {3} (n≤ 1) )     1 ∷ 0 ∷ 2 ∷ 3 ∷ []
 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ []    plist ( pins {3} (n≤ 2) )     2 ∷ 0 ∷ 1 ∷ 3 ∷ []
 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ []    plist ( pins {3} (n≤ 3) )     3 ∷ 0 ∷ 1 ∷ 2 ∷ []
-pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
-pins {_} {zero} _ = pid
-pins {suc _} {suc zero} _ = pswap pid
-pins {suc (suc n)} {suc m} (s≤s m<n) =  pins1 (suc m) (suc (suc n)) lem0 where
-    pins1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
-    pins1 _ zero _ = pid
-    pins1 zero _ _ = pid
-    pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n a≤sa ) 
+-- pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
+-- pins {_} {zero} _ = pid
+-- pins {suc _} {suc zero} _ = pswap pid
+-- pins {suc (suc n)} {suc m} (s≤s m<n) =  pins1 (suc m) (suc (suc n)) lem0 where
+--     pins1 : (i j : ℕ ) → j ≤ suc (suc n)  → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
+--     pins1 _ zero _ = pid
+--     pins1 zero _ _ = pid
+--     pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j}  (s≤s (s≤s si≤n))  ∘ₚ  pins1 i j (≤-trans si≤n a≤sa ) 
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 open ≡-Reasoning
 
-pins'  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
-pins' {_} {zero} _ = pid
-pins' {suc n} {suc m} (s≤s  m≤n) = permutation p← p→  record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
+pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
+pins {_} {zero} _ = pid
+pins {suc n} {suc m} (s≤s  m≤n) = permutation p← p→  record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
 
    next : Fin (suc (suc n)) → Fin (suc (suc n))
    next zero = suc zero
@@ -174,10 +174,13 @@
    piso→ zero with <-cmp (toℕ (fromℕ< (≤-trans (s≤s z≤n) (s≤s (s≤s  m≤n) )))) (suc m)
    ... | tri< a ¬b ¬c = refl
    piso→ (suc x) with <-cmp (toℕ (suc x)) (suc m)
-   ... | tri≈ ¬a b ¬c = p13 {!!} refl where
-       p13 : (y : Fin (suc (suc n)) ) → y ≡ {!!} → p← y ≡ suc x
-       p13 = {!!}
-   ... | tri> ¬a ¬b c = {!!} 
+   ... | tri≈ ¬a refl ¬c = p13 where
+       p13 : fromℕ< (s≤s (s≤s m≤n)) ≡ suc x
+       p13 = cong (λ k → suc k ) (fromℕ<-toℕ _ (s≤s m≤n) )
+   ... | tri> ¬a ¬b c = p16 (suc x) where
+       p16 : (x :  Fin (suc (suc n))) → p← x ≡ x
+       p16 zero = {!!}
+       p16 (suc x) = {!!}
    ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))) refl  where
        p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) ))  → p← y ≡ suc x
        p10 zero ()
@@ -239,8 +242,8 @@
              suc x
           ∎ 
 
-t7 =  plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷  plist ( pins' {3} (n≤ 3)  ∘ₚ  flip ( pins' {3} (n≤ 3))) ∷ []
-t8 =  {!!}
+t7 =  plist (pins {3} (n≤ 3)) ∷ plist (flip ( pins {3} (n≤ 3) )) ∷  plist ( pins {3} (n≤ 3)  ∘ₚ  flip ( pins {3} (n≤ 3))) ∷ []
+-- t8 =  {!!}
 
 
 plist2 : {n  : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ