# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1693733394 -32400
# Node ID 7c1e3e0be315fbb2fbb06b288930cb66681ddb28
# Parent  cc81d3b1a82aa30b254e80dc55a3d3ae66a61c80
...

diff -r cc81d3b1a82a -r 7c1e3e0be315 src/Gutil0.agda
--- a/src/Gutil0.agda	Sat Sep 02 16:44:24 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,101 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-open import Level hiding ( suc ; zero )
-module Gutil0  where
-
-open import Algebra
-open import Algebra.Structures
-open import Algebra.Definitions
-open import Data.Product
-open import Relation.Binary.PropositionalEquality 
-open import Algebra.Morphism.Structures
-open import Data.Empty
-open import Relation.Nullary
-
-open GroupMorphisms
-
-GR : {c l : Level } → Group c l → RawGroup c l
-GR G = record {
-     Carrier        = Carrier G
-     ; _≈_          = _≈_ G
-     ; _∙_          = _∙_ G
-     ; ε            = ε G
-     ; _⁻¹          = _⁻¹ G
-  } where open Group
-
-record GAxiom {c l : Level } (G : Group c l)  : Set ( c  Level.⊔  l ) where
-  open Group G
-  field
-     ∙-cong :  {x y u v : Carrier } → x ≈ y → u ≈ v →  x ∙ u ≈  y ∙ v 
-     assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈  x ∙ ( y ∙ z )
-     identity : ((y : Carrier) → ε ∙ y ≈ y ) ×  ((y : Carrier) → y ∙ ε ≈ y )
-     inverse   : ((y : Carrier) → y ⁻¹ ∙ y  ≈ ε ) ×  ((y : Carrier) → y ∙ y ⁻¹  ≈ ε )
-     ⁻¹-cong   : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹
-
-GA : {c l : Level } → (G : Group c l) → GAxiom G
-GA G = record {
-        ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)))
-     ;  assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))
-     ;  identity = IsMonoid.identity ( IsGroup.isMonoid isGroup)
-     ;  inverse   = IsGroup.inverse isGroup
-     ;  ⁻¹-cong   = IsGroup.⁻¹-cong isGroup
-   } where open Group G
-
-open import Relation.Binary.Structures
-
-Eq : {c l : Level } → (G : Group c l) → IsEquivalence _
-Eq G =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
-             (IsGroup.isMonoid (Group.isGroup G ))) )
-
-_<_∙_> : {c d : Level} (m : Group c d )  →    Group.Carrier m →  Group.Carrier m →  Group.Carrier m
-m < x ∙ y > =  Group._∙_ m x y
-
-_<_≈_> : {c d : Level} (m : Group c d )  →    (f  g : Group.Carrier m ) → Set d
-m < x ≈ y > =  Group._≈_ m x y
-
-infixr 9 _<_∙_>
-
--- assuming Homomorphism is too strong
---
-record NormalSubGroup {c d : Level} (A : Group c d )  : Set (Level.suc (Level.suc (c Level.⊔ d))) where
-   open Group A
-   field                           
-       P : Carrier  → Set (Level.suc c ⊔ d) 
-       Pε : P ε
-       P⁻¹ : (a : Carrier  ) → P a → P (a ⁻¹)
-       P≈ :  {a b : Carrier  } → a ≈ b → P a → P b
-       P∙ :  {a b : Carrier  } → P a → P b → P (  a ∙ b  )
-       -- gN ≈ Ng
-       Pcomm : {a b : Carrier  }  → P a  →  P ( b ∙  ( a  ∙ b ⁻¹ ) )
-
-import Relation.Binary.Reasoning.Setoid as EqReasoning
-
-record Nelm {c d : Level} {A : Group c d } (n : NormalSubGroup A) : Set  (Level.suc c ⊔ d)  where
-   open Group A
-   open NormalSubGroup n 
-   field                           
-       elm : Carrier
-       Pelm : P elm
-
-NGroup : {c d : Level} {A : Group c d } (n : NormalSubGroup A) → Group  (Level.suc c ⊔ d)  d
-NGroup {_} {_} {A} n = record {
-      Carrier        = Nelm n
-    ; _≈_            = λ x y → elm x ≈ elm y
-    ; _∙_            = λ x y → record { elm = elm x ∙ elm y ; Pelm = P∙ (Pelm x) (Pelm y) }
-    ; ε              = record { elm = ε ; Pelm = Pε }
-    ; _⁻¹            = λ x → record { elm = (elm x) ⁻¹  ; Pelm = P⁻¹ (elm x) (Pelm x) }
-    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record { refl = IsEquivalence.refl (IsGroup.isEquivalence ga) 
-          ; sym =  IsEquivalence.sym (IsGroup.isEquivalence ga) 
-          ; trans = IsEquivalence.trans (IsGroup.isEquivalence ga)  }
-       ; ∙-cong = IsGroup.∙-cong ga }
-       ; assoc = λ a b c → IsGroup.assoc ga (elm a) (elm b) (elm c) }
-       ; identity = ( (λ q → proj₁ (IsGroup.identity ga) (elm q)) , (λ q → proj₂ (IsGroup.identity ga) (elm q)) ) }
-       ; inverse = ( (λ q → proj₁ (IsGroup.inverse ga) (elm q)) , (λ q → proj₂ (IsGroup.inverse ga) (elm q)) ) 
-       ; ⁻¹-cong   = IsGroup.⁻¹-cong ga }
-   }  where
-       open Group A
-       open NormalSubGroup n 
-       open Nelm 
-       ga = Group.isGroup A
-
-
diff -r cc81d3b1a82a -r 7c1e3e0be315 src/Solvable.agda
--- a/src/Solvable.agda	Sat Sep 02 16:44:24 2023 +0900
+++ b/src/Solvable.agda	Sun Sep 03 18:29:54 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level hiding ( suc ; zero )
 open import Algebra
 module Solvable {n m : Level} (G : Group n m ) where
