--- a/Putil.agda	Fri Aug 28 13:33:35 2020 +0900
+++ b/Putil.agda	Fri Aug 28 22:20:39 2020 +0900
@@ -1,10 +1,11 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
 module Putil where
 
 open import Level hiding ( suc ; zero )
 open import Algebra
 open import Algebra.Structures
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ )
-open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant  ) renaming ( <-cmp to <-fcmp )
 open import Data.Fin.Permutation
 open import Function hiding (id ; flip)
 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
@@ -132,6 +133,8 @@
     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 refl-≤s ) 
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
 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
@@ -142,7 +145,7 @@
 
    p→ : Fin (suc (suc n)) → Fin (suc (suc n)) 
    p→ x with <-cmp (toℕ x) (suc m)
-   ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s  a) (≤-trans (s≤s (s≤s  m≤n) ) lem0 ))
+   ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s  a) (s≤s (s≤s  m≤n) )) 
    ... | tri≈ ¬a b ¬c = zero
    ... | tri> ¬a ¬b c = x
 
@@ -152,9 +155,49 @@
    ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s )
    ... | tri≈ ¬a b ¬c = suc x
    ... | tri> ¬a ¬b c = suc x
+
+   mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m 
+   mm = toℕ-fromℕ< (s≤s (s≤s  m≤n)) 
+
+   mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) ) ≤ m
+   mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n refl-≤s ) )) x<sm
    
    piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
-   piso← = {!!}
+   piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm
+   ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t )
+   ... | tri≈ ¬a b ¬c | t = refl
+   ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t )
+   piso← (suc x) with <-cmp (toℕ x) (suc m)
+   ... | tri≈ ¬a b ¬c = ?
+   ... | tri> ¬a ¬b c = {!!}
+   ... | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s ) )) (suc m)
+   ... | tri≈ ¬a b ¬c₁ = ⊥-elim ( ¬a (s≤s (mma x a)))
+   ... | tri> ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a)))
+   ... | tri< a₁ ¬b₁ ¬c₁ = p0 where
+       p2 : suc (suc (toℕ x)) ≤ suc (suc n)
+       p2 = s≤s (fin<n {suc n} {x})
+       p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s refl-≤s)))) ≤ suc (suc n)
+       p6 = s≤s (≤-trans a₁ (s≤s m≤n))
+
+       p3 :   toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s))) ≡ suc (toℕ x)
+       p3 = begin
+            toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s refl-≤s)))
+          ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  refl-≤s ) ) ⟩
+            suc (toℕ x)
+          ∎ where open ≡-Reasoning
+       p0 : fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))  ≡ suc x
+       p0 = begin
+             fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
+          ≡⟨⟩
+             fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
+          ≡⟨ lemma10 p3 {p6} {p2} ⟩
+             fromℕ< ( s≤s (fin<n {suc n} {x}) )
+          ≡⟨ lemma3 {toℕ x} {suc n} (fin<n {suc (n)} {x})  ⟩
+             suc (fromℕ< (fin<n {suc n} {x} )) 
+          ≡⟨ cong suc (fromℕ<-toℕ x (fin<n {suc n} {x}) ) ⟩
+             suc x
+          ∎ where open ≡-Reasoning
+
 
    piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
    piso→ = {!!}

--- a/sym2.agda	Fri Aug 28 13:33:35 2020 +0900
+++ b/sym2.agda	Fri Aug 28 22:20:39 2020 +0900
@@ -29,19 +29,13 @@
    -- open Group (Symmetric 2) using (_⁻¹)
 
    p0 :  FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid
-   p0 = record { peq = p00 } where
-      p00 : (q : Fin 2) → (FL→perm ((# 0) :: ((# 0) :: f0)) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-      p00 zero = refl
-      p00 (suc zero) = refl
+   p0 = pleq _ _ refl
 
-   p1 :  Permutation 2 2
-   p1 =  FL→perm ((# 1) :: ((# 0 ) :: f0)) 
+   p0r :  (p : Permutation 2 2 ) → perm→FL p ≡ ((# 0) :: ((# 0 ) :: f0)) → p =p= pid
+   p0r p eq = {!!}
 
-   p1rev : (p1  ∘ₚ  p1 ) =p= pid
-   p1rev = record { peq = p01 } where
-      p01 : (q : Fin 2) → ((p1 ∘ₚ p1) ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-      p01 zero = refl
-      p01 (suc zero) = refl
+   p1 :  FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid
+   p1 = pleq _ _ refl
 
    open _=p=_
    
@@ -62,6 +56,7 @@
           ∎ where
             open ≡-Reasoning
             sym2lem1 :  g =p= pid
+            sym2lem1 = pleq _ _ {!!}
             -- it works but very slow
             -- sym2lem1 = ptrans  (psym ( FL←iso g )) (subst (λ k → FL→perm k =p= pid) (sym g=00) p0 ) 
    sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} = begin