--- a/src/Fundamental.agda	Thu Jan 26 11:31:58 2023 +0900
+++ b/src/Fundamental.agda	Fri Jan 27 10:45:25 2023 +0900
@@ -40,6 +40,9 @@
 _<_∙_> :  (m : Group c c )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
 m < x ∙ y > =  Group._∙_ m x y
 
+_<_≈_> :  (m : Group c c )  →    (f  g : Group.Carrier m ) → Set c 
+m < x ≈ y > =  Group._≈_ m x y
+
 infixr 9 _<_∙_>
 
 --
@@ -163,8 +166,41 @@
            φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ 
            φ-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-φ f ≡ a (f ε)  -- not af ≡ a (f x)
+    --  φ (inv-φ f)  returns ( λ x → record { a = a (f ε) ; n = factor x (a (f ε)) ; is-factor x (a (f ε)) )
+    --          it should be ( λ x → record { a =      af ; n = factor x af        ; is-factor x af
+    --          it should be ( λ x → record { a =      af ; n = fn                 ; is-factor x af
+    --      ⟦ n (φ (inv-φ f) x)  ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧
+    --      ⟦ factor x (a (f ε)) ⟧ ≈ ⟦ n (f x) ⟧ ≈ ⟦ fn ⟧ ≈ ⟦ factor x g ⟧ 
+    --      g ∙ ⟦ factor y (a (f ε)) ⟧ ≈ x 
+    --            factor x g
+    --      g ∙ ⟦ factor y g ⟧ ≈ y 
+
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f = ⟦ n (f ε) ⟧ 
+    inv-φ f = a (f ε)
+
+    _∋_ : (f : Group.Carrier (G / K)) (x : Carrier ) → Set c
+    _∋_  f x = a (f x) ∙ ⟦ n (f x) ⟧ ≈ x  
+
+    aNeq : {f g : Group.Carrier (G / K)} →  (G / K)  < f ≈ g >
+       →  ( {x : Carrier  } → f ∋  x → g ∋ x ) × ( {x : Carrier  } → g ∋  x → f ∋ x )
+    aNeq {f} {g} f=g = an00 , ? where 
+        an00 : {x : Carrier} → f ∋ x → g ∋ x
+        an00 {x} fnx = begin
+           a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym G (an01 (a (f x)))) (grefl G) ⟩
+           (a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ∙ ⟦ n (g x) ⟧ ≈⟨ ? ⟩
+           a (f x) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ ? ⟩
+           a (f x) ∙ ( ⟦ factor (a (g x)) (a (f x)) ∙ n (g x) ⟧ ) ≈⟨ ? ⟩
+           a (f x) ∙ ⟦ n (f x) ⟧ ≈⟨ fnx ⟩
+           x ∎  where
+               an01 : (y : Carrier) → y ∙ ⟦ factor (a (g x)) y ⟧ ≈ a (g x)
+               an01 y = is-factor (a (g x)) y
 
     cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g
     cong-i = ?
@@ -174,8 +210,10 @@
     ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin
        ⟦ factor y z ⟧ ≈⟨ ? ⟩ 
        z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ 
-       z ⁻¹ ∙ y  ≈⟨ ? ⟩ 
-       z ⁻¹ ∙ fa ∙ ⟦ fn ⟧   ≈⟨ ? ⟩ 
+       z ⁻¹ ∙ y  ≈⟨ ∙-cong (grefl G) (gsym G faN=x )  ⟩ 
+       z ⁻¹ ∙ ( fa  ∙ ⟦ fn ⟧ )  ≈⟨ ? ⟩ 
+       (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧   ≈⟨ ? ⟩ 
+       ε ∙ ⟦ fn ⟧   ≈⟨ solve monoid ⟩ 
        ⟦ fn ⟧ ∎ where
           z = fa ⁻¹
 
@@ -193,10 +231,10 @@
     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 (φ ⟦ n (f ε) ⟧  y) ⟧  ≈⟨ grefl G ⟩
-       ⟦ factor y ⟦ n (f ε) ⟧ ⟧  ≈⟨ ? ⟩
-       ⟦ factor y afn' ⟧  ≈⟨ factor=nf f ⟩
-       ⟦ n (f y) ⟧ ∎ where
+       ⟦ n (φ (a (f ε)) y) ⟧  ≈⟨ grefl G ⟩
+       ⟦ factor y (a (f ε))  ⟧  ≈⟨ ? ⟩                 --  a (f ε) ∙ ⟦ factor y ( a (f ε)) ⟧ ≈ y 
+       ⟦ factor y ((a (f y)) ⁻¹) ⟧  ≈⟨ factor=nf f ⟩   --  a (f y) ∙ ⟦ factor y ( a (f y)) ⟧ ≈ y 
+       ⟦ n (f y) ⟧ ∎ where                             --  a (f y) ∙ ⟦ n (f y) ⟧ ≈ y 
            afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
            afn = aN=x (f ε)
            afn' = (a (f y)) ⁻¹