@@ -103,7 +104,7 @@
 comm-resp : {g h g1 h1  : Carrier } → g ≈ g1  → h ≈ h1 → [ g , h ] ≈ [ g1 , h1 ] 
 comm-resp {g} {h} {g1} {h1} g=g1 h=h1 =  ∙-cong (∙-cong (∙-cong (⁻¹-cong g=g1 ) (⁻¹-cong h=h1 )) g=g1 ) h=h1
 
-open import Gutil0
+open import NormalSubgroup
 import Algebra.Morphism.Definitions as MorphismDefinitions
 open import Algebra.Morphism.Structures
 
diff -r cc81d3b1a82a -r 7c1e3e0be315 src/homomorphism.agda
--- a/src/homomorphism.agda	Sat Sep 02 16:44:24 2023 +0900
+++ b/src/homomorphism.agda	Sun Sep 03 18:29:54 2023 +0900
@@ -12,7 +12,7 @@
 
 open import Data.Product
 open import Relation.Binary.PropositionalEquality
-open import Gutil0
+open import NormalSubgroup
 import Gutil
 import Function.Definitions as FunctionDefinitions
 
@@ -38,18 +38,6 @@
 
 import Relation.Binary.Reasoning.Setoid as EqReasoning
 
--- _<_∙_> :  (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 < x ≈ y > =  Group._≈_ m x y
-
--- infixr 9 _<_∙_>
-
---
---  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
---
-
 open GroupMorphisms
 
 -- import Axiom.Extensionality.Propositional
@@ -60,167 +48,114 @@
 
 -- Set of a ∙ ∃ n ∈ N
 --
-record an {A : Group c c }  (N : NormalSubGroup A ? ) (n x : Group.Carrier A  ) : Set c where
+
+data IsaN  {A : Group c d }  (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
+    an : (n : Group.Carrier A ) →  (pn : NormalSubGroup.P N n) → IsaN N a (A < a ∙ n > )
+
+record aNeq {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
+    field
+        eq→  : {x : Group.Carrier A}  → IsaN N a x → IsaN N b x
+        eq←  : {x : Group.Carrier A}  → IsaN N b x → IsaN N a x
+
+module AN (A : Group c d) (N : NormalSubGroup A  ) where
     open Group A
     open NormalSubGroup N
-    field
-        a : Carrier 
-        aN=x :  a ∙ ⟦ n ⟧ ≈ x
-
-record aN {A : Group c c }  (N : NormalSubGroup A ? )  : Set c where
-    open Group A
-    field
-        n : Carrier 
-        is-an : (x : Carrier) → an N n x
+    open EqReasoning (Algebra.Group.setoid A)
+    open Gutil A
 
-f0 :  {A : Group c c }  (N : NormalSubGroup A ? )  (x y : Group.Carrier A) → an N x y
-f0 {A} N x y = record { a = y ∙ ⟦ x ⟧ ⁻¹ ; aN=x = gk02  } where
-   open Group A
-   open NormalSubGroup N
-   open IsGroupHomomorphism normal
-   open EqReasoning (Algebra.Group.setoid A)
-   open Gutil A
-   gk02 : {x g : Carrier } →  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x
-   gk02 {x} {g}  = begin  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid  ⟩ 
-         x ∙  ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧)  ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ 
-         x ∙ ε  ≈⟨ proj₂ identity _  ⟩ 
-         x ∎
-
-_/_ : (A : Group c c ) (N  : NormalSubGroup A ? ) → Group c c
+_/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
 _/_ A N  = record {
-    Carrier  = aN N
-    ; _≈_      = λ f g → ⟦ n f ⟧ ≈ ⟦ n g ⟧
-    ; _∙_      = qadd
-    ; ε        = qid 
-    ; _⁻¹      = λ f → record { n = n f ⁻¹ ; is-an = λ x → record { a = an.a (is-an f x) ∙  ⟦ n f ⟧  ∙ ⟦ n f ⟧  ; aN=x = qinv0 f x } } 
+    Carrier  = Group.Carrier A
+    ; _≈_      = aNeq N
+    ; _∙_      = _∙_
+    ; ε        = ε
+    ; _⁻¹      = λ x → x ⁻¹
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
-       isEquivalence = record {refl = grefl ; trans = gtrans ; sym = gsym }
-       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gtrans (homo _ _) ( gtrans (∙-cong x=y u=v)  (gsym (homo _ _) )) }
-       ; assoc = qassoc }
-       ; identity = (λ q →   ⟦⟧-cong (proj₁ identity _) ) , (λ q → ⟦⟧-cong (proj₂ identity _) )  }
-       ; inverse   =  (λ x → ⟦⟧-cong (proj₁ inverse _  )) , (λ x → ⟦⟧-cong (proj₂ inverse _ ) )
-       ; ⁻¹-cong   = λ {x} {y} → i-conv  {x} {y}
+       isEquivalence = record {refl = nrefl
+           ; trans = ? ; sym = λ a=b → ? 
+          }
+       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
+       ; assoc = ? }
+       ; identity =  ?   }
+       ; inverse   =  (λ x → ? ) , (λ x → ? ) 
+       ; ⁻¹-cong   = ? 
       }
    } where
