# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1695476627 -32400
# Node ID e9de2bfef88d2fb1be76cfe70275a8edc6662486
# Parent  f5b2145c174cf0e4d847615631c7adccfe2ffb54
fix done

diff -r f5b2145c174c -r e9de2bfef88d src/FLComm.agda
--- a/src/FLComm.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/FLComm.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}   --  cannot use --cubical-compatible because of Solvable
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 module FLComm (n : ℕ) where
 
@@ -11,7 +11,7 @@
 open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev )
 open import Data.Product hiding (_,_ )
 open import Relation.Nullary 
-open import Data.Unit hiding (_≤_)
+open import Data.Unit -- hiding (_≤_)
 open import Data.Empty
 open import  Relation.Binary.Core 
 open import  Relation.Binary.Definitions hiding (Symmetric )
diff -r f5b2145c174c -r e9de2bfef88d src/Homomorphism.agda
--- a/src/Homomorphism.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/Homomorphism.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -358,7 +358,7 @@
                     ; ε-homo = ε-homo }
                    ; ⁻¹-homo = ⁻¹-homo  }
                ; injective = λ eq → AN.ab⁻¹∈N→a=b G (Ker G H f-homo) (h06 eq) }
-       ;  surjective = λ nx → (IsImage.gelm (Nelm.Pelm nx)) , h07 nx
+       ;  surjective = λ nx → (IsImage.gelm (Nelm.Pelm nx)) , h071 nx
    } where
     open GK G (Ker G H f-homo) 
     open Group H
@@ -367,8 +367,6 @@
     open EqReasoning (Algebra.Group.setoid H)
     open Nelm
     GC = Group.Carrier G 
-    h07 : (nx : Nelm H (Im G f-homo)) → f (IsImage.gelm (Nelm.Pelm nx)) ≈ elm nx
-    h07 nx = gsym ( IsImage.x=fg (Nelm.Pelm nx) )
     h06 : {x y : GC} → f x ≈ f y → f (G < x ∙ Group._⁻¹ G y >) ≈ ε 
     h06 {x} {y} fx=fy = begin
         f (G < x ∙ Group._⁻¹ G y >) ≈⟨ homo _ _  ⟩
@@ -393,6 +391,12 @@
            h (G < x ∙ (Group._⁻¹ G y ) > ) ∙ h y  ≈⟨ car kf ⟩ 
            ε ∙ h y  ≈⟨ proj₁ identity _ ⟩ 
            h y   ∎  
-
-
-
+    h07 : (nx : Nelm H (Im G f-homo)) → f (IsImage.gelm (Nelm.Pelm nx)) ≈ elm nx
+    h07 nx = gsym ( IsImage.x=fg (Nelm.Pelm nx) )
+    h071 : (nx : Nelm H (Im G f-homo)) → {z : Group.Carrier G} 
+       → (G / Ker G H f-homo) < z ≈  IsImage.gelm (Pelm nx) >
+       → f z ≈ elm nx
+    h071 nx {z} geq = begin
+        f z ≈⟨ h04 geq ⟩
+        f (IsImage.gelm (Pelm nx)) ≈⟨ gsym ( IsImage.x=fg (Nelm.Pelm nx) ) ⟩
+        elm nx ∎ 
diff -r f5b2145c174c -r e9de2bfef88d src/Putil.agda
--- a/src/Putil.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/Putil.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -295,22 +295,19 @@
     p003 : 0 < toℕ (Inverse.to perm zero)
     p003 = subst ( λ k → 0 < k ) (cong toℕ (sym eq)) (s≤s z≤n)
     p008 : toℕ (Data.Fin.pred (Inverse.to perm zero)) ≡ toℕ (Inverse.to perm zero) ∸ 1
-    p008 = ?
+    p008 = fpred-comm (Inverse.to perm zero)
     p002 : toℕ (Inverse.to perm zero) ≤ suc n
     p002 = toℕ≤pred[n] (Inverse.to perm zero)
