# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1653967627 -32400
# Node ID 864afb582fc706886215096682e5634b2b705041
# Parent  e6f9eb2bfc78377b184a76348d5e0a1b491cdc86
...

diff -r e6f9eb2bfc78 -r 864afb582fc7 src/Fundamental.agda
--- a/src/Fundamental.agda	Tue May 31 11:18:05 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 12:27:07 2022 +0900
@@ -52,7 +52,7 @@
          x   ∎ where open EqReasoning (Algebra.Group.setoid G )
 
 base1 : {G : Group c l}  {K : NormalSubGroup G} → {x : Group.Carrier G } → Coset G K x → Group.Carrier  G
-base1 {G} (coset a b) = a ⁻¹ ∙ b where open Group G
+base1 {G} {K} {x} (coset a b) = a ⁻¹ ∙ x where open Group G   -- x ≡ a ∙ sub K b
 base1 (cscong x y) = base1 y
 
 base :  {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → Group.Carrier G
@@ -100,32 +100,30 @@
       open Group G hiding (refl ; sym ; trans )
       open EqReasoning (Algebra.Group.setoid G)
       open IsGroupHomomorphism (s-homo K )
-      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 → sub K (base (mul x y)) ≈ sub K (base x ∙ base y)
-         mbase1 (coset a b) (coset a₁ b₁) = begin
-             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)
-         mbase1 (cscong eqs s) (cscong eqt t) = mbase1 s t
+      mbase {x} {y} = begin
+              sub K ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙
+                        (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ ∙
+                         sub K (base1 (x ε) ∙ base1 (y ε)))) ≈⟨  {!!}   ⟩
+              sub K ( ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙
+                        (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ )) ∙
+                         (base1 (x ε) ∙ base1 (y ε))) ≈⟨  ⟦⟧-cong ( ∙-cong (
+                     begin (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
+                     sub K ((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
+                     sub K (((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩
+                     sub K ε ≈⟨ {!!} ⟩
+                     ε  ∎ ) (grefl G) ) ⟩
+                  sub K (ε ∙ (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε)))  ≈⟨ {!!} ⟩
+                  sub K (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε)) ∎
       cresp : {x y u v : COSET G K} → sub K (base x) ≈ sub K (base y) → sub K (base u )≈ sub K (base v)
          → sub K (base (mul x u)) ≈ sub K (base (mul y v))
-      cresp {x} {y} {u} {v} x=y u=v = {!!}
+      cresp {x} {y} {u} {v} x=y u=v =  begin
+          sub K (base (mul x u)) ≈⟨ {!!} ⟩
+          sub K (base x ∙ base u) ≈⟨ {!!} ⟩
+          sub K (base x ) ∙ sub K (base u) ≈⟨ {!!} ⟩
+          sub K (base y ) ∙ sub K (base v) ≈⟨ {!!} ⟩
+          sub K (base y ∙ base v) ≈⟨ {!!} ⟩
+          sub K (base (mul y v))  ∎ 
       assoc1 : (x y z  : COSET G K) → sub K (base (mul (mul x y ) z)) ≈ sub K (base (mul x ( mul y z ) ))
       assoc1 x y z =  {!!} where
         -- crefl1 (coset a b) = ⟦⟧-cong (grefl G)