From 38b152a9a455f12605de1c62e5f7bf661de4dac0 Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Sun, 3 Nov 2024 00:48:30 -0500
Subject: [PATCH] wip

---
 src/Misc/FiveLemma.agda      | 35 -----------------------------------
 src/Misc/FiveLemmaGroup.agda | 27 ++++++++++++++++++---------
 2 files changed, 18 insertions(+), 44 deletions(-)

diff --git a/src/Misc/FiveLemma.agda b/src/Misc/FiveLemma.agda
index b6c1015..3413c4f 100644
--- a/src/Misc/FiveLemma.agda
+++ b/src/Misc/FiveLemma.agda
@@ -18,41 +18,6 @@ private
   variable
     ℓ ℓ' : Level
 
--- kernel : {l : Level} → {A B : Pointed l} → (f : A →∙ B) → Type l
--- kernel {l} {A = A @ A , a} {B = B @ B , b} (f , f-eq) =
---   -- all elements of A that map to the base point b of B
---   Σ A λ a → f a ≡ b
-
--- image : {l : Level} → {A B : Pointed l} → (f : A →∙ B) → Type l
--- image {l} {A = A @ A , a} {B = B @ B , b} (f , f-eq) =
---   -- all elements of B such that
---   Σ B (λ b →
---     -- there exists some A such that f(a) is b
---     Σ A λ a → f a ≡ b
---   )
-
--- module _ (C : Category ℓ ℓ') where
---   open Category C
-
---   module _ {x y : ob} where
-
---     record IsImage {i : ob} (f : Hom[ x , y ]) (m : Hom[ i , y ]) : Type (ℓ-max ℓ ℓ') where
---       field
---         e : Hom[ x , i ]
---         req1 : f ≡ (_⋆_ e m)
---         req2 : (i' : ob) → (e' : Hom[ x , i' ]) → (m' : Hom[ i' , y ]) → f ≡ (_⋆_ e' m')
---           → ∃![ v ∈ Hom[ i , i' ] ] (m ≡ (_⋆_ v m'))
-
-
---     record Image (f : Hom[ x , y ]) : Type (ℓ-max ℓ ℓ') where
---       field
---         i : ob
---         m : Hom[ i , y ]
---         isIm : IsImage f m
-
---   im : ∀ {x y : ob} → (f : Hom[ x , y ]) → Image f
---   im {x} {y} f = record { i = {!   !} ; m = {!   !} ; isIm = {!   !} }
-
 module fiveLemma (AC : AbelianCategory ℓ ℓ') where
   open AbelianCategory AC
 
diff --git a/src/Misc/FiveLemmaGroup.agda b/src/Misc/FiveLemmaGroup.agda
index e206960..3f526bb 100644
--- a/src/Misc/FiveLemmaGroup.agda
+++ b/src/Misc/FiveLemmaGroup.agda
@@ -6,14 +6,15 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Function
 open import Cubical.Foundations.Isomorphism
-
+open import Cubical.Foundations.Structure
 open import Cubical.Data.Unit
-
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.Group.MorphismProperties
 open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Properties
 open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.HITs.PropositionalTruncation.Properties renaming (rec to propTruncRec)
 
 private
   variable
@@ -29,9 +30,9 @@ module _
   (h : GroupHom C D)
   (j : GroupHom D E)
   (l : GroupHom A A')
-  (m : GroupHom B B')
+  (m : BijectionIso B B')
   (n : GroupHom C C')
-  (p : GroupHom D D')
+  (p : BijectionIso D D')
   (q : GroupHom E E')
   (r : GroupHom A' B')
   (s : GroupHom B' C')
@@ -44,17 +45,25 @@ module _
   (st : isExact s t)
   (tu : isExact t u)
   (lEpi : isSurjective l)
-  (mIso : isIso (m .fst))
-  (pIso : isIso (p .fst))
-  (q : isMono p)
+  (q : isMono q)
   where
+    open BijectionIso
 
     sur : isSurjective n
+    sur c' =
+      let pSurj = p .surj in
+      let t[c'] = t .fst c' in
+      let step1 = pSurj t[c'] in
+      let d-thing = snd D in
+      let d-is-group = isPropIsGroup {!   !} {!   !} {!   !} in
+      let step2 = propTruncRec {!   !} (λ x → fst x) step1 in
+      {!   !}
 
     mono : isMono n
+    mono x = {!   !}
 
     lemma : isIso (n .fst)
     lemma = gg , {!   !} , {!   !} where
       gg : C' .fst → C .fst
-      gg = {!   !}
-    
\ No newline at end of file
+      gg c' = {!  !}
+     
\ No newline at end of file