# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695089498 -32400
# Node ID 8fb16f9a882aefe94064d86a300b15c2c9167980
# Parent  fff18d4a063b17033572b4e966790f59336524bb
...

diff -r fff18d4a063b -r 8fb16f9a882a Galois.agda-lib
--- a/Galois.agda-lib	Mon Sep 18 13:19:37 2023 +0900
+++ b/Galois.agda-lib	Tue Sep 19 11:11:38 2023 +0900
@@ -1,5 +1,5 @@
 name: Galois
-depend: standard-library-2.0
+depend: standard-library
 include: src 
 flags:
   --warning=noUnsupportedIndexedMatch
diff -r fff18d4a063b -r 8fb16f9a882a src/Putil.agda
--- a/src/Putil.agda	Mon Sep 18 13:19:37 2023 +0900
+++ b/src/Putil.agda	Tue Sep 19 11:11:38 2023 +0900
@@ -5,7 +5,7 @@
 open import Algebra
 open import Algebra.Structures
 open import Data.Fin hiding ( _<_  ; _≤_ ; _-_ ; _+_ ; _≟_)
-open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties as DFP 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_)
@@ -123,7 +123,7 @@
 --     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
+-- open ≡-Reasoning
 
 pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 pins {_} {zero} _ = pid
@@ -157,7 +157,7 @@
             toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa)))
           ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n  a≤sa ) ) ⟩
             suc (toℕ x)
-          ∎ 
+          ∎ where open ≡-Reasoning
 
    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)
@@ -190,18 +190,18 @@
                toℕ (fromℕ< (≤-trans a (s≤s m≤n)))
              ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩
                suc (toℕ x)
-             ∎
+              ∎ where open ≡-Reasoning
           p15 : p← (suc y) ≡ suc x
           p15 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
             p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x
             p11 = begin
                fromℕ< (≤-trans (fin<n {_} {y}) a≤sa )
-              ≡⟨ ? ⟩  -- lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
+              ≡⟨ lemma10 {suc (suc n)} {_} {_} p12 {≤-trans (fin<n {_} {y}) a≤sa} {s≤s (fin<n {suc n} {x} )}  ⟩
                suc (fromℕ< (fin<n {suc n} {x} )) 
               ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
                suc x
-              ∎
+              ∎ where open ≡-Reasoning
           ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a ))  --  suc x < suc m -> y = suc x  → toℕ y < suc m 
           ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a ))  
 
@@ -232,13 +232,13 @@
              fromℕ< (≤-trans (s≤s  a₁) (s≤s (s≤s  m≤n) ))
           ≡⟨⟩
              fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) 
-          ≡⟨ ? ⟩  -- lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
+          ≡⟨ lemma10 {suc (suc n)} (p3 x) {p6} {p2} ⟩
              fromℕ< ( s≤s (fin<n {suc n} {x}) )
           ≡⟨⟩
              suc (fromℕ< (fin<n {suc n} {x} )) 
           ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩
              suc x
-          ∎ 
+          ∎ where open ≡-Reasoning
 
 t7 =  plist (pins {3} (n≤ 3)) ∷ plist (flip ( pins {3} (n≤ 3) )) ∷  plist ( pins {3} (n≤ 3)  ∘ₚ  flip ( pins {3} (n≤ 3))) ∷ []
 -- t8 =  {!!}
@@ -278,13 +278,13 @@
           p004 = p003  (fromℕ< (s≤s (s≤s m≤n))) (
              begin
                 fromℕ< (s≤s (s≤s m≤n))
-             ≡⟨ ? ⟩ --  lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
+             ≡⟨ lemma10 {suc (suc n)}  (cong suc meq) {s≤s (s≤s m≤n)} {subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) } ⟩
                 fromℕ< (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) )
              ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k →  suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩
                 suc t
              ≡⟨ sym e ⟩
                 (perm ⟨$⟩ʳ (# 0))
-             ∎ )
+             ∎ )   where open ≡-Reasoning 
 
 ----
 --  other elements are preserved in pins
@@ -350,7 +350,7 @@
           y ⟨$⟩ʳ zero
        ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩
           y ⟨$⟩ʳ q
-       ∎ 
+       ∎ where open ≡-Reasoning 
   pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i)
   ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a
   ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i )
@@ -363,6 +363,7 @@
        ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩
             y ⟨$⟩ʳ q
        ∎ where
