# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1697073136 -32400
# Node ID 1ff0b95e437f146454320a1692a16b393a72fc2d
# Parent  5d7a811ee428c05f40178fbdc3f12ff6ef052c15
try to add --cubical-compatible on Solvable

diff -r 5d7a811ee428 -r 1ff0b95e437f src/FLComm.agda
--- a/src/FLComm.agda	Sun Sep 24 18:10:44 2023 +0900
+++ b/src/FLComm.agda	Thu Oct 12 10:12:16 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}   --  cannot use --cubical-compatible because of Solvable
+{-# OPTIONS --cubical-compatible --safe #-}   
 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
 module FLComm (n : ℕ) where
 
@@ -152,23 +152,20 @@
 
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
 CommStage→ zero x (Level.lift tt) = anyP (anyFL n) (perm→FL x)
-CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 where
+CommStage→ (suc i) ix (comm {g} {h} p q eq ) = comm2 where
   G = perm→FL g
   H = perm→FL h
-  comm3 :  perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
+  comm3 :  perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL ix
   comm3 = begin
               perm→FL [ FL→perm G , FL→perm H ] 
            ≡⟨ pcong-pF (comm-resp (FL←iso _) (FL←iso _)) ⟩
               perm→FL [ g , h ]
+           ≡⟨ pcong-pF (psym eq) ⟩
+              perm→FL ix
           ∎  where open ≡-Reasoning
-  comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i))
+  comm2 : Any (_≡_ (perm→FL ix)) (CommFListN (suc i))
   comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3
      ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) )
-CommStage→ (suc i) x (ccong {f} {x} eq p) =
-      subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))))
-          (comm4 eq) (CommStage→ (suc i) f p ) where
-   comm4 : f =p= x →  perm→FL f ≡ perm→FL x
-   comm4 = pcong-pF
 
 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0
diff -r 5d7a811ee428 -r 1ff0b95e437f src/Homomorphism.agda
--- a/src/Homomorphism.agda	Sun Sep 24 18:10:44 2023 +0900
+++ b/src/Homomorphism.agda	Thu Oct 12 10:12:16 2023 +0900
@@ -293,7 +293,7 @@
          f x ≈⟨ h1-is-solution _ ⟩
          h1 x ∎ 
 -- 
--- Another from of Fundamental Homomorphism Theorm 
+-- Another form of Fundamental Homomorphism Theorm 
 --    i.e.  G / Ker f ≈ Im f
 
 record IsImage {c d : Level} (G  : Group c d) (H : Group c d)
diff -r 5d7a811ee428 -r 1ff0b95e437f src/Solvable.agda
--- a/src/Solvable.agda	Sun Sep 24 18:10:44 2023 +0900
+++ b/src/Solvable.agda	Thu Oct 12 10:12:16 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}  -- we cannot use --cubical-compatible because of Termination
+{-# OPTIONS --cubical-compatible --safe #-} 
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -21,18 +21,17 @@
 [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h 
 
 data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where
-  comm  : {g h : Carrier} → P g → P h  → Commutator P [ g , h ] 
-  ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g
+  comm  : {g h i : Carrier} → P g → P h  → i ≈ [ g , h ] → Commutator P  i
 
 deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m)
 deriving 0 x = Lift (Level.suc n ⊔ m) ⊤
 deriving (suc i) x = Commutator (deriving i) x 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
 deriving-subst : { i : ℕ } → {x y : Carrier } → x ≈ y → (dx : deriving i x ) → deriving i y 
 deriving-subst {zero} {x} {y} x=y dx = lift tt
-deriving-subst {suc i} {x} {y} x=y dx = ccong x=y dx
+deriving-subst {suc i} {x} {y} x=y (comm ig ih x=gh) = comm ig ih (gtrans (gsym x=y) x=gh)
 
 record solvable : Set (Level.suc n ⊔ m) where
   field 
@@ -62,8 +61,7 @@
 
 deriving-inv : { i : ℕ } → { x  : Carrier } → deriving i x → deriving i ( x ⁻¹ )
 deriving-inv {zero} {x} (lift tt) = lift tt
-deriving-inv {suc i} {_} (comm x x₁ )   = ccong (lemma4 _ _) (comm x₁ x) 
-deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix )
+deriving-inv {suc i} {x} (comm ig ih x=gh )   = comm ih ig (gtrans (⁻¹-cong x=gh) (gsym (lemma4 _ _)))
 
 idcomtr : (g  : Carrier ) → [ g , ε  ] ≈ ε 
 idcomtr g  = begin
