--- a/Putil.agda	Tue Sep 01 19:03:21 2020 +0900
+++ b/Putil.agda	Tue Sep 01 20:00:24 2020 +0900
@@ -28,15 +28,6 @@
 
 -- An inductive construction of permutation
 
--- Todo
---
---   describe property of pins    ( move 0 to any position)
---   describe property of shrink  ( remove one column )
---   prove FL→iso 
---   prove FL←iso 
-
--- we already have refl and trans in the Symmetric Group
-
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
 pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
    p→ : Fin (suc n) → Fin (suc n)
@@ -499,7 +490,6 @@
        ≡⟨ plem2 plem3 ⟩
           x
        ∎ where
-          open ≡-Reasoning
           plem2 :  suc t1 ≡ suc x → t1 ≡ x
           plem2 refl = refl
           plem3 :  suc t1 ≡ suc x
@@ -519,9 +509,17 @@
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
    → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
 shrink-iso2 {n} {perm} p=0 = record { peq =  s001 } where
-    s001 : (q : Fin (suc n)) → (pprep (shrink perm p=0) ⟨$⟩ʳ q) ≡ (perm ⟨$⟩ʳ q)
-    s001 zero = {!!}
-    s001 (suc q) = {!!}
+    s001 : (q : Fin (suc n)) → (pprep (shrink perm p=0) ⟨$⟩ʳ q) ≡ perm ⟨$⟩ʳ q
+    s001 zero = begin
+         zero
+       ≡⟨ sym ( inverseʳ perm ) ⟩
+         perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero )
+       ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) p=0 ⟩
+         perm ⟨$⟩ʳ zero
+       ∎ 
+    s001 (suc q) with perm ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ perm ) (suc q) 
+    ... | zero | record {eq = e}  = ⊥-elim (sh1 perm p=0 {q} e)
+    ... | suc t | e = refl
 
 
 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}
@@ -594,10 +592,6 @@
  
 t6 = perm→FL t4
 
-----
---  if n is fixed, perm→FL ( FL→perm fl ) ≡ fl is refl for each concrete fl
---  so we may prove this easily by co-induction
---
 FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 FL→iso f0 = refl
 FL→iso {suc n} (x :: fl) = cong₂ ( λ j k → j :: k ) f001 f002 where
@@ -650,7 +644,9 @@
         (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q
      ≡⟨  peq (presp (pprep-cong (FL←iso _ ) ) prefl ) q  ⟩
          (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
-     ≡⟨ {!!}  ⟩
+     ≡⟨  peq (passoc _ _ _  ) q ⟩
+         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))) ⟨$⟩ʳ ((  pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q )
+     ≡⟨ peq (shrink-iso2 (p=0 perm)) ((pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q) ⟩
          ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
      ≡⟨ peq (passoc _ _ _ ) q ⟩
          (perm ∘ₚ (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )))  ⟨$⟩ʳ q