-    p001 : suc (toℕ (Data.Fin.pred (Inverse.to perm zero))) ≤ suc n
-    p001 = begin
-        suc (toℕ (Data.Fin.pred (Inverse.to perm zero)))  ≡⟨ cong suc p008  ⟩
-        suc (Data.Nat.pred (toℕ (Inverse.to perm zero)))  ≡⟨ sucprd p003 ⟩
-        toℕ (Inverse.to perm zero)  ≤⟨ p002 ⟩
-        suc n  ∎ where open ≤-Reasoning
     p007 : Data.Nat.pred (toℕ (Inverse.to perm zero)) < suc n
-    p007 = subst (λ k → k < suc n ) p008 ?
+    p007 = subst (λ k → k < suc n ) p008 (<-transˡ (pred< _ (λ ne → DFP.<⇒≢ p003 (sym ne))) p002)
     p012 : Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡ # 0 
     p012 = begin
-        Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡⟨ cong (λ k → perm ∘ₚ flip (pins (toℕ≤pred[n] k)) ⟨$⟩ˡ # 0) (sym eq) ⟩ 
-        perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ # 0))) ⟨$⟩ˡ # 0 ≡⟨ p011 _ _ perm p001 (s≤s z≤n) ⟩
-        perm ⟨$⟩ˡ suc (fromℕ< p001) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (lemma10 (cong suc p008)) ⟩
+        Inverse.from perm (Inverse.to (pins (toℕ≤pred[n] (suc t))) zero) ≡⟨ p011 _ _ perm (toℕ≤pred[n] (suc t)) (s≤s z≤n) ⟩
+        perm ⟨$⟩ˡ suc (fromℕ< (s≤s (toℕ≤pred[n] t))) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (lemma10 (
+           begin
+           suc (toℕ t) ≡⟨ refl ⟩
+           suc (toℕ (suc t) ∸ 1) ≡⟨ cong (λ k → suc (toℕ k ∸ 1) ) (sym eq) ⟩
+           suc (toℕ (Inverse.to perm zero) ∸ 1) ∎ )) ⟩
         perm ⟨$⟩ˡ suc (fromℕ< p007) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (pred-fin (Inverse.to perm zero) p003 p007 ) ⟩
         perm ⟨$⟩ˡ (Inverse.to perm zero) ≡⟨ inverseˡ perm  ⟩
         # 0 ∎ where 
@@ -779,11 +776,21 @@
    pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
    pf0 = pcong-Fp eq
 
+shrink-pid : {n : ℕ} → (shrink (pid ∘ₚ flip (pins (toℕ≤pred[n] {suc n} (pid ⟨$⟩ʳ # 0)))) (p=0 pid)) =p= pid
+shrink-pid {zero}  = record { peq = λ () }
+shrink-pid {suc n} = record { peq = pf5 } where
+    pf5 :  (q : Fin (suc n)) → (shrink (pid ∘ₚ flip (pins (toℕ≤pred[n] {suc (suc n)} (pid ⟨$⟩ʳ # 0)))) (p=0 pid)) ⟨$⟩ʳ q ≡ pid ⟨$⟩ʳ q
+    pf5 zero = refl
+    pf5 (suc q) with <-fcmp ((pid ⟨$⟩ʳ (suc q))) (# 0) 
+    ... | tri> ¬a ¬b c = pf6 where
+      pf6 : suc (fromℕ< (≤-trans (fin<n {_} {q}) (Data.Nat.Properties.≤-reflexive refl))) ≡ suc q
+      pf6 = cong suc ( begin
+          fromℕ< (≤-trans (fin<n {_} {q}) (Data.Nat.Properties.≤-reflexive refl)) ≡⟨ lemma10 refl  ⟩ 
+          fromℕ< fin<n ≡⟨  fromℕ<-toℕ _ fin<n  ⟩ 
+          q ∎  ) where 
+             open ≡-Reasoning 
+
+
 pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid
 pFL0 {zero} = refl
-pFL0 {suc n} = cong (λ k → zero :: k ) pf3 where
-   pf4 : FL0 {n} ≡ perm→FL pid
-   pf4 = pFL0
-   pf3 : FL0 {n} ≡ perm→FL (shrink (pid ∘ₚ flip (pins (toℕ≤pred[n] {suc n} (pid ⟨$⟩ʳ # 0)))) (p=0 pid))
-   pf3 = {!!}
-
+pFL0 {suc n} = cong (λ k → zero :: k ) (trans pFL0 (pcong-pF (psym shrink-pid) )) 
diff -r f5b2145c174c -r e9de2bfef88d src/Solvable.agda
--- a/src/Solvable.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/Solvable.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}  -- we cannot use --cubical-compatible because of Termination
 
 open import Level hiding ( suc ; zero )
 open import Algebra
diff -r f5b2145c174c -r e9de2bfef88d src/fin.agda
--- a/src/fin.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/fin.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -100,25 +100,26 @@
 -- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl
 -- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl  )
 
--- fromℕ<-irrelevant 
--- 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})
 
+fpred-comm : {n : ℕ } → (x : Fin n) → toℕ (Data.Fin.pred x) ≡ toℕ x ∸ 1
+fpred-comm {suc n} zero = refl
+fpred-comm {suc n} (suc x) = begin
+       toℕ (Data.Fin.pred (suc x)) ≡⟨ sym ( toℕ-fromℕ< _ ) ⟩
+       toℕ (fromℕ< fin<n ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩
+       toℕ (fromℕ< (<-trans fin<n a<sa) ) ≡⟨  toℕ-fromℕ< _ ⟩
+       toℕ (suc x) ∸ 1 ∎  where open ≡-Reasoning
+
 -- 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) 
 
 -- toℕ-fromℕ<
 lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x
 lemma11 {n} {m} {x} n<m  = begin
-              toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m))
-           ≡⟨ toℕ-fromℕ< _ ⟩
-              toℕ x
-           ∎  where
-               open ≡-Reasoning
+      toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡⟨ toℕ-fromℕ< _ ⟩
+      toℕ x ∎  where open ≡-Reasoning
 
 x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} →  toℕ x < toℕ y  → Fin n
 x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ ))
diff -r f5b2145c174c -r e9de2bfef88d src/sym2.agda
--- a/src/sym2.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym2.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -52,8 +52,8 @@
    open ≡-Reasoning
 
    sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
-   sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
-   sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00}  = begin
+   sym2lem0 g h q with perm→FL g in g=00 | perm→FL h in h=00 
+   sym2lem0 g h q | zero :: (zero :: f0) | _ = begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
@@ -68,7 +68,7 @@
            ∎ where
              sym2lem1 :  g =p= pid
              sym2lem1 = FL-inject  g=00
-   sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin
+   sym2lem0 g h q | t | zero :: (zero :: f0) = begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
@@ -80,10 +80,10 @@
              [ g , pid ]  ⟨$⟩ʳ q
            ≡⟨ peq (idcomtr g) q ⟩
              q
-          ∎ where
+           ∎ where
              sym2lem2 :  h =p= pid
              sym2lem2 = FL-inject h=00
-   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin
+   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin
              [ g , h ]  ⟨$⟩ʳ q
            ≡⟨⟩
               h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
@@ -95,9 +95,10 @@
               g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) 
            ≡⟨ inverseʳ g   ⟩
              q
-          ∎ where
+           ∎ where
               g=h :  g =p= h
               g=h =  FL-inject (trans g=00 (sym h=00))
+   sym2lem0 g h q | s | t = ?
    solved :  (x : Permutation 2 2) → Commutator  (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid
    solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h  } 
    solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
diff -r f5b2145c174c -r e9de2bfef88d src/sym2n.agda
--- a/src/sym2n.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym2n.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 open import Level hiding ( suc ; zero )
 open import Algebra
 module sym2n where
diff -r f5b2145c174c -r e9de2bfef88d src/sym3.agda
--- a/src/sym3.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym3.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -102,59 +102,59 @@
    st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm  ((suc (suc zero)) :: (suc zero) :: (zero :: f0))  ]
 
    st02 :  ( g h : Permutation 3 3) →  ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4)
-   st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h
-   ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
-   ... | s | (zero :: (zero :: (zero :: f0))) | se |  record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
-   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } =
+   st02 g h with perm→FL g in ge | perm→FL h in he 
+   ... | (zero :: (zero :: (zero :: f0))) | t = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) )
+   ... | s | (zero :: (zero :: (zero :: f0))) | se = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) )
+   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = 
+   ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) = 
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) |  record { eq = ge } |  record { eq = he } = 
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (suc zero) :: (suc zero :: (zero :: f0 )) = 
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =
+   ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) =
         case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
 
