# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674956829 -32400
# Node ID b70cc2534d2fd0bf907c934b7ce889946db8a49b
# Parent  803f909fdd174e03b77260be3eee33f42a9ddfae
double record on quontient group

diff -r 803f909fdd17 -r b70cc2534d2f src/Fundamental.agda
--- a/src/Fundamental.agda	Sun Jan 29 08:19:19 2023 +0900
+++ b/src/Fundamental.agda	Sun Jan 29 10:47:09 2023 +0900
@@ -11,13 +11,13 @@
 open import Algebra.Bundles
 
 open import Data.Product
-open import Relation.Binary.PropositionalEquality 
+open import Relation.Binary.PropositionalEquality
 open import Gutil0
 import Gutil
 import Function.Definitions as FunctionDefinitions
 
 import Algebra.Morphism.Definitions as MorphismDefinitions
-open import Algebra.Morphism.Structures 
+open import Algebra.Morphism.Structures
 
 open import Tactic.MonoidSolver using (solve; solve-macro)
 
@@ -41,7 +41,7 @@
 _<_∙_> :  (m : Group c c )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
 m < x ∙ y > =  Group._∙_ m x y
 
-_<_≈_> :  (m : Group c c )  →    (f  g : Group.Carrier m ) → Set c 
+_<_≈_> :  (m : Group c c )  →    (f  g : Group.Carrier m ) → Set c
 m < x ≈ y > =  Group._≈_ m x y
 
 infixr 9 _<_∙_>
@@ -59,85 +59,69 @@
 
 record NormalSubGroup (A : Group c c )  : Set c  where
    open Group A
-   field  
-       ⟦_⟧ : Group.Carrier A → Group.Carrier A 
+   field
+       ⟦_⟧ : Group.Carrier A → Group.Carrier A
        normal :  IsGroupHomomorphism (GR A) (GR A)  ⟦_⟧
-       comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b 
-       -- 
+       comm : {a b :  Carrier } → b ∙ ⟦ a ⟧  ≈ ⟦ a ⟧  ∙ b
+       --
        factor : (a b : Carrier) → Carrier
        is-factor : (a b : Carrier) →  b ∙ ⟦ factor a b ⟧ ≈ a
 
 -- Set of a ∙ ∃ n ∈ N
 --
-record aN {A : Group c c }  (N : NormalSubGroup A ) (x : Group.Carrier A  ) : Set c where 
+record an {A : Group c c }  (N : NormalSubGroup A ) (n x : Group.Carrier A  ) : Set c where
     open Group A
     open NormalSubGroup N
-    field 
-        a n : Group.Carrier A 
+    field
+        a : Group.Carrier A
         aN=x :  a ∙ ⟦ n ⟧ ≈ x
 
+record aN {A : Group c c }  (N : NormalSubGroup A )  : Set c where
+    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
+
 _/_ : (A : Group c c ) (N  : NormalSubGroup A ) → Group c c
 _/_ A N  = record {
-    Carrier  = (x : Group.Carrier A) → aN N x
-    ; _≈_      = _=n=_
-    ; _∙_      = qadd 
-    ; ε        = qid
-    ; _⁻¹      = qinv
+    Carrier  = aN N
+    ; _≈_      = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
+    ; _∙_      = qadd
+    ; ε        = qid N
+    ; _⁻¹      = ?
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record {refl = ? ; trans = ? ; sym = ? }
-       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v {w} → qcong {x} {y} {u} {v} x=y u=v {w} }
+       isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
+       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
        ; assoc = ? }
-       ; identity =  idL , (λ q → ? )  }
-       ; inverse   = ( (λ x → ? ) , (λ x → ? ))  
+       ; identity =  ? , (λ q → ? )  }
+       ; inverse   = ( (λ x → ? ) , (λ x → ? ))
        ; ⁻¹-cong   = λ i=j → ?
       }
    } where
        open Group A
        open aN
+       open an
        open NormalSubGroup N
-       open IsGroupHomomorphism normal 
+       open IsGroupHomomorphism normal
        open EqReasoning (Algebra.Group.setoid A)
        open Gutil A
