# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674965394 -32400
# Node ID 515de7624a0c1cb523b00656d7e300213ef724e0
# Parent  69645d667f45f2ccea13572d5cb4b4ef83501b8c
...

diff -r 69645d667f45 -r 515de7624a0c src/FundamentalHomorphism.agda
--- a/src/FundamentalHomorphism.agda	Sun Jan 29 11:40:29 2023 +0900
+++ b/src/FundamentalHomorphism.agda	Sun Jan 29 13:09:54 2023 +0900
@@ -52,9 +52,8 @@
 
 open GroupMorphisms
 
-import Axiom.Extensionality.Propositional
-postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
-open import Tactic.MonoidSolver using (solve; solve-macro)
+-- import Axiom.Extensionality.Propositional
+-- postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 
 
 record NormalSubGroup (A : Group c c )  : Set c  where
@@ -73,25 +72,21 @@
     open Group A
     open NormalSubGroup N
     field
-        a : Group.Carrier A
+        a : Carrier 
         aN=x :  a ∙ ⟦ n ⟧ ≈ x
 
 record aN {A : Group c c }  (N : NormalSubGroup A )  : Set c where
+    open Group A
     field
-        n : Group.Carrier A
-        is-an : (x : Group.Carrier A) → an N n x
-
-qid : {A : Group c c }  (N : NormalSubGroup A )  → aN N
-qid {A} N = record { n = ε ; is-an = λ x → record { a = x ; aN=x = ? } } where
-       open Group A
-       open NormalSubGroup N
+        n : Carrier 
+        is-an : (x : Carrier) → an N n x
 
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
     Carrier  = aN N
     ; _≈_      = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
     ; _∙_      = qadd
-    ; ε        = qid N
+    ; ε        = qid 
     ; _⁻¹      = ?
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
        isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
@@ -119,10 +114,19 @@
               x ⁻¹ ∙  (a (is-an f x) ∙ ( a (is-an g x) ∙  ⟦ n f ⟧)  ∙ ⟦ n g ⟧)  ≈⟨ ? ⟩
               x ⁻¹ ∙  (a (is-an f x) ∙ ( ⟦ n f ⟧ ∙ a (is-an g x) )  ∙ ⟦ n g ⟧)  ≈⟨ ? ⟩
               x ⁻¹ ∙  ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x)   ∙ ⟦ n g ⟧))  ≈⟨ ? ⟩
-              x ⁻¹ ∙  ((a (is-an f x) ∙ ⟦ n f ⟧ ) ∙ ( a (is-an g x)   ∙ ⟦ n g ⟧))  ≈⟨ ? ⟩
               x ⁻¹ ∙  (x ∙ x)  ≈⟨ ? ⟩
+              (x ⁻¹ ∙  x ) ∙ x  ≈⟨ ? ⟩
+              ε ∙ x  ≈⟨ ? ⟩
+              x ∎
+       qid :  aN N
+       qid = record { n = ε ; is-an = λ x → record { a = x ; aN=x = qid1 } } where
+           qid1 : {x : Carrier } →  x ∙ ⟦ ε ⟧ ≈ x
+           qid1 {x} = begin
+             x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong grefl ε-homo ⟩
+             x ∙ ε  ≈⟨ proj₂ identity _ ⟩
              x ∎
 
+
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c c)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
 K⊆ker G H K f = (x : Group.Carrier G ) → f ( ⟦ x ⟧ ) ≈ ε   where
@@ -171,6 +175,7 @@
        ⟦ n (φ (inv-φ f) ) ⟧  ≈⟨ grefl  ⟩
        ⟦ n (φ (⟦ n f  ⟧ ⁻¹) ) ⟧  ≈⟨ grefl  ⟩
        ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
+       ε ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
        ( ⟦ n f ⟧ ∙ ⟦ n f  ⟧ ⁻¹) ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
        ⟦ n f ⟧ ∙ ( ⟦ n f  ⟧ ⁻¹ ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
        ⟦ n f ⟧ ∙ ε  ≈⟨ ? ⟩
@@ -182,8 +187,9 @@
     gk00 : {x : Carrier } → ⟦ factor ε x ⟧ ⁻¹ ≈ x
     gk00 {x} = begin
         ⟦ factor ε x ⟧ ⁻¹ ≈⟨ ? ⟩ 
-        ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ? ⟩ 
-        ( x ⁻¹ ∙ ( x ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x))  ⟩ 
+        (ε ∙ ⟦ factor ε x ⟧)  ⁻¹ ≈⟨ ? ⟩ 
+        ( ( x ⁻¹ ∙   x ) ∙ ⟦ factor ε x ⟧ ) ⁻¹ ≈⟨ ? ⟩ 
+        ( x ⁻¹ ∙ ( x   ∙ ⟦ factor ε x ⟧) ) ⁻¹ ≈⟨ ⁻¹-cong (∙-cong grefl (is-factor ε x))  ⟩ 
         ( x ⁻¹ ∙ ε ) ⁻¹ ≈⟨ ? ⟩ 
         ( x ⁻¹  ) ⁻¹ ≈⟨ ? ⟩ 
         x ∎