+       _=n=_ = aNeq N
        open Group A
-       open aN
-       open an
        open NormalSubGroup N
-       open IsGroupHomomorphism normal
        open EqReasoning (Algebra.Group.setoid A)
        open Gutil A
-       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 ⟧ ≈⟨ solve monoid ⟩
-              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 ⟧ )) ≈⟨ solve monoid ⟩
-              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 ⁻¹ ∙  (x ∙ x)  ≈⟨ solve monoid ⟩
-              (x ⁻¹ ∙  x ) ∙ x  ≈⟨ ? ⟩
-              ε ∙ x  ≈⟨ solve monoid ⟩
-              x ∎
-       qinv0 : (f : aN N) → (x : Carrier ) → (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈ x
-       qinv0 f x = begin
-          (a (is-an f x) ∙ ⟦ n f ⟧ ∙ ⟦ n f ⟧) ∙ ⟦ n f ⁻¹ ⟧ ≈⟨ ? ⟩
-           a (is-an f x) ∙ ⟦ n f ⟧  ≈⟨ an.aN=x (is-an f 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 ∎
-       qassoc : (f g h : aN N) → ⟦ n ( qadd (qadd f g) h) ⟧ ≈  ⟦ n( qadd f (qadd g h)) ⟧
-       qassoc f g h = ⟦⟧-cong (assoc  _ _ _ )
-       i-conv : {x y : aN N} → ⟦ n x ⟧ ≈ ⟦ n y ⟧ →  ⟦ n x ⁻¹ ⟧ ≈ ⟦ n y ⁻¹ ⟧ 
-       i-conv {x} {y} nx=ny = begin
-          ⟦ n x ⁻¹ ⟧ ≈⟨ ⁻¹-homo _ ⟩
-          ⟦ n x ⟧ ⁻¹  ≈⟨ ⁻¹-cong nx=ny ⟩
-          ⟦ n y ⟧ ⁻¹  ≈⟨ gsym ( ⁻¹-homo _)  ⟩
-          ⟦ n y ⁻¹ ⟧  ∎
+       open AN A N
+       nrefl :  {x : Carrier} → x =n= x
+       nrefl = ?
 
 
 -- 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
+K⊆ker : (G H : Group c d)  (K : NormalSubGroup G ) (f : Group.Carrier G → Group.Carrier H ) 
+   → Set (Level.suc c ⊔ d)
+K⊆ker G H K f = (x : Group.Carrier G ) → P x → f x ≈ ε   where
   open Group H
   open NormalSubGroup K
 
 open import Function.Surjection
 open import Function.Equality
 
-module GK (G : Group c c) (K : NormalSubGroup G ? ) where
+module GK (G : Group c d) (K : NormalSubGroup G  ) where
     open Group G
-    open aN
-    open an
     open NormalSubGroup K
-    open IsGroupHomomorphism normal
     open EqReasoning (Algebra.Group.setoid G)
     open Gutil G
 
+    gkε : ?
+    gkε = ? -- record { a = ε ; n = ε ; pn = Pε }
+
     φ : Group.Carrier G → Group.Carrier (G / K )
-    φ g = record { n = g ; is-an = λ x → record { a = x ∙ ( ⟦ g ⟧ ⁻¹)   ; aN=x = gk02  } } where
-       gk02 : {x : Carrier } →  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈ x
-       gk02 {x} = begin  x ∙ ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧ ≈⟨ solve monoid  ⟩ 
-         x ∙  ( ⟦ g ⟧ ⁻¹ ∙ ⟦ g ⟧)  ≈⟨ ∙-cong grefl (proj₁ inverse _ ) ⟩ 
-         x ∙ ε  ≈⟨ proj₂ identity _  ⟩ 
-         x ∎
+    φ g = ?
 
     φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
-    φ-homo = record {⁻¹-homo = λ g → ?  ; isMonoidHomomorphism = record { ε-homo = ? ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
-       record { cong = ? } }}}
+    φ-homo = record {⁻¹-homo = ? ; isMonoidHomomorphism = record { ε-homo = ?
+           ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
+       record { cong = ? } }}} where
 
