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

diff -r 864afb582fc7 -r 86408a621c6e src/Fundamental.agda
--- a/src/Fundamental.agda	Tue May 31 12:27:07 2022 +0900
+++ b/src/Fundamental.agda	Tue May 31 12:42:57 2022 +0900
@@ -125,7 +125,7 @@
           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
+      assoc1 x y z =  {!!} 
         -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) 
 
 -- K ⊂ ker(f)
@@ -139,9 +139,9 @@
     (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔  l ) where
   open Group H
   field
-    h : {!!} → Group.Carrier H
-    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
-    unique : (x : Group.Carrier G)  →  {!!} -- f x ≈ h ( φ x )
+    h : COSET G K → Group.Carrier H
+    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
+    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
 
 FundamentalHomomorphismTheorm : (G H : Group c l)
     (f : Group.Carrier G → Group.Carrier H )
@@ -159,10 +159,11 @@
              (IsGroup.isMonoid (Group.isGroup G) )))
     h1 : {x : Group.Carrier G } → Coset G K x → Carrier
     h1 (coset a b) = f a 
-    h : {!!} -- CosetCarrier G K → Carrier   --  G / K → H
-    h r = {!!}
+    h1 (cscong a b) = h1 b
+    h : COSET G K → Carrier   --  G / K → H
+    h r = h1 {Group.ε G} (r (Group.ε G))
     _o_ = Group._∙_ G
-    h03 : (x y : Group.Carrier (G / K ) ) → {!!}
+    h03 : (x y : Group.Carrier (G / K ) ) →  h ( mul x y ) ≈ h x ∙ h y
     h03 x y = {!!} 
     h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
     h-homo = record {
@@ -175,7 +176,8 @@
     unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
     unique x = begin
          f x ≈⟨ {!!} ⟩
-         f ( x o (Group._⁻¹ G (sub K x)))   ∎ where open EqReasoning (Algebra.Group.setoid H )
+         f ((G Group.∙ Group.ε G) ((G Group.⁻¹) (sub K x))) ≈⟨ grefl H  ⟩
+         h1 {Group.ε G} ((φ x) (Group.ε G))  ∎ where open EqReasoning (Algebra.Group.setoid H )