# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1674570200 -32400
# Node ID 043bd660753b064cb70631be8e095b0317c7ff3e
# Parent  57683a6e567445c31735bb4346f28f0158bc9cd3
...

diff -r 57683a6e5674 -r 043bd660753b src/group.agda
--- a/src/group.agda	Tue Jan 24 23:10:15 2023 +0900
+++ b/src/group.agda	Tue Jan 24 23:23:20 2023 +0900
@@ -187,11 +187,8 @@
 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 G H f K = record { FObj = λ _ → lift  tt ; FMap = λ x y → record { a = ? ; n = ? ; x=aN = ?  } ; isFunctor = ?  }
 
 --       f                f   ε
 --    G --→ H          G --→  H (a)
@@ -200,25 +197,21 @@
 --    ↓ /              ↓  /
 --    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
+fundamentalTheorem' G H K f kerf⊆K = record { U = λ _ → lift tt ; ε = λ _ g → record { a = ? ; n = ? ; x=aN = ? }  
+   ; _* = λ {b} {a} g → solution {b} {a} g ; iscoUniversalMapping 
+       = record { couniversalMapping = ?  ; 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 ]
+     solution : {b : Obj (GC (G / K))} {a : Obj (GC H)} { f0 : Hom (GC (G / K)) (lift tt) b} →
+            GC (G / K) [ GC (G / K) [ (λ g → record { a = ? ; n = ? ; x=aN = ? }) o
+                (λ y → record { a = ? ; n = ? ; x=aN = ? }) ] ≈ f0 ]
+     solution = ?
+     is-solution :  ?
      is-solution a b g = ?