+          open ≡-Reasoning 
           pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn)
           pleq3 tq=si = toℕ-injective ( begin
                   toℕ  q
@@ -409,7 +410,8 @@
           suc ( y ⟨$⟩ʳ q )
         ≡⟨⟩
           pprep y ⟨$⟩ʳ suc q
-        ∎  
+        ∎  where
+          open ≡-Reasoning 
 
 pprep-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y)
 pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where
@@ -430,7 +432,8 @@
           suc (suc (y ⟨$⟩ʳ q))
         ≡⟨⟩
           pswap y ⟨$⟩ʳ suc (suc q)
-        ∎  
+        ∎  where
+          open ≡-Reasoning 
  
 pswap-dist : {n  : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y)
 pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where
@@ -446,7 +449,8 @@
           perm ⟨$⟩ʳ zero                     ≡⟨ cong (λ k →  perm ⟨$⟩ʳ k ) (sym p0=0) ⟩
           perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero)        ≡⟨ inverseʳ perm  ⟩
           zero
-       ∎ 
+       ∎ where
+          open ≡-Reasoning 
 
 shlem← : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero
 shlem← perm p0=0 x px=0 =  begin
@@ -454,7 +458,8 @@
           perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x )          ≡⟨ cong (λ k →  perm ⟨$⟩ˡ k ) px=0 ⟩
           perm ⟨$⟩ˡ zero                     ≡⟨ p0=0  ⟩
           zero
-       ∎ 
+       ∎ where
+          open ≡-Reasoning 
 
 sh2 : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero
 sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq
@@ -469,62 +474,85 @@
 shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
 shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where
 
+   p00 : (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ʳ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.to perm (suc x))) < n
+   p00 x c = sx≤py→x≤y ( begin
+     suc (suc (Data.Nat.pred (toℕ (Inverse.to perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
+     suc (toℕ (Inverse.to perm (suc x))) ≤⟨ fin<n ⟩
+     suc n ∎ ) where
+        open Data.Nat.Properties.≤-Reasoning
+
+   p01 : (x : Fin n) → (c :  0 < toℕ (perm ⟨$⟩ˡ (suc x) ) ) → Data.Nat.pred (toℕ (Inverse.from perm (suc x))) < n
+   p01 x c = sx≤py→x≤y ( begin
+     suc (suc (Data.Nat.pred (toℕ (Inverse.from perm (suc x))))) ≡⟨ cong suc (sucprd c) ⟩
+     suc (toℕ (Inverse.from perm (suc x))) ≤⟨ fin<n ⟩
+     suc n ∎ ) where
+        open Data.Nat.Properties.≤-Reasoning
+
    p→ : Fin n → Fin n 
-   p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) 
-   p→ x | zero  | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e )
-   p→ x | suc t | _ = t
+   p→ x with <-fcmp (perm ⟨$⟩ʳ (suc x) ) (# 0)
+   p→ x | tri≈ ¬a b ¬c = ⊥-elim (sh1 perm p0=0 b)
+   p→ x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.to perm (suc x)))} (p00 x c) 
 
    p← : Fin n → Fin n 
-   p← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) 
-   p← x | zero  | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e )
-   p← x | suc t | _ = t
+   p← x with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0)
+   p← x | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
+   p← x | tri> ¬a ¬b c = fromℕ< {Data.Nat.pred (toℕ (Inverse.from perm (suc x)))} (p01 x c)
 
+   --  using "with" something binded in ≡ is prohibited
    piso← : (x : Fin n ) → p→ ( p← x ) ≡ x