-    -- gk03 : {f : Group.Carrier (G / K) } → ⟦ n f  ⟧ ≈ ⟦ ⟦ n f ⟧ ⟧  -- a (is-an f x)  ∙ ⟦ n f ⟧ ≡ x
-    -- gk03 {x} = ?                                                   --  
 
     φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
-    φe = record { _⟨$⟩_ = φ ; cong = ?  }  where
-           φ-cong : {f g : Carrier } → f ≈ g  → ⟦ n (φ f ) ⟧ ≈ ⟦ n (φ g ) ⟧
-           φ-cong = ?
-
-    inv-φ : Group.Carrier (G / K ) → Group.Carrier G
-    inv-φ f =  n f    -- ⟦ n f ⟧ ( if we have gk03 )
+    φe = record { _⟨$⟩_ = φ ; cong = gk40 }  where
+          gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j >
+          gk40 {i} {j} i=j = ?
 
-    cong-i : {f g : Group.Carrier (G / K ) } → ⟦ n f ⟧ ≈ ⟦ n g ⟧ → inv-φ f ≈ inv-φ g
-    cong-i {f} {g} nf=ng = ? 
-
-    is-inverse : (f : aN K  ) →  ⟦ n (φ (inv-φ f) ) ⟧ ≈ ⟦ n f ⟧
-    is-inverse f = begin
-       ⟦ n (φ (inv-φ f) ) ⟧  ≈⟨ grefl  ⟩
-       ⟦ n (φ ( n f  ) ) ⟧  ≈⟨ grefl  ⟩
-       ⟦ n f ⟧ ∎
+    inv-φ : Group.Carrier (G / K ) → Carrier 
+    inv-φ = ? -- record { a = a ; n = n ; pn = pn } = a ∙ n 
 
     φ-surjective : Surjective φe