-       _=n=_ : (f g : (x : Group.Carrier A  )  → aN N x ) →  Set c
-       f =n= g = {x y : Group.Carrier A  } → ⟦ n (f x) ⟧  ≈ ⟦ n (g y) ⟧  
-       qadd : (f g : (x : Group.Carrier A  )  → aN N x ) → (x : Group.Carrier A  )  → aN N x
-       qadd f g x = record { a = x ⁻¹ ∙ a (f x) ∙ a (g x) ; n = n (f x) ∙ n (g x) ; aN=x = q00 } where
-           q00 : ( x ⁻¹ ∙  a (f x) ∙ a (g x)  ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈ x
-           q00 = begin 
-              ( x ⁻¹ ∙ a (f x) ∙ a (g x) ) ∙ ⟦ n (f x) ∙ n (g x) ⟧  ≈⟨ ∙-cong (assoc _ _ _) (homo _ _ ) ⟩
-              x ⁻¹ ∙ (a (f x) ∙ a (g x) ) ∙ ( ⟦ n (f x) ⟧  ∙ ⟦ n (g x) ⟧ ) ≈⟨ solve monoid ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ((a (g x)  ∙ ⟦ n (f x) ⟧ ) ∙ ⟦ n (g x) ⟧ )) ≈⟨ ∙-cong (grefl ) (∙-cong (grefl ) (∙-cong comm (grefl ) ))  ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ((⟦ n (f x) ⟧  ∙ a (g x)) ∙ ⟦ n (g x) ⟧ ))  ≈⟨ solve monoid ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ (a (g x) ∙ ⟦ n (g x) ⟧ )  ≈⟨ ∙-cong (grefl ) (aN=x (g x)  ) ⟩
-              x ⁻¹ ∙ (a (f x) ∙ ⟦ n (f x) ⟧ ) ∙ x   ≈⟨ ∙-cong (∙-cong (grefl ) (aN=x (f x))) (grefl )  ⟩
-              (x ⁻¹ ∙ x ) ∙ x   ≈⟨ ∙-cong (proj₁ inverse _ ) (grefl )  ⟩
-              ε ∙ x  ≈⟨ solve monoid  ⟩
-              x ∎ 
-       qid : ( x : Carrier ) → aN N x
-       qid x = record { a = x  ; n = ε  ; aN=x = qid1 } where
-           qid1 : x ∙ ⟦ ε ⟧ ≈ x
-           qid1 = begin
-              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
-              x ∙ ε  ≈⟨ solve monoid ⟩
-              x ∎ 
-       qinv : (( x : Carrier ) → aN N x) → ( x : Carrier ) → aN N x
-       qinv f x = record { a = x ∙ ⟦ n (f x) ⟧  ⁻¹  ; n = n (f x)  ; aN=x = qinv1  } where
-             qinv1 : x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈ x
-             qinv1 = begin
-              x ∙ ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
-              x ∙ ⟦ (n (f x)) ⁻¹ ⟧  ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩
-              x ∙ ⟦ ((n (f x)) ⁻¹ )  ∙ n (f x) ⟧ ≈⟨ ? ⟩
-              x ∙ ⟦ ε ⟧ ≈⟨ ∙-cong (grefl ) ε-homo ⟩
-              x ∙ ε  ≈⟨ solve monoid ⟩
-              x ∎ 
-       qcong :  { x y u v : (x₁ : Carrier) → aN N x₁ } → (x=y : x =n= y) ( u=v : u =n= v ) →  qadd x u =n= qadd y v
-       qcong {x} {y} {u} {v} x=y u=v {w} {z} = begin
-              ⟦ n (x w) ∙ n (u w) ⟧  ≈⟨ homo _ _ ⟩
-              ⟦ n (x w) ⟧ ∙ ⟦ n (u w) ⟧  ≈⟨ ∙-cong x=y u=v ⟩
-              ⟦ n (y z) ⟧ ∙ ⟦ n (v z) ⟧  ≈⟨ gsym (homo _ _ )  ⟩
-              ⟦ n (y z) ∙ n (v z) ⟧    ∎ 
-       idL : (f : (x  : Carrier )→  aN N x) → (qadd qid f ) =n= f 
-       idL f = ?
+       qadd : (f g : aN N) → aN N
+       qadd f g = record { n = n f ∙ n g  ; is-an = λ x → record { a = x ⁻¹ ∙ ( a (is-an f x) ∙ a (is-an g x))  ; aN=x = qadd0 }  } where
+           qadd0 : {x : Carrier} →   x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈ x
+           qadd0 {x} = begin
+              x ⁻¹ ∙ (a (is-an f x) ∙ a (is-an g x)) ∙ ⟦ n f ∙ n g ⟧ ≈⟨ ? ⟩
+              x ⁻¹ ∙  (a (is-an f x) ∙ a (is-an g x) ∙ ⟦ n f ∙ n g ⟧) ≈⟨ ? ⟩
+              x ⁻¹ ∙  (a (is-an f x) ∙ a (is-an g x) ∙ ( ⟦ n f ⟧  ∙ ⟦ n g ⟧ )) ≈⟨ ? ⟩
+              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 ∎
 
 -- K ⊂ ker(f)
 K⊆ker : (G H : Group c c)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set c
