# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598661412 -32400
# Node ID 2e5d0b142ecaafa18549992b03d08dcc1a403e7b
# Parent  482ef04890f8336d0d7720a25fb4b793bcb0a88a
...

diff -r 482ef04890f8 -r 2e5d0b142eca Putil.agda
--- a/Putil.agda	Sat Aug 29 07:48:45 2020 +0900
+++ b/Putil.agda	Sat Aug 29 09:36:52 2020 +0900
@@ -169,6 +169,35 @@
           ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  a≤sa ) ) ⟩
             suc (toℕ x)
           ∎ 
+
+   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
+   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 = {!!}
+   ... | tri> ¬a ¬b c = {!!} 
+   ... | 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 ()
+       p10 (suc y) eq with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) ,  a : suc x < suc m
+       ... | tri< a₁ ¬b ¬c = p11 where
+           p12 : (toℕ (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) ≡ (toℕ x)
+           p12 = {!!}
+           p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
+           p11 = begin
+              fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
+             ≡⟨ {!!} ⟩
+              fromℕ< (≤-trans (fin<n {_} {suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))}) a≤sa )
+             ≡⟨ {!!} ⟩
+              fromℕ< (≤-trans (fin<n {_} {fromℕ< (≤-trans a (s≤s m≤n))}) a≤sa )
+             ≡⟨ fromℕ<-irrelevant _ _ (cong suc p12 ) (≤-trans (fin<n {_} {fromℕ< (≤-trans a (s≤s m≤n))}) a≤sa) (s≤s (fin<n {suc n}))  ⟩
+              suc (fromℕ< (fin<n {suc n} {x} )) 
+             ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
+              suc x
+             ∎
+       ... | tri≈ ¬a b ¬c = {!!}
+       ... | tri> ¬a ¬b c = {!!}
+
    piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
    piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm
    ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t )
@@ -204,10 +233,6 @@
              suc x
           ∎ 
 
-
-   piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
-   piso→ = {!!}
-
 t7 =  plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷  plist ( pins' {3} (n≤ 3)  ∘ₚ  flip ( pins' {3} (n≤ 3))) ∷ []
 t8 =  {!!}