-   piso← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) 
-   piso← x | zero  | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e )
-   piso← x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t)
-   piso← x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh1 perm p0=0 e )
-   piso← x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
-          t1
-       ≡⟨ plem0 plem1 ⟩
-          x
-       ∎ where
-          open ≡-Reasoning
-          plem0 :  suc t1 ≡ suc x → t1 ≡ x
-          plem0 refl = refl
-          plem1 :  suc t1 ≡ suc x
-          plem1 = begin
-               suc t1
-            ≡⟨ sym e1 ⟩
-               Inverse.to perm  _
-            ≡⟨ cong (λ k →  Inverse.to perm k ) (sym e0) ⟩
-               Inverse.to perm ( Inverse.from perm _ )
-            ≡⟨ inverseʳ perm   ⟩
-               suc x
-            ∎ 
+   piso← x = p02 _ _ refl refl  where
+      p02 : (y z : Fin n) → p← x ≡ y → p→ y ≡ z → z ≡ x
+      p02 y z px=y py=z with <-fcmp (perm ⟨$⟩ˡ (suc x)) (# 0)
+      ... | tri≈ ¬a b ¬c = ⊥-elim (sh2 perm p0=0 b)
+      ... | tri> ¬a ¬b c with <-fcmp (perm ⟨$⟩ʳ (suc y)) (# 0)
+      ... | tri≈ ¬a₁ b ¬c = ⊥-elim (sh1 perm p0=0 b)
+      ... | tri> ¬a₁ ¬b₁ c₁ = ? where
+           open ≡-Reasoning 
+           p03 : toℕ (Inverse.to perm (suc x)) ≡ suc (toℕ y)
+           p03 = ?
 
+        -- with perm ⟨$⟩ˡ (suc x) in eq 
+        -- ... | t = ?
+--        ... | zero = ⊥-elim ( sh2 perm p0=0 {y} eq )
+--        ... | suc s with perm ⟨$⟩ˡ (suc x) in eq1
+--        ... | zero = ⊥-elim ( sh1 perm p0=0 eq1 )
+--        ... | suc t1 = begin
+--             ? ≡⟨ ? ⟩
+--             ? ∎  where
+--              open ≡-Reasoning
+--              plem0 :  suc t1 ≡ suc x → t1 ≡ x
+--              plem0 refl = refl
+--              plem1 :  suc t1 ≡ suc x
+--              plem1 = begin
+--                   suc t1                                  ≡⟨ sym eq1 ⟩
+--                   Inverse.to perm  _                      ≡⟨ cong (λ k →  Inverse.to perm k ) (sym ?) ⟩
+--                   Inverse.to perm ( Inverse.from perm _ ) ≡⟨ inverseʳ perm   ⟩
+--                   suc x
+--                ∎ 
+-- 
    piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x
-   piso→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x)
-   piso→ x | zero  | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e )
-   piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t)
-   piso→ x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh2 perm p0=0 e )
-   piso→ x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
-          t1
-       ≡⟨ plem2 plem3 ⟩
-          x
-       ∎ where
-          plem2 :  suc t1 ≡ suc x → t1 ≡ x
-          plem2 refl = refl
-          plem3 :  suc t1 ≡ suc x
-          plem3 = begin
-               suc t1 ≡⟨ sym e1 ⟩
-               Inverse.from perm (suc t)  ≡⟨ cong (λ k →  Inverse.from perm k ) (sym e0 ) ⟩
-               Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k →  Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩
-               Inverse.from perm ( Inverse.to perm  _ ) ≡⟨ inverseˡ perm   ⟩
-               suc x ∎
-
+   piso→ x = ?
+--   with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x)
+--   piso→ x | zero  | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e )
+--   piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t)
+--   piso→ x | suc t | _ | zero |  record { eq = e } =  ⊥-elim ( sh2 perm p0=0 e )
+--   piso→ x | suc t |  record { eq = e0 } | suc t1 |  record { eq = e1 } = begin
+--          t1
+--       ≡⟨ plem2 plem3 ⟩
+--          x
+--       ∎ where
+--          plem2 :  suc t1 ≡ suc x → t1 ≡ x
+--          plem2 refl = refl
+--          plem3 :  suc t1 ≡ suc x
+--          plem3 = begin
+--               suc t1 ≡⟨ sym e1 ⟩
+--               Inverse.from perm (suc t)  ≡⟨ cong (λ k →  Inverse.from perm k ) (sym e0 ) ⟩
+--               Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k →  Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩
+--               Inverse.from perm ( Inverse.to perm  _ ) ≡⟨ inverseˡ perm   ⟩
+--               suc x ∎
+-- 
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
-shrink-iso {n} {perm} = record { peq = λ q → refl  } 
+shrink-iso {n} {perm} = record { peq = λ q → ? } 
 
 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} 
    → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0)  → pprep (shrink perm p=0) =p= perm
@@ -536,10 +564,12 @@
          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
+       ∎ where
+          open ≡-Reasoning 
+    s001 = ?
+    -- 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)}
@@ -547,22 +577,23 @@
     → (x=0 :  x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 )  → shrink x x=0 =p=  shrink y y=0 
 shrink-cong {n} {x} {y} x=y x=0 y=0  = record  { peq = p002 } where
     p002 : (q : Fin n) → (shrink x x=0 ⟨$⟩ʳ q) ≡ (shrink y y=0 ⟨$⟩ʳ q)