@@ -151,21 +135,22 @@
 module _ (G : Group c c) (K : NormalSubGroup G) where
     open Group G
     open aN
+    open an
     open NormalSubGroup K
-    open IsGroupHomomorphism normal 
+    open IsGroupHomomorphism normal
     open EqReasoning (Algebra.Group.setoid G)
     open Gutil G
 
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g x = record { a = g  ; n = factor x g ; aN=x = is-factor x g  } 
+    φ g = record { n = factor ε g ; is-an = λ x → record { a = x ∙ ( ⟦ factor ε g ⟧ ⁻¹)   ; aN=x = ?  } }
 
-    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ 
+    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
     φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
        record { cong = ? } }}}
 
     φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
     φe = record { _⟨$⟩_ = φ ; cong = ?  }  where
-           φ-cong : {f g : Carrier } → f ≈ g  → {x : Carrier } →  ⟦ n (φ f x ) ⟧ ≈ ⟦ n (φ g x ) ⟧ 
+           φ-cong : {f g : Carrier } → f ≈ g  → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧
            φ-cong = ?
 
     -- inverse ofφ
@@ -175,158 +160,35 @@
     --           f x → φ (inv-φ f) (h1 x)
 
     inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f = ⟦ n (f ε) ⟧ ⁻¹ 
-
-    an02 : (f : Group.Carrier (G / K)) → {x : Carrier } → a (f x) ≈ x ∙ ⟦ n (f x) ⟧ ⁻¹
-    an02 f {x} = begin
-        a (f x ) ≈⟨ gsym  ( proj₂ identity _) ⟩
-        a (f x ) ∙ ε  ≈⟨ ∙-cong (grefl ) (gsym  (proj₂ inverse _)) ⟩
-        a (f x ) ∙ ( ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹)  ≈⟨ solve monoid ⟩
-        (a (f x ) ∙  ⟦ n (f x) ⟧) ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ ∙-cong (aN=x (f x)) (grefl ) ⟩
-        x ∙ ⟦ n (f x) ⟧ ⁻¹ ∎
+    inv-φ f = ⟦ n f ⟧ ⁻¹
 
