--- a/src/homomorphism.agda	Tue Sep 05 11:13:19 2023 +0900
+++ b/src/homomorphism.agda	Wed Sep 06 11:21:39 2023 +0900
@@ -74,7 +74,7 @@
     anaN=x (an n x eq pn) = eq
     an-factor : {x y a : Carrier } → (xua : IsaN N (x ∙ y) a ) → IsaN N x (a ∙ y ⁻¹) × IsaN N y y
     an-factor {x} {y} {a} (an n a1 eqa pn) = an n1 _ an02 (Pcomm pn) 
-                  , an n2 _ an03 Pε where
+                  , an n1 _ an03 Pε where
         an04 : x ∙ y ∙ n  ≈ a 
         an04 = eqa
         -- n ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)
@@ -108,10 +108,27 @@
            b ∙ n ≈⟨ car (gsym eq) ⟩
            a ∙ n ≈⟨ eq1 ⟩
            x ∎
+    conj : (n x : Carrier) → Carrier
+    conj n x = x ∙ (n ∙ x ⁻¹)
+    Pconj  : (n x : Carrier) → P n → P (conj n x)
+    Pconj n x pn = Pcomm pn
+    aN=Na : {x n : Carrier} → x ∙ n ≈ conj n x ∙ x 
+    aN=Na {x} {n}  = gsym ( begin
+        (x ∙ (n ∙ x ⁻¹)) ∙ x ≈⟨ solve monoid ⟩
+        (x ∙ n ) ∙ (x ⁻¹ ∙ x) ≈⟨ cdr (proj₁ inverse _) ⟩
+        (x ∙ n ) ∙ ε  ≈⟨ proj₂ identity _ ⟩
+        x ∙ n ∎ )
+    Na=aN : {x n  : Carrier} → n ∙ x ≈ x ∙ conj n (x ⁻¹) 
+    Na=aN {x} {n}  = gsym ( begin
+        x ∙ ( x ⁻¹ ∙ (n ∙ (x ⁻¹ ) ⁻¹ ) )  ≈⟨ solve monoid ⟩
+        (x ∙ x ⁻¹ ) ∙ (n ∙ (x ⁻¹) ⁻¹) ≈⟨ ∙-cong (proj₂ inverse _) (cdr f⁻¹⁻¹≈f) ⟩
+        ε ∙ (n ∙ x) ≈⟨ proj₁ identity _ ⟩
+        n ∙ x ∎ )
+
     aneq : {a b : Carrier } → a ≈ b → aNeq N a b
     aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt }   
-    aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x)  →  naN ia ≈ naN ib
-    aNeq→n-eq eq = ?
+    -- this may wrong 
+    -- aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x)  →  naN ia ≈ naN ib
 
 _/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
@@ -201,28 +218,20 @@
                  a ∎
        gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) 
        gkcong⁻¹ {x} {y} x=y  = record { eq→ = gk07 ; eq← =  gk08 }  where
+          --  a⁻¹N     ≈ (Na)⁻¹          ≈ (aN)⁻¹        ≈ (bN)⁻¹        ≈ (Nb)⁻¹         ≈ b⁻¹N
+          --  a ⁻¹ ∙ n ≈ ( n ⁻¹ ∙ a ) ⁻¹ ≈ ( a ∙ n₁ ) ⁻¹ ≈ ( b ∙ n₂ ) ⁻¹ ≈ ( n₃  ∙ b ) ⁻¹ ≈ b ⁻¹ ∙ n₃
           gk07 : {a : Carrier } →  IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a
-          gk07 {a} (an n _ eq pn) = an n _ gk05 pn where
-              gk06 : x ∙ n ≈ a → y ∙ n ≈ a
-              gk06 eq with eq→ x=y (an n _ eq pn)
-              ... | an n1 .a eq1 pn = ?
-              gk05 :  y ⁻¹ ∙ n   ≈ a
-              gk05 = begin
-                 y ⁻¹ ∙ n   ≈⟨ cdr ( gsym  f⁻¹⁻¹≈f ) ⟩
-                 y ⁻¹ ∙ ( n ⁻¹ ) ⁻¹  ≈⟨ lemma5 _ _  ⟩
-                 (n ⁻¹ ∙ y ) ⁻¹  ≈⟨ ⁻¹-cong ( begin
-                    n ⁻¹ ∙ y ≈⟨ gsym (proj₂ identity _) ⟩
-                    (n ⁻¹ ∙ y) ∙  ε  ≈⟨  cdr (gsym (proj₂ inverse _)) ⟩
-                    (n ⁻¹ ∙ y) ∙  (n ∙ n ⁻¹)  ≈⟨  solve monoid ⟩
-                    n ⁻¹ ∙ (y ∙ n) ∙ n ⁻¹   ≈⟨ car (cdr ?) ⟩
-                    n ⁻¹ ∙ (x ∙ n) ∙ n ⁻¹   ≈⟨ ? ⟩
-                    n ⁻¹ ∙ x ∙ (n ∙ n ⁻¹)   ≈⟨ ? ⟩
-                    n ⁻¹ ∙ x ∙ ε   ≈⟨ ? ⟩
-                    n ⁻¹ ∙ x   ∎ ) ⟩
-                 ( n ⁻¹ ∙  x ) ⁻¹   ≈⟨ ? ⟩
-                 x ⁻¹ ∙ (n ⁻¹ ) ⁻¹   ≈⟨ ? ⟩
+          gk07 {a} (an n _ eq pn) = an ? _ ? ? where
+              gk01 : y ⁻¹ ∙ ?  ≈ a
+              gk01 = begin
+                 y ⁻¹ ∙ ?  ≈⟨ ? ⟩
+                 (?  ∙ y ) ⁻¹  ≈⟨ ?  ⟩
+                 (y ∙ ?  ) ⁻¹  ≈⟨ ?  ⟩
+                 (x ∙ conj (n ⁻¹) (x ⁻¹) ) ⁻¹  ≈⟨  ⁻¹-cong (gsym Na=aN )  ⟩
+                 (n ⁻¹ ∙ x ) ⁻¹  ≈⟨ ?  ⟩
+                 x ⁻¹ ∙ (n ⁻¹) ⁻¹   ≈⟨ ? ⟩
                  x ⁻¹ ∙ n  ≈⟨ eq ⟩
-                 a  ∎
+                 a ∎
           gk08 : {a : Carrier } →  IsaN N (y ⁻¹) a → IsaN N (x ⁻¹) a
           gk08 {a} (an n _ eq pn) = an n _ gk05 pn where
               gk05 :  x ⁻¹ ∙ n  ≈ a