# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674893405 -32400
# Node ID 523adaf1dceca4ada365fceb3bba5615dad769aa
# Parent  386ece574509d907b526cb78f526bf05ec11766a
...

diff -r 386ece574509 -r 523adaf1dcec src/Fundamental.agda
--- a/src/Fundamental.agda	Sat Jan 28 10:55:32 2023 +0900
+++ b/src/Fundamental.agda	Sat Jan 28 17:10:05 2023 +0900
@@ -55,6 +55,8 @@
 
 import Axiom.Extensionality.Propositional
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+open import Tactic.MonoidSolver using (solve; solve-macro)
+
 
 record NormalSubGroup (A : Group c c )  : Set c  where
    open Group A
@@ -75,7 +77,11 @@
         a n : Group.Carrier A 
         aN=x :  a ∙ ⟦ n ⟧ ≈ x
 
-open import Tactic.MonoidSolver using (solve; solve-macro)
+factor' :  {A : Group c c }  (N : NormalSubGroup A ) (f : (x : Group.Carrier A) → aN N x )  (a b : Group.Carrier A  ) → Group.Carrier A
+factor' = ?
+is-factor' :  {A : Group c c }  (N : NormalSubGroup A ) (f : (x : Group.Carrier A) → aN N x )  → 
+    (a b : Group.Carrier A ) →  A < A < b ∙ ( NormalSubGroup.⟦_⟧ N (factor' {A} N f a b )) > ≈ a >
+is-factor' {A} N f a b = ?
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
@@ -256,7 +262,7 @@
           z = fa ⁻¹
 
     φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → f ∋ x → f ∋ y →  ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧
-    φ-factor f {x} {y} gx gy = begin
+    φ-factor f {x} {y} fx fy = begin
        ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
        (a (f x))  ⁻¹  ∙ x ≈⟨ ? ⟩ 
        (((a (f y))  ⁻¹  ∙ y ) ∙ ((a (f y))  ⁻¹  ∙ y ))  ⁻¹ ∙ ( (a (f x))  ⁻¹  ∙ x ) ≈⟨ ? ⟩ 
@@ -268,19 +274,39 @@
        (a (f y))  ⁻¹  ∙ y ≈⟨ ? ⟩ 
        ⟦ n (f y) ⟧ ∎ where
           fa00 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x
-          fa00 = gx
+          fa00 = fx
           fa01 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y
-          fa01 = gy
+          fa01 = fy
           an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x)
           an01 y = is-factor (a (f x)) y
           an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x)
           an04 = is-factor (a (f x)) (a (f y))
+          an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧
+          an07 {z} {w} = gsym ( is-factor z w )
+          an05 : {z : Carrier} → f ∋ z  → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧
+          an05 {z} fz = begin
+              ⟦ n (f z) ⟧ ≈⟨ ? ⟩
+              ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧  ≈⟨ ? ⟩
+              (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧)  ≈⟨ ∙-cong grefl fz ⟩
+              (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z))))  ⟩
+              (a (f z) ⁻¹) ∙ (a (f z)  ∙ ⟦ factor z (a (f z))  ⟧ ) ≈⟨ ? ⟩
+              ⟦ factor z ( a ( f z)) ⟧ ∎
+          an06 : {z : Carrier} → ⟦ factor z z ⟧ ≈ ε 
+          an06 {z} = begin
+             ⟦ factor z z ⟧ ≈⟨ ? ⟩  
+             (z ⁻¹ ∙ z ) ∙ ⟦ factor z z ⟧ ≈⟨ ? ⟩  
+             z ⁻¹ ∙ ( z  ∙ ⟦ factor z z ⟧ ) ≈⟨ ∙-cong grefl (is-factor z z) ⟩  
+             z ⁻¹ ∙ z ≈⟨ ? ⟩  
+             ε ∎
           an03 : ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈ ε 
           an03 = begin
               ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈⟨ ? ⟩ 
-              ⟦ n (f y) ⁻¹ ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
-              ⟦ n (f y) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
-              ⟦ n (f y) ⟧ ⁻¹ ∙ (a (f x) ∙ x  ⁻¹ )  ≈⟨ ? ⟩ 
+              ⟦ factor y (a (f y)) ⟧ ⁻¹  ∙ ⟦ factor x (a (f x)) ⟧ ≈⟨ ? ⟩ 
+              ⟦ factor y (a (f y)) ⟧ ⁻¹  ∙ ⟦ factor x ( x ∙ ⟦ n (f x) ⟧  ⁻¹ )  ⟧ ≈⟨ ? ⟩ 
+              ⟦ n (f (y ⁻¹  ∙ x)) ⟧ ≈⟨ ? ⟩ 
+              ⟦ factor (y ⁻¹  ∙ x) (a (f (y ⁻¹  ∙ x))) ⟧ ≈⟨ ? ⟩ 
+              ⟦ n (f ⟦ ε ⟧ ) ⟧ ≈⟨ ? ⟩ 
+              ⟦ ε ⟧ ≈⟨ ? ⟩ --   ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ →  ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
               ε  ∎
 
     is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