-    aNeqε : {f g : Group.Carrier (G / K)} →  (G / K)  < f ≈ g >
-       →  {x : Carrier } → ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
-    aNeqε {f} {g} f=g {x} = begin
-           ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
-          ε ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈⟨ ? ⟩
-          (a (f x)  ⁻¹ ∙  a (f x)) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧   ≈⟨ solve monoid ⟩
-           a (f x)  ⁻¹ ∙ (a (f x)  ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ≈⟨ ? ⟩
-           a (f x)  ⁻¹ ∙ a (g x) ≈⟨ ∙-cong (⁻¹-cong (an02 f) )  (an02 g) ⟩
-           (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x  ∙ ⟦ n (g x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
-           (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ⁻¹ ∙ (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
-           ( ⟦ n (f x) ⟧ ∙  x ⁻¹ ) ∙ (x  ∙ ⟦ n (f x) ⟧ ⁻¹ ) ≈⟨ ? ⟩
-           ⟦ n (f x) ⟧ ∙  ( x ⁻¹  ∙ x ) ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ ? ⟩
-           ⟦ n (f x) ⟧ ∙  ε ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ solve monoid ⟩
-           ⟦ n (f x) ⟧ ∙ ⟦ n (f x) ⟧ ⁻¹  ≈⟨ proj₂ inverse _ ⟩
-           ε ∎  where
-               an01 : a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ a (g x)
-               an01 = is-factor (a (g x)) (a (f x))
-               an03 : {f : Group.Carrier (G / K)} → {x : Carrier } → a (f x) ⁻¹ ≈ x ∙ ⟦ n (f x) ⟧ 
-               an03 = ?
 
-    cong-i : {f g : Group.Carrier (G / K ) } → ({x y : Carrier } →  ⟦ n (f x) ⟧ ≈ ⟦ n (g y) ⟧ ) → inv-φ f ≈ inv-φ g
+    cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
     cong-i = ?
 
-    factor=nf : (f : (x : Carrier) → aN K x ) {y : Carrier} → ⟦ factor y ((a (f y)) ⁻¹ ) ⟧ ≈ ⟦ n (f y) ⟧
-    factor=nf f {y} with f y
-    ... | record { a = fa ; n = fn ; aN=x = faN=x } = begin
-       ⟦ factor y z ⟧ ≈⟨ ? ⟩ 
-       z ⁻¹ ∙ ( z ∙ ⟦ factor y z ⟧ ) ≈⟨ ? ⟩ 
-       z ⁻¹ ∙ y  ≈⟨ ∙-cong (grefl ) (gsym  faN=x )  ⟩ 
-       z ⁻¹ ∙ ( fa  ∙ ⟦ fn ⟧ )  ≈⟨ ? ⟩ 
-       (z ⁻¹ ∙ fa ) ∙ ⟦ fn ⟧   ≈⟨ ? ⟩ 
-       ε ∙ ⟦ fn ⟧   ≈⟨ solve monoid ⟩ 
-       ⟦ fn ⟧ ∎ where
-          z = fa ⁻¹
-
-    φ-factor : (f : Group.Carrier ( G / K )) → {x y : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (f y) ⟧
-    φ-factor f {x} {y} = begin
-       ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
-       ⟦ n (f x) ⟧ ∙ ε ≈⟨ ? ⟩ 
-       ⟦ n (f x) ⟧ ∙ (  ⟦ n (f y) ⟧  ∙  ⟦ n (f y) ⟧  ⁻¹ ) ≈⟨ cdr ( cdr an07 )  ⟩ 
-       ⟦ n (f x) ⟧ ∙ ( ⟦ n (f y) ⟧  ∙  (  ⟦ n (f x) ⟧ ⁻¹  ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹)  (⟦ n (f x) ⟧ ⁻¹)  ⟧  )) ≈⟨ ? ⟩ 
-       ⟦ n (f y) ⟧ ∙ ⟦ factor (⟦ n (f y) ⟧ ⁻¹)  (⟦ n (f x) ⟧ ⁻¹)  ⟧  ≈⟨ ? ⟩ 
-       ⟦ n (f y) ⟧ ∙ ⟦ factor (a (f y) ∙ y ⁻¹)  (a (f x) ∙ x ⁻¹)  ⟧  ≈⟨ ? ⟩ 
-       ⟦ n (f y) ⟧ ∙ ε  ≈⟨ ? ⟩ 
-       ⟦ n (f y) ⟧ ∎ where
-          fxy =  ⟦ n (f x) ⟧ ⁻¹ ∙ ⟦ n (f y) ⟧ 
-
-          fa11 : a (f (x ∙ y  ⁻¹  )) ∙ ⟦ n (f (x ∙ y ⁻¹)) ⟧  ≈ x ∙ y  ⁻¹
-          fa11 = aN=x ( f ( x ∙ y  ⁻¹ ))
-
-          fa21 : a (f ε) ∙ ⟦ n (f ε) ⟧  ≈ ε
-          fa21 = aN=x ( f ε)
-
-          fa22 : {x : Carrier } → a (f (x ⁻¹)) ∙ ⟦ n (f (x ⁻¹)) ⟧  ≈ x ⁻¹
-          fa22 {x} = aN=x ( f (x ⁻¹))
-
-          fa14 : a (f x) ∙ ⟦ n (f x) ⟧ ≈ x
-          fa14 = aN=x ( f x)
-
-          fa13 : a (f y) ∙ ⟦ n (f y) ⟧ ≈ y
-          fa13 = aN=x ( f y)
+    is-inverse : (f : aN K  ) →  ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
+    is-inverse f = begin
+       ⟦ n (φ (inv-φ f) ) ⟧  ≈⟨ grefl  ⟩
+       ⟦ n (φ (⟦ n f  ⟧ ⁻¹) ) ⟧  ≈⟨ grefl  ⟩
+       ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
+       ( ⟦ n f ⟧ ∙ ⟦ n f  ⟧ ⁻¹) ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩
+       ⟦ n f ⟧ ∙ ( ⟦ n f  ⟧ ⁻¹ ∙  ⟦ factor ε (⟦ n f  ⟧ ⁻¹) ⟧ ) ≈⟨ ∙-cong grefl (is-factor ε _ ) ⟩
+       ⟦ n f ⟧ ∙ ε  ≈⟨ ? ⟩
+       ⟦ n f ⟧ ∎
 
-          fa12 : aN K ( x ∙ y  ⁻¹ )
-          fa12 = f (x ∙ y  ⁻¹  ) 
-          an01 : (y : Carrier) → y ∙ ⟦ factor (a (f x)) y ⟧ ≈ a (f x)
-          an01 y = is-factor (a (f x)) y
-          an04 : a (f y) ∙ ⟦ factor (a (f x)) (a (f y)) ⟧ ≈ a (f x)
-          an04 = is-factor (a (f x)) (a (f y))
-          an07 : {z w : Carrier} → z ≈ w ∙ ⟦ factor z w ⟧
-          an07 {z} {w} = gsym ( is-factor z w )
-          an10 :  ⟦ factor (a (f y) ∙ y ⁻¹)  (a (f x) ∙ x ⁻¹)  ⟧  ≈ ε
-          an10 = begin
-               ⟦ factor (a (f y) ∙ y ⁻¹)  (a (f x) ∙ x ⁻¹)  ⟧  ≈⟨ ? ⟩ 
-               ( a (f x) ∙ x ⁻¹ ) ⁻¹ ∙  (a (f y) ∙ y ⁻¹)   ≈⟨ ? ⟩ 
-               x ∙ a (f x) ⁻¹ ∙  a (f y) ∙ y ⁻¹   ≈⟨ ? ⟩ 
-               ε ∎
-          an08 : ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈ ε 
-          an08 = begin 
-              ⟦ n (f y) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ 
-              ε ∎ 
-          an05 : {z : Carrier} → ⟦ n (f z) ⟧ ≈ ⟦ factor z (a (f z)) ⟧
-          an05 {z} = begin
-              ⟦ n (f z) ⟧ ≈⟨ ? ⟩
-              ((a (f z) ⁻¹) ∙ a (f z)) ∙ ⟦ n (f z) ⟧  ≈⟨ ? ⟩
-              (a (f z) ⁻¹) ∙ ( a (f z) ∙ ⟦ n (f z) ⟧)  ≈⟨ ∙-cong grefl (aN=x (f z)) ⟩
-              (a (f z) ⁻¹) ∙ z ≈⟨ ∙-cong grefl ( gsym ( is-factor z (a (f z))))  ⟩
-              (a (f z) ⁻¹) ∙ (a (f z)  ∙ ⟦ factor z (a (f z))  ⟧ ) ≈⟨ ? ⟩
-              ⟦ factor z ( a ( f z)) ⟧ ∎
-          an06 : {z : Carrier} → ⟦ factor z z ⟧ ≈ ε 
-          an06 {z} = begin
-             ⟦ factor z z ⟧ ≈⟨ ? ⟩  
-             (z ⁻¹ ∙ z ) ∙ ⟦ factor z z ⟧ ≈⟨ ? ⟩  
-             z ⁻¹ ∙ ( z  ∙ ⟦ factor z z ⟧ ) ≈⟨ ∙-cong grefl (is-factor z z) ⟩  
-             z ⁻¹ ∙ z ≈⟨ ? ⟩  
-             ε ∎
-          an03 : ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈ ε 
-          an03 = begin
-              ⟦ n (f y) ⁻¹  ∙ n (f x) ⟧ ≈⟨ ? ⟩ 
-              ⟦ factor y (a (f y)) ⟧ ⁻¹  ∙ ⟦ factor x (a (f x)) ⟧ ≈⟨ ? ⟩ 
-              ⟦ factor y (a (f y)) ⟧ ⁻¹  ∙ ⟦ factor x ( x ∙ ⟦ n (f x) ⟧  ⁻¹ )  ⟧ ≈⟨ ? ⟩ 
-              ⟦ n (f (y ⁻¹  ∙ x)) ⟧ ≈⟨ ? ⟩ 
-              ⟦ factor (y ⁻¹  ∙ x) (a (f (y ⁻¹  ∙ x))) ⟧ ≈⟨ ? ⟩ 
-              ⟦ n (f ⟦ ε ⟧ ) ⟧ ≈⟨ ? ⟩ 
-              ⟦ ε ⟧ ≈⟨ ? ⟩ --   ⟦ n (f x) ⟧ ≡ ⟦ n (g x) ⟧ →  ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε
-              ε  ∎
+    φ-surjective : Surjective φe
+    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse }
 
-    is-inverse : (f : (x : Carrier) → aN K x ) →  {x y : Carrier} → ⟦ n (φ (inv-φ f) x) ⟧ ≈ ⟦ n (f y) ⟧
-    is-inverse f {x} {y} = begin
-       ⟦ n (φ (inv-φ f) x) ⟧  ≈⟨ grefl  ⟩
-       ⟦ n (φ (⟦ n (f ε) ⟧ ⁻¹) x) ⟧  ≈⟨ grefl  ⟩
-       ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩            
-       ε ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩       
-       (x ∙ x ⁻¹ ) ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧  ≈⟨ ? ⟩       
-       x ∙ ( x ⁻¹  ∙ ⟦ factor x (⟦ n (f ε) ⟧ ⁻¹) ⟧ )  ≈⟨ ? ⟩       
-       x ∙ ⟦ n (f ε) ⟧ ⁻¹  ≈⟨ ? ⟩       
-       y ∙ ⟦ n (f y) ⟧ ⁻¹  ≈⟨ ? ⟩       
-       ⟦ n (f y) ⟧ ∎ where  
-           afn : a (f ε) ∙ ⟦ n (f ε) ⟧ ≈ ε
-           afn = aN=x (f ε)
-           afn' = (a (f y)) ⁻¹
-           f00 : ⟦ n (f ε) ⟧ ≈ (a (f y)) ⁻¹
-           f00 = begin
-              ⟦ n (f ε) ⟧ ≈⟨ ? ⟩ 
-              (a (f ε)) ⁻¹ ∙ a (f ε) ∙ ⟦ n (f ε) ⟧ ≈⟨ ? ⟩
-              (a (f ε)) ⁻¹ ∙ ε ≈⟨ ? ⟩
-              ⟦ n (f y) ⟧ ∙ y ⁻¹  ≈⟨ ? ⟩
-              (a (f y)) ⁻¹ ∙ ( a (f y) ∙ ⟦ n (f y) ⟧ ∙ y ⁻¹ ) ≈⟨ ? ⟩
-              (a (f y)) ⁻¹ ∎
-
-    φ-surjective : Surjective φe 
-    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = ? } 
- 
 record FundamentalHomomorphism (G H : Group c c )
-    (f : Group.Carrier G → Group.Carrier H ) 
-    (homo : IsGroupHomomorphism (GR G) (GR H) f ) 
+    (f : Group.Carrier G → Group.Carrier H )
+    (homo : IsGroupHomomorphism (GR G) (GR H) f )
     (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set c where
   open Group H
   field
     h : Group.Carrier (G / K ) → Group.Carrier H
     h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
     is-solution : (x : Group.Carrier G)  →  f x ≈ h ( φ G K x )
-    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  →
        ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
 
 FundamentalHomomorphismTheorm : (G H : Group c c)
@@ -341,14 +203,14 @@
   } where
     open Group H
     h : Group.Carrier (G / K ) → Group.Carrier H
-    h r = f ( aN.n (r (Group.ε G )  ))
+    h r = f ( aN.n ? )
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
     h03 x y = {!!}
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
           isMagmaHomomorphism = record {
-             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
+             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} }
            ; homo = h03 }
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
@@ -356,12 +218,14 @@
     is-solution x = begin
          f x ≈⟨ ? ⟩
          ? ≈⟨ ? ⟩
-         f ( aN.n (( φ G K x ) (Group.ε G )  )) ≈⟨ ?  ⟩
+         f ( aN.n (( φ G K  ) (Group.ε G )  )) ≈⟨ ?  ⟩
          h ( φ G K x ) ∎ where open EqReasoning (Algebra.Group.setoid H )
-    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → 
+    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  →
        ( (x : Group.Carrier G)  →  f x ≈ h1 ( φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
     unique = ?
 
 
 
 
+
+