-   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) =
            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) = 
            case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } |  record { eq = he } =  
+   ... | (zero :: (suc zero) :: (zero :: f0 )) |  (suc (suc zero)) :: (zero :: (zero :: f0 ))=  
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } |  record { eq = he } =   
+   ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))=   
            case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) = 
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } = 
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) = 
             case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } |  record { eq = he } =  
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))=  
             case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | ((suc zero) :: (zero :: (zero :: f0 ))) |  (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } |  record { eq = he } =  
+   ... | ((suc zero) :: (zero :: (zero :: f0 ))) |  (suc (suc zero)) :: (suc zero) :: (zero :: f0) =  
             case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } |  record { eq = he } =  
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  (zero :: (suc zero) :: (zero :: f0 )) =  
             case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =  
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc zero) :: (zero :: (zero :: f0 ))) =  
             case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =  
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (zero :: (zero :: f0 ))) =  
          case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } =   
+   ... | (suc zero) :: (suc zero :: (zero :: f0 )) |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) =   
             case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) =
           case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )
-   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } |  record { eq = he } = 
+   ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) = 
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } |  record { eq = he } =
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } |  record { eq = he } =
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) =
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 )))  | record { eq = ge } |  record { eq = he } =
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 )))  =
           case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
-   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 ))  | record { eq = ge } |  record { eq = he } =
+   ... |  ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 ))  =
           case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ))
    
    stage12  :  (x : Permutation 3 3) → stage1 x →  ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 )