-    p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q)
-    p002 q | zero   | record { eq = ex } | zero   | ey                  = ⊥-elim ( sh1 x x=0 ex )
-    p002 q | zero   | record { eq = ex } | suc py | ey                  = ⊥-elim ( sh1 x x=0 ex )
-    p002 q | suc px | ex                 | zero   | record { eq = ey }  = ⊥-elim ( sh1 y y=0 ey )
-    p002 q | suc px | record { eq = ex } | suc py | record { eq = ey }  = p003 ( begin
-           suc px
-         ≡⟨ sym ex ⟩
-           x ⟨$⟩ʳ (suc q)
-         ≡⟨ peq x=y (suc q) ⟩
-           y ⟨$⟩ʳ (suc q)
-         ≡⟨ ey ⟩
-           suc py
-         ∎ ) where
-        p003 : suc px ≡ suc py → px ≡ py
-        p003 refl = refl
-
+    p002 q = ?
+--    p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q)
+--    p002 q | zero   | record { eq = ex } | zero   | ey                  = ⊥-elim ( sh1 x x=0 ex )
+--    p002 q | zero   | record { eq = ex } | suc py | ey                  = ⊥-elim ( sh1 x x=0 ex )
+--    p002 q | suc px | ex                 | zero   | record { eq = ey }  = ⊥-elim ( sh1 y y=0 ey )
+--    p002 q | suc px | record { eq = ex } | suc py | record { eq = ey }  = p003 ( begin
+--           suc px
+--         ≡⟨ sym ex ⟩
+--           x ⟨$⟩ʳ (suc q)
+--         ≡⟨ peq x=y (suc q) ⟩
+--           y ⟨$⟩ʳ (suc q)
+--         ≡⟨ ey ⟩
+--           suc py
+--         ∎ ) where
+--        p003 : suc px ≡ suc py → px ≡ py
+--        p003 refl = refl
+-- 
 open import FLutil
 
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
@@ -643,7 +674,8 @@
        pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) 
      ≡⟨ px=x x ⟩
        x 
-     ∎
+     ∎ where
+          open ≡-Reasoning 
     x=0 :  (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0
     x=0 = subst ( λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ˡ (# 0) ≡ # 0 ) f001 (p=0 perm)
     x=0' : (pprep (FL→perm fl) ∘ₚ pid) ⟨$⟩ˡ (# 0) ≡ # 0
@@ -671,7 +703,8 @@
         perm→FL ( FL→perm fl ) 
      ≡⟨ FL→iso fl  ⟩
         fl 
-     ∎ 
+     ∎ where
+          open ≡-Reasoning 
 
 pcong-Fp : {n : ℕ }  → {x y : FL n}  → x ≡ y → FL→perm x =p= FL→perm y
 pcong-Fp {n} {x} {x} refl = prefl
@@ -691,6 +724,7 @@
      ≡⟨⟩
         perm ⟨$⟩ʳ q
      ∎  ) } 
+      where open ≡-Reasoning 
 
 FL-inject : {n : ℕ }  → {g h : Permutation n n }  → perm→FL g ≡  perm→FL h → g =p= h
 FL-inject {n} {g} {h} g=h = record { peq = λ q → ( begin
@@ -702,6 +736,7 @@
      ≡⟨ peq (FL←iso h) q ⟩
         h ⟨$⟩ʳ q
      ∎  ) }
+      where open ≡-Reasoning 
 
 FLpid :  {n : ℕ} → (x : Permutation n n) → perm→FL x ≡ FL0 → FL→perm FL0 =p= pid   → x =p= pid
 FLpid x eq p0id = ptrans pf2 (ptrans pf0 p0id ) where
@@ -712,4 +747,4 @@
 
 pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid
 pFL0 {zero} = refl
-pFL0 {suc n} = cong (λ k → zero :: k ) pFL0
+pFL0 {suc n} = cong (λ k → zero :: k ) ? -- pFL0
diff -r fff18d4a063b -r 8fb16f9a882a src/fin.agda
--- a/src/fin.agda	Mon Sep 18 13:19:37 2023 +0900
+++ b/src/fin.agda	Tue Sep 19 11:11:38 2023 +0900
@@ -104,6 +104,10 @@
 -- lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
 -- lemma10 {n} refl  = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl  ))
 
+lemma10 : {n i j  : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n }  → fromℕ< i<n ≡ fromℕ< j<n
+lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl
+lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n})
+
 -- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c
 -- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) 
 
@@ -134,7 +138,6 @@
 open import Data.List
 open import Relation.Binary.Definitions
 
-
 -----
 --
 -- find duplicate element in a List (Fin n)