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

diff -r 1874c573682f -r d08663bae245 src/FundamentalHomorphism.agda
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 16:50:56 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 19:58:30 2023 +0900
@@ -83,42 +83,34 @@
         n : Carrier 
         is-an : (x : Carrier) → an N n x
 
-record Factor (A : Group c c ) (N : NormalSubGroup A) (a b : Group.Carrier A )  : Set c  where
+f0 :  {A : Group c c }  (N : NormalSubGroup A )  (x y : Group.Carrier A) → an N x y
+f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = ? } where
+   open Group A
+   open NormalSubGroup N
+   open IsGroupHomomorphism normal
+
+record Factor (A : Group c c ) (N : NormalSubGroup A) (a b : Group.Carrier A)  : Set c  where
    open Group A
    open NormalSubGroup N
    open IsGroupHomomorphism normal
    field
-       factor : Carrier
-       is-factor : b ∙ ⟦ factor ⟧ ≈ a
+       factor :  Carrier
+       is-factor :  b ∙ ⟦ factor ⟧ ≈ a
 
-¬¬Factor : (A : Group c c ) (N : NormalSubGroup A) → ¬ ¬ ( (a b : Group.Carrier A )  →  Factor A N a b )
-¬¬Factor A N neg = ⊥-elim ( fa ( λ y → record { n = y ; is-an = λ x → record { a = x ∙ ⟦ y ⟧ ⁻¹ ; aN=x = f03 } }  ))  where
+¬¬Factor : (A : Group c c ) (N : NormalSubGroup A) → ¬ ( ( x y : Group.Carrier A) →  ¬ Factor A N  x y )
+¬¬Factor A N  neg = ⊥-elim ( fa (f0 N) )  where
    open Group A
    open NormalSubGroup N
    open IsGroupHomomorphism normal
    open EqReasoning (Algebra.Group.setoid A)
    open Gutil A
    open aN
-   f03 : {x y : Carrier } → x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈ x
-   f03 {x} {y} = begin
-      x ∙ ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧ ≈⟨ ? ⟩ 
-      x ∙ ( ⟦ y ⟧ ⁻¹ ∙ ⟦ y ⟧)  ≈⟨ ? ⟩ 
-      x ∎
-   fa : ¬ ( (x : Carrier) →  aN N ) 
-   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 ∙ ( ( 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
-               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 = ?
+   open an
+
+   fa : ¬ ( (x y : Group.Carrier A) → an N x y )
+   fa f = neg ε (a (f ε ε)) record { factor = ε ; is-factor = aN=x (f ε ε)  }
+   -- λ x y → record { factor = ? ; is-factor = ? } )
+             
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {