# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1693879999 -32400
# Node ID 1e40a3ed74c221bba21249f31f0e899c457f4c1a
# Parent  c9fbb00962246e807987b7fcf28333189a9dccc3
...

diff -r c9fbb0096224 -r 1e40a3ed74c2 src/homomorphism.agda
--- a/src/homomorphism.agda	Tue Sep 05 08:56:07 2023 +0900
+++ b/src/homomorphism.agda	Tue Sep 05 11:13:19 2023 +0900
@@ -101,6 +101,17 @@
            (x ∙ ε ∙ n1) ∙ y  ∙ n2  ≈⟨ solve monoid ⟩
            (x ∙ n1) ∙ (y ∙ n2)  ≈⟨ ∙-cong eqa eqb ⟩
            a ∙ b  ∎
+    an-cong : {a b x : Carrier } → a ≈ b → IsaN N a x → IsaN N b x
+    an-cong {a} {b} {x} eq (an n _ eq1 pn) = an n _ an04 pn where
+        an04 : b ∙ n  ≈ x
+        an04 = begin
+           b ∙ n ≈⟨ car (gsym eq) ⟩
+           a ∙ n ≈⟨ eq1 ⟩
+           x ∎
+    aneq : {a b : Carrier } → a ≈ b → aNeq N a b
+    aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt }   
+    aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x)  →  naN ia ≈ naN ib
+    aNeq→n-eq eq = ?
 
 _/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
@@ -114,10 +125,10 @@
            ; trans = ntrans ; sym = λ a=b → nsym a=b 
           }
        ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v }
-       ; assoc = ? }
-       ; identity =  ?   }
-       ; inverse   =  (λ x → ? ) , (λ x → ? ) 
-       ; ⁻¹-cong   = ? 
+       ; assoc = gkassoc }
+       ; identity =  (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) )  }
+       ; inverse   =  (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) 
+       ; ⁻¹-cong   = gkcong⁻¹
       }
    } where
        _=n=_ = aNeq N
@@ -172,6 +183,53 @@
                  a ∙ (v ⁻¹ ∙ v)  ≈⟨ cdr ( proj₁ inverse _)  ⟩ 
                  a ∙ ε  ≈⟨ solve monoid  ⟩ 
                  a ∎
+       gkassoc : (x y z : Carrier ) → aNeq N ((x ∙ y ) ∙ z) (x ∙ (y ∙ z))
+       gkassoc x y z = record { eq→ = gk04 ; eq← =  gk06 }  where
+          gk04 : {a : Carrier } →  IsaN N (x ∙ y ∙ z) a → IsaN N (x ∙ (y ∙ z)) a
+          gk04 {a} (an n _ eq pn) = an n _ gk05 pn where
+              gk05 :  x ∙ (y ∙ z) ∙ n  ≈ a
+              gk05 = begin
+                 x ∙ (y ∙ z) ∙ n  ≈⟨ solve monoid ⟩
+                 x ∙ y ∙ z ∙ n  ≈⟨ eq ⟩
+                 a ∎
+          gk06 : {a : Carrier } →  IsaN N (x ∙ (y ∙ z)) a → IsaN N (x ∙ y ∙ z) a
+          gk06 {a} (an n _ eq pn) = an n _ gk05 pn where
+              gk05 :  x ∙ y ∙ z ∙ n  ≈ a
+              gk05 = begin
+                 x ∙ y ∙ z ∙ n  ≈⟨ solve monoid ⟩
+                 x ∙ (y ∙ z) ∙ n  ≈⟨ eq ⟩
+                 a ∎
+       gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) 
+       gkcong⁻¹ {x} {y} x=y  = record { eq→ = gk07 ; eq← =  gk08 }  where
+          gk07 : {a : Carrier } →  IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a
+          gk07 {a} (an n _ eq pn) = an n _ gk05 pn where
+              gk06 : x ∙ n ≈ a → y ∙ n ≈ a
+              gk06 eq with eq→ x=y (an n _ eq pn)
+              ... | an n1 .a eq1 pn = ?
+              gk05 :  y ⁻¹ ∙ n   ≈ a
+              gk05 = begin
+                 y ⁻¹ ∙ n   ≈⟨ cdr ( gsym  f⁻¹⁻¹≈f ) ⟩
+                 y ⁻¹ ∙ ( n ⁻¹ ) ⁻¹  ≈⟨ lemma5 _ _  ⟩
+                 (n ⁻¹ ∙ y ) ⁻¹  ≈⟨ ⁻¹-cong ( begin
+                    n ⁻¹ ∙ y ≈⟨ gsym (proj₂ identity _) ⟩
+                    (n ⁻¹ ∙ y) ∙  ε  ≈⟨  cdr (gsym (proj₂ inverse _)) ⟩
+                    (n ⁻¹ ∙ y) ∙  (n ∙ n ⁻¹)  ≈⟨  solve monoid ⟩
+                    n ⁻¹ ∙ (y ∙ n) ∙ n ⁻¹   ≈⟨ car (cdr ?) ⟩
+                    n ⁻¹ ∙ (x ∙ n) ∙ n ⁻¹   ≈⟨ ? ⟩
+                    n ⁻¹ ∙ x ∙ (n ∙ n ⁻¹)   ≈⟨ ? ⟩
+                    n ⁻¹ ∙ x ∙ ε   ≈⟨ ? ⟩
+                    n ⁻¹ ∙ x   ∎ ) ⟩
+                 ( n ⁻¹ ∙  x ) ⁻¹   ≈⟨ ? ⟩
+                 x ⁻¹ ∙ (n ⁻¹ ) ⁻¹   ≈⟨ ? ⟩
+                 x ⁻¹ ∙ n  ≈⟨ eq ⟩
+                 a  ∎
+          gk08 : {a : Carrier } →  IsaN N (y ⁻¹) a → IsaN N (x ⁻¹) a
+          gk08 {a} (an n _ eq pn) = an n _ gk05 pn where
+              gk05 :  x ⁻¹ ∙ n  ≈ a
+              gk05 = begin
+                 x ⁻¹ ∙ n  ≈⟨ ? ⟩
+                 y ⁻¹ ∙ n  ≈⟨ eq ⟩
+                 a ∎
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H )