--- a/src/FundamentalHomorphism.agda	Sun Jan 29 20:31:03 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 21:05:55 2023 +0900
@@ -81,11 +81,17 @@
         is-an : (x : Carrier) → an N n x
 
 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
+f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = gk02  } where
    open Group A
    open NormalSubGroup N
    open IsGroupHomomorphism normal
-
+   open EqReasoning (Algebra.Group.setoid A)
+   open Gutil A
+   gk02 : {x g : Carrier } →  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x
+   gk02 {x} {g}  = begin  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid  ⟩ 
+         x ∙  ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧)  ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ 
+         x ∙ ε  ≈⟨ proj₂ identity _  ⟩ 
+         x ∎
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
@@ -152,29 +158,30 @@
     open Gutil G
 
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹)   ; aN=x = ?  } }
+    φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹)   ; aN=x = gk02  } } where
+       gk02 : {x : Carrier } →  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x
+       gk02 {x} = begin  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid  ⟩ 
+         x ∙  ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧)  ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ 
+         x ∙ ε  ≈⟨ proj₂ identity _  ⟩ 
+         x ∎
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
     φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
        record { cong = ? } }}}
 
+    -- gk03 : {f : Group.Carrier (G / K) } → ⟦ n f  ⟧ ≈ ⟦ ⟦ n f ⟧ ⟧  -- a (is-an f x)  ∙ ⟦ n f ⟧ ≡ x
+    -- gk03 {x} = ?                                                   --  
+
     φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
     φe = record { _⟨$⟩_ = φ ; cong = ?  }  where
            φ-cong : {f g : Carrier } → f ≈ g  → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧
            φ-cong = ?
 
-    -- inverse ofφ
-    --  f = λ x → record { a = af ; n = fn ; aN=x = x ≈ af ∙ ⟦ fn ⟧  )   = (af)K  , fn ≡ factor x af , af ≡ a (f x)
-    --        (inv-φ f)K ≡ (af)K
-    --           φ (inv-φ f) x → f (h0 x)
-    --           f x → φ (inv-φ f) (h1 x)
-
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
     inv-φ f =  n f  
 
-
     cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
-    cong-i = ?
+    cong-i {f} {g} nf=ng = ? 
 
     is-inverse : (f : aN K  ) →  ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
     is-inverse f = begin