--- a/src/group.agda	Tue Jan 24 20:25:02 2023 +0900
+++ b/src/group.agda	Tue Jan 24 23:10:15 2023 +0900
@@ -22,6 +22,7 @@
 open import Algebra.Core
 open import Algebra.Structures
 open import Data.Product
+open import Data.Unit
 
 record ≡-Group : Set (suc c) where
   infixr 9 _∙_
@@ -181,24 +182,43 @@
 φ : (G : Obj Groups ) (K  : NormalGroup G ) → Homomorph G (G / K )
 φ = ?
 
-GC : (G : Obj Groups ) → Category c c (suc c)
-GC G = ?
-
-U : (G H : Obj Groups ) → (f : Homomorph G H ) →  Functor (GC G) (GC H)
-U = ?
 
 
-fundamentalTheorem : (G H : Obj Groups ) → (K : NormalGroup G) → (f : Homomorph G H ) → UniversalMapping (GC G) (GC (G / K)) (U G H f )
-fundamentalTheorem G H K f = record { F = morph (φ G K)  ; η = eta ; _* = ? ; isUniversalMapping 
-       = record { universalMapping = λ {a} {b} {g} → is-solution a b g ; uniquness = ? }}  where
-     eta :  (a : Obj (GC G)) → Hom (GC G) a (Functor.FObj (U G H f) ( (morph (φ G K) a)) )
-     eta = ?
-     solution : {a : Obj (GC G)} {b : Obj (GC (G / K))} → Hom (GC G) a (Functor.FObj (U G H f) b) → Hom (GC (G / K)) (morph (φ G K) a) b
-     solution = ?
-     is-solution :  (a : Obj (GC G)) (b : Obj (GC (G / K)))
-            (g : Hom (GC G) a (Functor.FObj (U G H f) b)) →
-            (GC G) [ (GC G) [ Functor.FMap (U G H f) (solution {a} {b} g) o eta a ] ≈ g ]
-     is-solution = ?
+GC : (G : Obj Groups ) → Category c c (suc c)
+GC G = record { Obj = Lift c ⊤ ; Hom = λ _ _ → ≡-Group.Carrier G ; _o_ = ≡-Group._∙_ G }
+
+U : (G H : Obj Groups ) → (f : Homomorph G H ) →  Functor (GC G) (GC H)
+U G H f = record { FObj = λ _ → lift  tt ; FMap = λ an → morph f ? }
+
+F : (G H : Obj Groups ) → (f : Homomorph G H ) → (K : NormalGroup G)  →  Functor (GC H) (GC (G / K))
+F G H f = ? --record { FObj = λ _ → lift  tt ; FMap = λ x → morph f x }
+
+--       f                f   ε
+--    G --→ H          G --→  H (a)
+--    |   /            |    /
+--  φ |  / h         φ |   /h ↑
+--    ↓ /              ↓  /
+--    G/K              G/K
+
+fundamentalTheorem : (G H : Obj Groups ) → (K : NormalGroup G) → (f : Homomorph G H ) 
+     → ( kerf⊆K : (x : ≡-Group.Carrier G) → aN K x  → morph f x ≡ ≡-Group.ε H  )
+     → UniversalMapping (GC G) (GC H) ?
+fundamentalTheorem G H K f kerf⊆K = record { U = λ _ → lift tt ; ε = λ _ → ? ; _* = ? ; isUniversalMapping 
+       = record { universalMapping = λ {a} {b} {g} → ? ; uniquness = ? }}  
+
+fundamentalTheorem' : (G H : Obj Groups ) → (K : NormalGroup G) → (f : Homomorph G H ) 
+     → ( kerf⊆K : (x : ≡-Group.Carrier G) → aN K x  → morph f x ≡ ≡-Group.ε H  )
+     → coUniversalMapping (GC H) (GC (G / K)) (F G H f K )
+fundamentalTheorem' G H K f kerf⊆K = record { U = λ _ → lift tt ; ε = λ _ → ? ; _* = ? ; iscoUniversalMapping 
+       = record { couniversalMapping = λ {a} {b} {g} → ? ; uniquness = ? }}  where
+     m : Homomorph G G
+     m = NormalGroup.normal K 
+     φ⁻¹ : ≡-Group.Carrier (G / K) → ≡-Group.Carrier G
+     φ⁻¹ = ?
+     ---      f ( φ⁻¹ z ) ) ≡ g
+     solution :  {b : Obj (GC H)} {a : Obj (GC (G / K))} → Hom (GC H) (lift tt) b → Hom (GC G) a (lift tt)
+     solution g = ?
+     is-solution :  (a : Obj (GC G)) (b : Obj (GC (G / K))) (g :  Hom (GC H) (lift tt) a  ) →  GC H [ GC H [ ≡-Group.ε H o morph f ? ] ≈ g ]
+     is-solution a b g = ?
    
 
-