# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674700318 -32400
# Node ID e83341c5c981202cff592b8235328969583c681e
# Parent  33d248c9081ec8b71da13398ca1b58afeb89ee01
...

diff -r 33d248c9081e -r e83341c5c981 src/Fundamental.agda
--- a/src/Fundamental.agda	Thu Jan 26 07:55:24 2023 +0900
+++ b/src/Fundamental.agda	Thu Jan 26 11:31:58 2023 +0900
@@ -164,8 +164,7 @@
            φ-cong = ?
 
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f = a (f ε) ∙ ⟦ n (f ε) ⟧ where
-         afn = (a (f (a (f ε) ∙ ⟦ n (f ε) ⟧))) ⁻¹
+    inv-φ f = ⟦ n (f ε) ⟧ 
 
     cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
     cong-i = ?
@@ -180,16 +179,35 @@
        ⟦ fn ⟧ ∎ where
           z = fa ⁻¹
 
+    k*factor : {x y z : Carrier } → ⟦ factor y x ⟧ ≈ ⟦ factor (z ∙ y) x ⟧
+    k*factor {x} {y} {z} = ?
+
+    cong-factor : {x y z : Carrier } → ⟦ factor y x ⟧ ≈ ⟦ factor y z ⟧   
+    cong-factor {x} {y} {z} = begin
+       ⟦ factor y x ⟧ ≈⟨ ? ⟩ 
+       ⟦ factor ( x ∙ z ⁻¹ ∙ y   ) x ⟧ ≈⟨ ? ⟩ 
+       x ⁻¹ ∙ ( x ∙ z ⁻¹ ∙ y )  ≈⟨ ? ⟩ 
+       z ⁻¹ ∙ y  ≈⟨ ? ⟩ 
+       ⟦ factor y z ⟧ ∎ 
+
     is-inverse : (f : (x : Carrier) → aN K x ) →  {y : Carrier} → ⟦ n (φ (inv-φ f) y) ⟧ ≈ ⟦ n (f y) ⟧
     is-inverse f {y} = begin
        ⟦ n (φ (inv-φ f) y) ⟧  ≈⟨ grefl G ⟩
-       ⟦ n (φ (a (f ε) ∙ ⟦ n (f ε) ⟧) y) ⟧  ≈⟨ grefl G ⟩
-       ⟦ factor y (a (f ε) ∙ ⟦ n (f ε) ⟧) ⟧  ≈⟨ grefl G ⟩
-       ⟦ factor y afn ⟧  ≈⟨ ? ⟩
+       ⟦ n (φ ⟦ n (f ε) ⟧  y) ⟧  ≈⟨ grefl G ⟩
+       ⟦ factor y ⟦ n (f ε) ⟧ ⟧  ≈⟨ ? ⟩
        ⟦ factor y afn' ⟧  ≈⟨ factor=nf f ⟩
        ⟦ n (f y) ⟧ ∎ where
-           afn = a (f ε) ∙ ⟦ n (f ε) ⟧
+           afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
+           afn = aN=x (f ε)
            afn' = (a (f y)) ⁻¹
+           f00 : ⟦ n (f ε) ⟧ ≈ (a (f y)) ⁻¹
+           f00 = begin
+              ⟦ n (f ε) ⟧ ≈⟨ ? ⟩ 
+              (a (f ε)) ⁻¹ ∙ a (f ε) ∙ ⟦ n (f ε) ⟧ ≈⟨ ? ⟩
+              (a (f ε)) ⁻¹ ∙ ε ≈⟨ ? ⟩
+              ⟦ n (f y) ⟧ ∙ y ⁻¹  ≈⟨ ? ⟩
+              (a (f y)) ⁻¹ ∙ ( a (f y) ∙ ⟦ n (f y) ⟧ ∙ y ⁻¹ ) ≈⟨ ? ⟩
+              (a (f y)) ⁻¹ ∎
 
     φ-surjective : Surjective φe 
     φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse } where