# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674978656 -32400
# Node ID 1874c573682ffb5213f353d789a250204ccfe731
# Parent  f257ab4afa516da5867b4854bd39c4a980f8c666
...

diff -r f257ab4afa51 -r 1874c573682f src/FundamentalHomorphism.agda
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 16:08:09 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 16:50:56 2023 +0900
@@ -108,23 +108,17 @@
    fa f = neg ( λ a b →  record { factor = n (f ( a ∙ b ⁻¹)) ; is-factor = fa01 a b }  ) where
         fa01 : (a b : Carrier ) →  b ∙  ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈ a 
         fa01 a b = begin
-           b ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧  ≈⟨ ? ⟩ 
-           b ∙ (ε ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ) ≈⟨ ? ⟩ 
-           b ∙ (( f02  ⁻¹ ∙  f02 ) ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ) ≈⟨ ? ⟩ 
-           b ∙ ( f02  ⁻¹ ∙ ( f02  ∙  ⟦ n  (f ( a ∙ b ⁻¹)) ⟧ ))  ≈⟨ cdr ( cdr ( an.aN=x (is-an  (f ( a ∙ b ⁻¹)) (f05 ∙ a)  )))  ⟩ 
-           b ∙ (f02 ⁻¹ ∙ ( f05  ∙ a))  ≈⟨ ? ⟩ 
-           b ∙ ( (f02 ⁻¹ ∙ f02 ) ∙ b ⁻¹)  ∙ a  ≈⟨ ? ⟩ 
-           b ∙ ( ε ∙ b ⁻¹)  ∙ a  ≈⟨ ? ⟩ 
-           b ∙ ( b ⁻¹ ∙ a )   ≈⟨ ? ⟩ 
-           (b ∙  b ⁻¹ ) ∙ a    ≈⟨ ? ⟩ 
-           ε ∙ a    ≈⟨ ? ⟩ 
+           b ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧  ≈⟨  ?  ⟩ 
+           b ∙ ( ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ ( an.a (is-an (f ( a ∙ b ⁻¹) )  (a ∙ ⟦ b ⁻¹ ⟧ )  ) ∙ ⟦ n  (f ( a ∙ b ⁻¹)) ⟧))  ≈⟨ cdr ( cdr (f06 ( a ∙ b ⁻¹)  (a ∙ ⟦ b ⁻¹ ⟧ ))) ⟩ 
+           b ∙ ( ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ (a ∙ ⟦ b ⁻¹ ⟧ )) ≈⟨ ? ⟩ 
+           ⟦ b ⟧ ∙ ( a ∙ ⟦ b ⁻¹ ⟧ )  ≈⟨ ? ⟩ 
            a  ∎  where
-               f05 : Carrier
-               f05 = a ∙ b ⁻¹
-               f02 : Carrier
-               f02 = an.a (is-an (f (a ∙ b ⁻¹)) (f05 ∙ a))
-               f04 : f02 ∙ b ⁻¹ ≈ f05
-               f04 = ?
+               f06 : (x y : Carrier ) → an.a (is-an (f x) y ) ∙ ⟦ n (f x) ⟧ ≈ y
+               f06 x y = an.aN=x (is-an (f x) y)
+               f07 : (y : Carrier ) → an.a (is-an (f ( a ∙ b ⁻¹)) y ) ∙ ⟦ n (f ( a ∙ b ⁻¹)) ⟧ ≈ y
+               f07  y = an.aN=x (is-an (f ( a ∙ b ⁻¹)) y)
+               f08 : ( b ⁻¹ ∙ ⟦ b ⟧ ) ∙ ( an.a (is-an (f ( a ∙ b ⁻¹) )  (a ∙ ⟦ b ⁻¹ ⟧ ))) ≈ ε   
+               f08 = ?
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {