diff --git a/src/Misc/FiveLemma/Exact.agda b/src/Misc/FiveLemma/Exact.agda
index f9e6502..f9beb67 100644
--- a/src/Misc/FiveLemma/Exact.agda
+++ b/src/Misc/FiveLemma/Exact.agda
@@ -1,13 +1,13 @@
 {-# OPTIONS --cubical #-}
 
-module Misc.Exact where
+module Misc.FiveLemma.Exact where
 
 open import Agda.Primitive
-open import Cubical.Data.Sigma
 open import Cubical.Categories.Abelian
 open import Cubical.Categories.Additive
 open import Cubical.Categories.Category
 open import Cubical.Categories.Morphism
+open import Cubical.Data.Sigma
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Pointed
 open import Cubical.Foundations.Prelude
@@ -15,6 +15,8 @@ open import Cubical.Foundations.Structure
 open import Cubical.Functions.Embedding
 open import Cubical.Functions.Surjection
 
+open import Misc.FiveLemma.GroupMorphisms
+
 private
   variable
     ℓ ℓ' : Level
diff --git a/src/Misc/FiveLemma/Group/Exact.agda b/src/Misc/FiveLemma/Group/Exact.agda
new file mode 100644
index 0000000..e1d57ff
--- /dev/null
+++ b/src/Misc/FiveLemma/Group/Exact.agda
@@ -0,0 +1,18 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Exact where
+
+open import Agda.Primitive
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Misc.FiveLemma.Group.Morphisms
+
+private
+  variable
+    ℓ ℓ' : Level
+
+isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
+isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
diff --git a/src/Misc/FiveLemma/Group/Injective.agda b/src/Misc/FiveLemma/Group/Injective.agda
new file mode 100644
index 0000000..2941cde
--- /dev/null
+++ b/src/Misc/FiveLemma/Group/Injective.agda
@@ -0,0 +1,134 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Injective where
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation.Properties
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Pushout
+
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
+
+open BijectionIso'
+open IsGroupHom
+open GroupStr using (1g)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso' B B') (n : GroupHom C C') (p : BijectionIso' D D') (q : GroupHom E E')
+  (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
+  (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
+  (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
+  where
+    nInjective : isInjective n
+    nInjective c c-in-ker[n] =
+      let
+        t[n[c]]≡0 : t .fst (n .fst c) ≡ D' .snd .1g
+        t[n[c]]≡0 = cong (t .fst) c-in-ker[n] ∙ t .snd .pres1
+
+        t[n[c]]≡p[h[c]] : t .fst (n .fst c) ≡ p .fun .fst (h .fst c)
+        t[n[c]]≡p[h[c]] = sq3 c
+
+        p[h[c]]≡0 : p .fun .fst (h .fst c) ≡ D' .snd .1g
+        p[h[c]]≡0 = sym t[n[c]]≡p[h[c]] ∙ t[n[c]]≡0
+
+        h[c]≡0 : h .fst c ≡ D .snd .1g
+        h[c]≡0 = p .inj (h .fst c) p[h[c]]≡0
+
+        c-in-ker[h] : isInKer h c
+        c-in-ker[h] = h[c]≡0
+
+        c-in-im[g] : isInIm' g c
+        c-in-im[g] = gh c .fst c-in-ker[h]
+
+        b : ⟨ B ⟩
+        b = fst c-in-im[g]
+
+        g[b]≡c : g .fst b ≡ c
+        g[b]≡c = snd c-in-im[g]
+
+        n[g[b]]≡0 : n .fst (g .fst b) ≡ C' .snd .1g
+        n[g[b]]≡0 = cong (n .fst) g[b]≡c ∙ c-in-ker[n]
+
+        m[b] : ⟨ B' ⟩
+        m[b] = m .fun .fst b
+
+        s[m[b]]≡n[g[b]] : s .fst m[b] ≡ n .fst (g .fst b)
+        s[m[b]]≡n[g[b]] = sq2 b
+
+        s[m[b]]≡0 : s .fst m[b] ≡ C' .snd .1g
+        s[m[b]]≡0 = s[m[b]]≡n[g[b]] ∙ n[g[b]]≡0
+
+        m[b]-in-ker[s] : isInKer s m[b]
+        m[b]-in-ker[s] = s[m[b]]≡0
+        
+        m[b]-in-im[r] : isInIm' r m[b]
+        m[b]-in-im[r] = rs m[b] .fst m[b]-in-ker[s]
+
+        a' : ⟨ A' ⟩
+        a' = fst m[b]-in-im[r]
+
+        r[a']≡m[b] : r .fst a' ≡ m[b]
+        r[a']≡m[b] = snd m[b]-in-im[r]
+
+        a : ⟨ A ⟩
+        a = lSurj a' .fst
+        
+        l[a]≡a' : l .fst a ≡ a'
+        l[a]≡a' = lSurj a' .snd
+
+        m[f[a]] : ⟨ B' ⟩
+        m[f[a]] = m .fun .fst (f .fst a)
+
+        r[l[a]]≡m[f[a]] : r .fst (l .fst a) ≡ m[f[a]]
+        r[l[a]]≡m[f[a]] = sq1 a
+
+        m[f[a]]≡m[b] : m[f[a]] ≡ m[b]
+        m[f[a]]≡m[b] = sym r[l[a]]≡m[f[a]] ∙ cong (r .fst) l[a]≡a' ∙ r[a']≡m[b]
+
+        f[a]≡b : f .fst a ≡ b
+        f[a]≡b = isInjective→isMono (m .fun) (m .inj) m[f[a]]≡m[b]
+
+        g[f[a]]≡c : g .fst (f .fst a) ≡ c
+        g[f[a]]≡c = cong (g .fst) f[a]≡b ∙ g[b]≡c
+
+        f[a]-in-im[f] : isInIm' f (f .fst a)
+        f[a]-in-im[f] = a , refl
+
+        f[a]-in-ker[g] : isInKer g (f .fst a)
+        f[a]-in-ker[g] = invIsEq (fg (f .fst a) .snd) f[a]-in-im[f]
+
+        g[f[a]]≡0 : g .fst (f .fst a) ≡ C .snd .1g
+        g[f[a]]≡0 = f[a]-in-ker[g]
+
+        c≡0 : c ≡ C .snd .1g
+        c≡0 = sym g[f[a]]≡c ∙ g[f[a]]≡0
+      in c≡0
\ No newline at end of file
diff --git a/src/Misc/FiveLemma/Group/Lemma.agda b/src/Misc/FiveLemma/Group/Lemma.agda
new file mode 100644
index 0000000..b55645c
--- /dev/null
+++ b/src/Misc/FiveLemma/Group/Lemma.agda
@@ -0,0 +1,57 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.Lemma where
+
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.GroupPath
+open import Cubical.Algebra.Group.Instances.Unit
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.Properties
+open import Cubical.Algebra.Monoid
+open import Cubical.Algebra.Semigroup
+open import Cubical.Data.Unit
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Cubical.HITs.PropositionalTruncation.Base
+open import Cubical.HITs.PropositionalTruncation.Properties
+  renaming (rec to propTruncRec ; map to propTruncMap ; rec2 to propTruncRec2 ; map2 to propTruncMap2 ; elim to propTruncElim)
+open import Cubical.HITs.Pushout.Base
+open import Cubical.HITs.Pushout
+
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
+open import Misc.FiveLemma.Group.Injective
+open import Misc.FiveLemma.Group.Surjective
+
+open BijectionIso'
+open IsGroupHom
+open GroupStr using (1g)
+
+private
+  variable
+    ℓ ℓ' : Level
+
+module _
+  (A B C D E A' B' C' D' E' : Group ℓ)
+  (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
+  (l : GroupHom A A') (m : BijectionIso' B B') (n : GroupHom C C') (p : BijectionIso' D D') (q : GroupHom E E')
+  (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
+  (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
+  (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
+  (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
+  (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
+  (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
+  (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
+  where
+    nInj = nInjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
+    nSur = nSurjective A B C D E A' B' C' D' E' f g h j l m n p q r s t u fg gh hj rs st tu lSurj qInj sq1 sq2 sq3 sq4
+
+    lemma : BijectionIso' C C'
+    lemma = bijIso' n nInj nSur
\ No newline at end of file
diff --git a/src/Misc/FiveLemma/GroupMorphisms.agda b/src/Misc/FiveLemma/Group/Morphisms.agda
similarity index 97%
rename from src/Misc/FiveLemma/GroupMorphisms.agda
rename to src/Misc/FiveLemma/Group/Morphisms.agda
index 84516ed..0310079 100644
--- a/src/Misc/FiveLemma/GroupMorphisms.agda
+++ b/src/Misc/FiveLemma/Group/Morphisms.agda
@@ -4,7 +4,7 @@
 -- Not sure why it's defined this way yet
 -- TODO: Find out
 
-module Misc.FiveLemma.GroupMorphisms where
+module Misc.FiveLemma.Group.Morphisms where
 
 open import Agda.Primitive
 open import Cubical.Algebra.Group
diff --git a/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md b/src/Misc/FiveLemma/Group/Surjective.agda
similarity index 91%
rename from src/Misc/FiveLemma/FiveLemmaGroup.lagda.md
rename to src/Misc/FiveLemma/Group/Surjective.agda
index dc25788..c97c322 100644
--- a/src/Misc/FiveLemma/FiveLemmaGroup.lagda.md
+++ b/src/Misc/FiveLemma/Group/Surjective.agda
@@ -1,7 +1,6 @@
-```
 {-# OPTIONS --cubical #-}
 
-module Misc.FiveLemma.FiveLemmaGroup where
+module Misc.FiveLemma.Group.Surjective where
 
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.GroupPath
@@ -24,7 +23,8 @@ open import Cubical.HITs.PropositionalTruncation.Properties
 open import Cubical.HITs.Pushout.Base
 open import Cubical.HITs.Pushout
 
-open import Misc.FiveLemma.GroupMorphisms
+open import Misc.FiveLemma.Group.Morphisms
+open import Misc.FiveLemma.Group.Exact
 
 open BijectionIso'
 open IsGroupHom
@@ -34,9 +34,6 @@ private
   variable
     ℓ ℓ' : Level
 
-isExact : {A B C : Group ℓ} → (f : GroupHom A B) → (g : GroupHom B C) → Type ℓ
-isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
-
 module _
   (A B C D E A' B' C' D' E' : Group ℓ)
   (f : GroupHom A B) (g : GroupHom B C) (h : GroupHom C D) (j : GroupHom D E)
@@ -44,16 +41,15 @@ module _
   (r : GroupHom A' B') (s : GroupHom B' C') (t : GroupHom C' D') (u : GroupHom D' E')
   (fg : isExact f g) (gh : isExact g h) (hj : isExact h j)
   (rs : isExact r s) (st : isExact s t) (tu : isExact t u)
-  (lEpi : isSurjective' l)
-  (qMono : isMono q)
+  (lSurj : isSurjective' l)
+  (qInj : isInjective q)
   (sq1 : (a : fst A) → r .fst (l .fst a) ≡ m .fun .fst (f .fst a))
   (sq2 : (b : fst B) → s .fst (m .fun .fst b) ≡ n .fst (g .fst b))
   (sq3 : (c : fst C) → t .fst (n .fst c) ≡ p .fun .fst (h .fst c))
   (sq4 : (d : fst D) → u .fst (p .fun .fst d) ≡ q .fst (j .fst d))
   where
-
-    sur : isSurjective' n
-    sur c' =
+    nSurjective : isSurjective' n
+    nSurjective c' =
       let
         d' : ⟨ D' ⟩
         d' = t .fst c'
@@ -92,7 +88,7 @@ module _
         q[j[d]]≡0 = sym u[p[d]]≡q[j[d]] ∙ u[p[d]]≡0
 
         j[d]≡0 : j[d] ≡ E .snd .1g
-        j[d]≡0 = qMono (q[j[d]]≡0 ∙ sym (q .snd .IsGroupHom.pres1))
+        j[d]≡0 = qInj j[d] q[j[d]]≡0
 
         d-in-ker[j] : isInKer j d
         d-in-ker[j] = j[d]≡0
@@ -189,14 +185,4 @@ module _
 
         n[g[b]+c]≡c' : n .fst g[b]+c ≡ c'
         n[g[b]+c]≡c' = n .snd .pres· g[b] c ∙ n[g[b]]+n[c]≡c'
-      in g[b]+c , n[g[b]+c]≡c'
-
-    mono : isMono n
-    mono x = {!   !}
-
-    lemma : isIso (n .fst)
-    lemma = gg , {!   !} , {!   !} where
-      gg : C' .fst → C .fst
-      gg c' = {!  !}
-
-```
+      in g[b]+c , n[g[b]+c]≡c'
\ No newline at end of file