@@ -85,7 +83,7 @@
 
 deriving-ε : { i : ℕ } → deriving i ε
 deriving-ε {zero} = lift tt
-deriving-ε {suc i} = ccong (idcomtr ε) (comm deriving-ε deriving-ε) 
+deriving-ε {suc i} = comm (deriving-ε {i}) (deriving-ε {i}) (gsym (idcomtr ε))
 
 comm-refl : {f g : Carrier } → f ≈ g  → [ f ,  g ] ≈ ε 
 comm-refl {f} {g} f=g = begin
@@ -111,7 +109,9 @@
 
 Pcomm : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i (b ∙ (a ∙ b ⁻¹ ))
 Pcomm {a} {b} zero (lift tt) = lift tt
-Pcomm {.([ _ , _ ])} {b} (suc i) (comm {g} {h} pg ph ) = ccong cc2 (comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph)) where
+Pcomm {a} {b} (suc i) (comm {g} {h} pg ph eq ) = comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph) (gtrans cc3 (gsym cc2)) where
+   cc3 : b ∙ (a ∙ b ⁻¹) ≈ b ∙ ([ g , h ] ∙ b ⁻¹)
+   cc3 = cdr (car eq ) 
    cc2 : [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈ b ∙ ([ g , h ] ∙ b ⁻¹)
    cc2 = begin
     [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈⟨ grefl ⟩ 
@@ -133,7 +133,6 @@
     ((b  ∙ g ⁻¹ )  ∙ h ⁻¹ ) ∙ (g ∙ (h ∙ b ⁻¹)) ≈⟨ solve monoid ⟩ 
     b ∙ (( g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h ) ∙ b ⁻¹) ≈⟨ grefl ⟩
     b ∙ ([ g , h ] ∙ b ⁻¹) ∎
-Pcomm {a} {b} (suc i) (ccong f=a pa) = ccong (∙-cong grefl (∙-cong f=a grefl)) (Pcomm {_} {b} (suc i) pa)
 
 -- Finitely Generated Commutator is normal subgroup of G
 
diff -r 5d7a811ee428 -r 1ff0b95e437f src/sym2.agda
--- a/src/sym2.agda	Sun Sep 24 18:10:44 2023 +0900
+++ b/src/sym2.agda	Thu Oct 12 10:12:16 2023 +0900
@@ -1,4 +1,4 @@
-{-# OPTIONS  --safe #-}
+{-# OPTIONS --cubical-compatible --safe #-}
 
 open import Level hiding ( suc ; zero )
 open import Algebra
@@ -51,67 +51,79 @@
    open _=p=_
    open ≡-Reasoning
 
+   -- we cannot use sym2lem0 g h q with perm→FL g in g=00 | perm→FL h in h=00 
+   --   because of Panic: uncaught pattern violation 
+
    sym2lem0 :  ( g h : Permutation 2 2 ) → (q : Fin 2)  → ([ g , h ]  ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
    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 ))) 
-           ≡⟨ cong (λ k → h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ  k))) ((peqˡ sym2lem1 _ )) ⟩
-              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
-           ≡⟨ cong (λ k →  h ⟨$⟩ʳ k ) (peq sym2lem1 _ )  ⟩
-              h ⟨$⟩ʳ  (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
-           ≡⟨⟩
-             [ pid , h ]  ⟨$⟩ʳ q
-           ≡⟨ peq (idcomtl h) q ⟩
-             q
-           ∎ where
-             sym2lem1 :  g =p= pid
-             sym2lem1 = FL-inject  g=00
-   sym2lem0 g h q | t | zero :: (zero :: f0) = begin
-             [ g , h ]  ⟨$⟩ʳ q
-           ≡⟨⟩
-              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ peq sym2lem2 _   ⟩
-              pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
-              pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨⟩
-             [ g , pid ]  ⟨$⟩ʳ q
-           ≡⟨ peq (idcomtr g) q ⟩
-             q
-           ∎ where
-             sym2lem2 :  h =p= pid
-             sym2lem2 = FL-inject h=00
-   sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin
-             [ g , h ]  ⟨$⟩ʳ q
-           ≡⟨⟩
-              h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ peq (psym g=h ) _  ⟩
-              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
-              g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
-           ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
-              g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) 
-           ≡⟨ inverseʳ g   ⟩
-             q
-           ∎ where
-              g=h :  g =p= h
-              g=h =  FL-inject (trans g=00 (sym h=00))
-   sym2lem0 g h q | s | t = ?
+   ... | s | t = ?
+
+--  sym2lem0 g h q | zero :: (zero :: f0) | _ = begin
+--            [ g , h ]  ⟨$⟩ʳ q
+--          ≡⟨⟩
+--             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ cong (λ k → h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ  k))) ((peqˡ sym2lem1 _ )) ⟩
+--             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
+--          ≡⟨ cong (λ k →  h ⟨$⟩ʳ k ) (peq sym2lem1 _ )  ⟩
+--             h ⟨$⟩ʳ  (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) 
+--          ≡⟨⟩
+--            [ pid , h ]  ⟨$⟩ʳ q
+--          ≡⟨ peq (idcomtl h) q ⟩
+--            q
+--          ∎ where
+--            sym2lem1 :  g =p= pid
+--            sym2lem1 = FL-inject  g=00
+--  sym2lem0 g h q | t | zero :: (zero :: f0) = begin
+--            [ g , h ]  ⟨$⟩ʳ q
+--          ≡⟨⟩
+--             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ peq sym2lem2 _   ⟩
+--             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ cong (λ k → pid ⟨$⟩ʳ  (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩
+--             pid ⟨$⟩ʳ  (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨⟩
+--            [ g , pid ]  ⟨$⟩ʳ q
+--          ≡⟨ peq (idcomtr g) q ⟩
+--            q
+--          ∎ where
+--            sym2lem2 :  h =p= pid
+--            sym2lem2 = FL-inject h=00
+--  sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin
+--            [ g , h ]  ⟨$⟩ʳ q
+--          ≡⟨⟩
+--             h ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ peq (psym g=h ) _  ⟩
+--             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ cong (λ k →   g ⟨$⟩ʳ  (g ⟨$⟩ʳ  k) ) (peqˡ (psym g=h) _)  ⟩
+--             g ⟨$⟩ʳ  (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) 
+--          ≡⟨ cong (λ k → g  ⟨$⟩ʳ k) ( inverseʳ g )  ⟩
+--             g ⟨$⟩ʳ  ( g ⟨$⟩ˡ q ) 
+--          ≡⟨ inverseʳ g   ⟩
+--            q
+--          ∎ 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
-   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
-      cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
+   solved x (comm {f} {g} _ _ eq ) = record { peq = cc }  where
+      cc : (q : Fin 2) → x ⟨$⟩ʳ q ≡ pid ⟨$⟩ʳ q 
       cc q = begin
-             x ⟨$⟩ʳ q
-          ≡⟨ sym (f=g q) ⟩
-             f ⟨$⟩ʳ q
-          ≡⟨ f=e q ⟩
-             q
-          ∎ where open ≡-Reasoning
+             x ⟨$⟩ʳ q ≡⟨ peq eq q ⟩
+             [ f , g ] ⟨$⟩ʳ q ≡⟨ sym2lem0 f g q ⟩
+             q ∎ where open ≡-Reasoning
+
+   -- solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d
+--   ... | record { peq = f=e }  =  record  { peq = λ q → cc q } where
+--      cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q
+--      cc q = begin
+--             x ⟨$⟩ʳ q
+--          ≡⟨ sym (f=g q) ⟩
+--             f ⟨$⟩ʳ q
+--          ≡⟨ f=e q ⟩
+--             q
+--          ∎ where open ≡-Reasoning
+-- 
 
 
 
-
diff -r 5d7a811ee428 -r 1ff0b95e437f src/sym5h.agda
--- a/src/sym5h.agda	Sun Sep 24 18:10:44 2023 +0900
+++ b/src/sym5h.agda	Thu Oct 12 10:12:16 2023 +0900
@@ -101,7 +101,7 @@
            s12 : abc ≡ perm→FL [ dba , aec ]  
            s12 = refl
            s11 : FL→perm abc =p= [ dba , aec ]  
-           s11 = ptrans (pcong-Fp s12 ) (FL←iso _)
+           s11 = ptrans (pcong-Fp s12 ) ? -- (FL←iso _)
            s17 : deriving  (suc i) ( FL→perm abc )
            s17 = ccong (psym s11) (comm (Pcomm {_} {FL→perm dc} i (deriving-inv s10)) (Pcomm {_} {FL→perm be} i s10) )