@@ -170,12 +170,9 @@
    ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
       cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q
       cc q = begin
-             x ⟨$⟩ʳ q
-          ≡⟨ sym (f=g q) ⟩
-             f ⟨$⟩ʳ q
-          ≡⟨ f=e q ⟩
-             q
-          ∎ 
+             x ⟨$⟩ʳ q ≡⟨ sym (f=g q) ⟩
+             f ⟨$⟩ʳ q ≡⟨ f=e q ⟩
+             q ∎ 
    solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y
    ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl)
    ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h)
diff -r f5b2145c174c -r e9de2bfef88d src/sym3n.agda
--- a/src/sym3n.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym3n.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
diff -r f5b2145c174c -r e9de2bfef88d src/sym4.agda
--- a/src/sym4.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym4.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
diff -r f5b2145c174c -r e9de2bfef88d src/sym5.agda
--- a/src/sym5.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym5.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
diff -r f5b2145c174c -r e9de2bfef88d src/sym5a.agda
--- a/src/sym5a.agda	Sat Sep 23 19:22:22 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-{-# OPTIONS --cubical-compatible --safe #-}
-
---
--- checking does not terminate, sorry
---
-open import Level hiding ( suc ; zero )
-open import Algebra
-module sym5a where
-
-open import Symmetric 
-open import Data.Unit using (⊤ ; tt )
-open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
-open import Function hiding (flip)
-open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero)
-open import Data.Nat.Properties
-open import Relation.Nullary
-open import Data.Empty
-open import Data.Product
-
-open import Gutil 
-open import Putil 
-open import Solvable using (solvable)
-open import  Relation.Binary.PropositionalEquality hiding ( [_] )
-
-open import Data.Fin hiding (_<_ ; _≤_  ; lift )
-open import Data.Fin.Permutation  hiding (_∘ₚ_)
-
-infixr  200 _∘ₚ_
-_∘ₚ_ = Data.Fin.Permutation._∘ₚ_
-
-open import Data.List  hiding ( [_] )
-open import nat
-open import fin
-open import logic
-
-open _∧_
-
-¬sym5solvable : ¬ ( solvable (Symmetric 5) )
-¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where
---
---    dba       1320      d → b → a → d
---    (dba)⁻¹   3021      a → b → d → a
---    aec       21430
---    (aec)⁻¹   41032
---    [ dba , aec ] = (abd)(cea)(dba)(aec) = abc
---      so commutator always contains abc, dba and aec
-
-     open ≡-Reasoning
-
-     open solvable
-     open Solvable ( Symmetric 5) 
-     end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
-     end5 x der = end sol x der
-
-     0<4 : 0 < 4
-     0<4 = s≤s z≤n
-
-     0<3 : 0 < 3
-     0<3 = s≤s z≤n
-
-     --- 1 ∷ 2 ∷ 0 ∷ []      abc
-     3rot : Permutation 3 3
-     3rot = pid {3} ∘ₚ pins (n≤ 2)
-
-     save2 : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) →  Permutation  5 5 
-     save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) 
-
-     -- Permutation 5 5 include any Permutation 3 3
-     any3 : {i j : ℕ }  → Permutation 3 3  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
-     any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) 
-
-     any3cong : {i j : ℕ }  → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4  =p= any3 y i<3 j<4
-     any3cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )}
-         (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl 
-
-     open _=p=_
-
-     -- derving n includes any Permutation 3 3, 
-     any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) →  (i<3 : i ≤ 3 ) → (j<4 :  j ≤ 4 ) → deriving n (any3 abc i<3 j<4)
-     any3de {i} {j} zero abc i<3 j<4 = Level.lift tt
-     any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc  ∘ₚ abc) i<3 j0<4 ) (any3de n (abc  ∘ₚ abc) i0<3 j<4 ))  where
-         i0 : ℕ
-         i0 = ?
-         j0 : ℕ
-         j0 = ?
-         i0<3 : i0 ≤ 3
-         i0<3 = {!!}
-         j0<4 : j0 ≤ 4
-         j0<4 = {!!}
-         abc-from-comm : [ any3 (abc  ∘ₚ abc) i<3 j0<4  , any3 (abc  ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4
-         abc-from-comm = {!!}
-
-     abc : {i j : ℕ }  → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation  5 5
-     abc i<3 j<4 = any3 3rot i<3 j<4
-
-     counter-example :  ¬ (abc 0<3 0<4  =p= pid )
-     counter-example eq with ←pleq _ _ eq
-     ...  | ()
-
diff -r f5b2145c174c -r e9de2bfef88d src/sym5h.agda
--- a/src/sym5h.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym5h.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS --cubical-compatible --safe #-}
+{-# OPTIONS  --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
diff -r f5b2145c174c -r e9de2bfef88d src/sym5n.agda
--- a/src/sym5n.agda	Sat Sep 23 19:22:22 2023 +0900
+++ b/src/sym5n.agda	Sat Sep 23 22:43:47 2023 +0900
@@ -1,4 +1,3 @@
-{-# OPTIONS --cubical-compatible  #-}
 {-# OPTIONS --guardedness #-}
 
 open import Level hiding ( suc ; zero )