-    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → cong-i {f} {g} }  ; right-inverse-of = is-inverse }
+    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → ? }
+          ; right-inverse-of = ? } where
+       gk50 :  (f g : Group.Carrier (G / K)) → ? ≈ ? → inv-φ f ≈ inv-φ g
+       gk50 = ?
+       gk60 : (x : Group.Carrier (G / K )) → inv-φ x ∙ ε ≈ ?
+       gk60 = ?
 
     gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >
-    gk01 x = begin
-        ⟦ inv-φ x ⟧  ≈⟨ grefl ⟩ 
-        ⟦ n x ⟧ ∎
+    gk01 = ?
 
 
-record FundamentalHomomorphism (G H : Group c c )
+record FundamentalHomomorphism (G H : Group c d )
     (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
+    (K : NormalSubGroup G  ) (kf : K⊆ker G H K f) :  Set (Level.suc c ⊔ d) where
   open Group H
   -- open GK G K
   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 ? -- ( GK.φ ? x )
+    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( GK.φ G K x )
     unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
-       → ( (x : Group.Carrier G)  →  f x ≈ h1 ? ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
+       → ( (x : Group.Carrier G)  →  f x ≈ h1 ( GK.φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
 
-FundamentalHomomorphismTheorm : (G H : Group c c)
+FundamentalHomomorphismTheorm : (G H : Group c d)
     (f : Group.Carrier G → Group.Carrier H )
     (homo : IsGroupHomomorphism (GR G) (GR H) f )
-    (K : NormalSubGroup G ? ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
+    (K : NormalSubGroup G  ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
 FundamentalHomomorphismTheorm G H f homo K kf = record {
      h = h
    ; h-homo = h-homo
@@ -232,11 +167,11 @@
     open Gutil H
     -- open NormalSubGroup K ?
     open IsGroupHomomorphism homo
-    open aN
+    open EqReasoning (Algebra.Group.setoid H)
     h : Group.Carrier (G / K ) → Group.Carrier H
-    h r = f ( GK.inv-φ ? ? ? )
+    h r = f ( GK.inv-φ G K r )
     h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
-    h03 x y = {!!}
+    h03 = ?
     h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
     h-homo = record {
      isMonoidHomomorphism = record {
@@ -245,10 +180,9 @@
            ; homo = h03 }
         ; ε-homo = {!!} }
        ; ⁻¹-homo = {!!} }
-    open EqReasoning (Algebra.Group.setoid H)
     is-solution : (x : Group.Carrier G)  →  f x ≈ h ( GK.φ ? ? x )
     is-solution x = begin
-         f x ≈⟨ grefl  ⟩
+         f x ≈⟨ ? ⟩
          h ( GK.φ ? ? x ) ∎ 
     unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
        → ( (x : Group.Carrier G)  →  f x ≈ h1 ( GK.φ ? ? x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )