--- a/src/Fundamental.agda	Tue May 31 09:49:12 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 11:18:05 2022 +0900
@@ -59,6 +59,7 @@
 base {G} {K} x = base1 (x ε) where     -- with x ε won't work why?
     open Group G
 
+
 --  Na ∙ Nb = Nab
 mul : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → (g : Group.Carrier G ) → Coset G K g
 mul {G} {K} x y g = φ (base x ∙ base y) g where open Group G
@@ -99,13 +100,25 @@
       open Group G hiding (refl ; sym ; trans )
       open EqReasoning (Algebra.Group.setoid G)
       open IsGroupHomomorphism (s-homo K )
-      mbase :  {x y : COSET G K} → base (mul x y) ≈ sub K (base x ∙ base y)
+      idem-base :  {x : COSET G K} → sub K (sub K (base x))  ≈ sub K (base x )
+      idem-base {x} = ib01 (x ε) where
+         ib01 :  {a : Carrier } → (t : Coset G K a ) → sub K (sub K (base1 t))  ≈ sub K (base1 t )
+         ib01 {y} (coset a b) = begin
+             sub K (sub K (base1 {G} {K} (coset a b))) ≈⟨ {!!} ⟩
+             sub K (sub K (a ⁻¹ ∙ b))  ≈⟨ {!!} ⟩
+             sub K (a ⁻¹ ∙ b)  ≈⟨ {!!} ⟩
+             sub K (base1 {G} {K} (coset a b)) ∎
+         ib01 (cscong x t) = ib01 t  
+      mbase :  {x y : COSET G K} → sub K (base (mul x y)) ≈ sub K (base x ∙ base y)
       mbase {x} {y} = mbase1 (x ε) (y ε) where
-         mbase1 : {a b : Carrier } → Coset G K a → Coset G K b → base (mul x y) ≈ sub K (base x ∙ base y)
+         mbase1 : {a b : Carrier } → Coset G K a → Coset G K b → sub K (base (mul x y)) ≈ sub K (base x ∙ base y)
          mbase1 (coset a b) (coset a₁ b₁) = begin
-             (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
-             (sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
-             (sub K (base1 (x ε) ∙ base1 (y ε))) ∙ (base1 (x ε) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
+             sub K ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩
+             sub K ((sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩
+             sub K ((sub K (base1 (x ε) ∙ base1 (y ε))) ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩
+             sub K (sub K (base1 (x ε)) ∙ sub K (base1 (y ε)) ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩
+             sub K (sub K (base1 (x ε)) ∙ base1 (x ε) ∙ sub K (base1 (y ε)) ∙ base1 (y ε)) ≈⟨ {!!} ⟩
+             sub K (base1 (x ε)) ∙ sub K (base1 (y ε))  ≈⟨ {!!} ⟩
              sub K (base1 (x ε) ∙ base1 (y ε)) ∎
          mbase1 (coset a b) (cscong x t) = mbase1 (coset a b) t
          mbase1 (cscong eq s) (coset a b) = mbase1 s (coset a b)