diff --git a/src/Misc/FiveLemma/Exact.agda b/src/Misc/FiveLemma/Category/Exact.agda
similarity index 63%
rename from src/Misc/FiveLemma/Exact.agda
rename to src/Misc/FiveLemma/Category/Exact.agda
index f9beb67..fbf7ffd 100644
--- a/src/Misc/FiveLemma/Exact.agda
+++ b/src/Misc/FiveLemma/Category/Exact.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --cubical #-}
 
-module Misc.FiveLemma.Exact where
+module Misc.FiveLemma.Category.Exact where
 
 open import Agda.Primitive
 open import Cubical.Categories.Abelian
@@ -15,8 +15,6 @@ open import Cubical.Foundations.Structure
 open import Cubical.Functions.Embedding
 open import Cubical.Functions.Surjection
 
-open import Misc.FiveLemma.GroupMorphisms
-
 private
   variable
     ℓ ℓ' : Level
@@ -59,7 +57,7 @@ module _ (AC : AbelianCategory ℓ ℓ') where
 
     -- I am using Vec in the reverse way!!!
 
-    -- Fin 5   4    3    2    1    0
+    -- Fin 5   0    1    2    3    4
     -- obSeq = E :: D :: C :: B :: A :: []
 
     -- Fin 4    3     2     1      0
@@ -67,37 +65,24 @@ module _ (AC : AbelianCategory ℓ ℓ') where
 
     -- sequence of Homs
     data HomSeq : {n : ℕ} → (os : obSeq n) → Type (ℓ-max ℓ ℓ') where
-      h[_] : {os : obSeq z} → Hom[ lookup os (inject₁ Fin.zero) , lookup os (suc Fin.zero) ] → HomSeq os
-      _h∷_ : {n : ℕ} {os : obSeq n} {o : ob}
-        → Hom[ (head os) , o ] → HomSeq os → HomSeq (o ∷ os)
+      h[_] : {os : obSeq z} → Hom[ lookup os (suc Fin.zero) , lookup os (inject₁ Fin.zero) ] → HomSeq os
+      _h∷_ : {n : ℕ} {os : obSeq n} {o : ob} → Hom[ (head os) , o ] → HomSeq os → HomSeq (o ∷ os)
 
     homSeqN : {n : ℕ} → (os : obSeq n) → (m : Fin (suc n)) → Type ℓ'
-    homSeqN {n = n} os m = Hom[ (lookup os (inject₁ m)) , (lookup os (suc m)) ]
+    homSeqN {n = n} os m = Hom[ (lookup os (opposite (inject₁ m))) , (lookup os (opposite (suc m))) ]
 
-    op-inv : {n : ℕ} → (m : Fin n) → opposite (opposite m) ≡ m
-    op-inv {n = n} m = sym (fuckyou2 n (opposite (opposite m))) ∙ {!    !} ∙ fuckyou2 n m where
-      fuckyou1 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ m) n
-      fuckyou1 (suc n) Fin.zero = z<s
-      fuckyou1 (suc n) (suc m) = s<s (fuckyou1 n m)
-
-      fuckyou2 : (n : ℕ) → (m : Fin n) → fromℕ< {m = toℕ m} (fuckyou1 n m) ≡ m
-      fuckyou2 (suc n) Fin.zero = refl
-      fuckyou2 (suc n) (suc m) = let IH = fuckyou2 n m in cong suc IH
-
-      fuckyou3 : (n : ℕ) → (m : Fin n) → Data.Nat._<_ (toℕ (opposite m)) n
-      fuckyou3 (suc ℕ.zero) Fin.zero = z<s
-      fuckyou3 (2+ n) Fin.zero = let IH = fuckyou3 (suc n) Fin.zero in s<s IH
-      fuckyou3 (suc n) (suc m) = let IH = fuckyou3 n m in {!   !}
-
-    homSeqLookup : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
-    homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = x
-    homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {! opposite m   !} where
-      op = opposite m
-      helper : (k : Fin (2+ n)) → homSeqN (o ∷ os) (opposite k)
-      helper k = {!   !}
+    -- homSeqLookupOpp : {n : ℕ} {os : obSeq n} → HomSeq os → (m : Fin (suc n)) → homSeqN os m
+    -- homSeqLookupOpp {n = ℕ.zero} {os = y ∷ x ∷ []} h[ h ] Fin.zero = h
+    -- homSeqLookupOpp {n = suc n} {os = y ∷ x ∷ os} (h1 h∷ hs) (suc m) =
+    --   homSeqLookupOpp {n = n} {os = x ∷ os} hs {!   !}
+    -- homSeqLookup {n = ℕ.zero} h[ x ] Fin.zero = {! x  !}
+    -- homSeqLookup {n = suc n} (_h∷_ {os = os} {o = o} h1 hs) m = helper {!    !} where
+    --   op = opposite m
+    --   helper : (k : Fin (2+ n)) → homSeqN (o ∷ os) (opposite k)
+    --   helper k = {!   !}
     
     -- Retrieve the LAST hom in the sequence
-    hhead : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {!   !} , {!   !} ]
+    -- hhead : ∀ {n : ℕ} {os : obSeq n} → HomSeq os → Hom[ {!   !} , {!   !} ]
     -- hhead h[ x ] = x
     -- hhead (x h∷ hs) = x
 
@@ -116,5 +101,5 @@ module _ (AC : AbelianCategory ℓ ℓ') where
     -- exactHomSeq {n = suc n} (y h∷ (x h∷ x₂)) (suc m) = {!   !}
 
     -- -- exactHomVec : Type (ℓ-max ℓ ℓ')
-    -- -- exactHomVec = {n : ℕ} {o : ob} →               
+    -- -- exactHomVec = {n : ℕ} {o : ob} →                 
     -- --   Σ (HomVec o n) λ h → finExactSequence {!   !} {!   !} 
\ No newline at end of file
diff --git a/src/Misc/FiveLemma/FiveLemma.agda b/src/Misc/FiveLemma/Category/Lemma.agda
similarity index 98%
rename from src/Misc/FiveLemma/FiveLemma.agda
rename to src/Misc/FiveLemma/Category/Lemma.agda
index 7e859f1..389d64c 100644
--- a/src/Misc/FiveLemma/FiveLemma.agda
+++ b/src/Misc/FiveLemma/Category/Lemma.agda
@@ -1,6 +1,6 @@
 {-# OPTIONS --cubical #-}
 
-module Misc.FiveLemma where
+module Misc.FiveLemma.Category.Lemma where
 
 open import Agda.Primitive
 open import Cubical.Data.Sigma
diff --git a/src/Misc/FiveLemma/Group/Exact.agda b/src/Misc/FiveLemma/Group/Exact.agda
index e1d57ff..fccb891 100644
--- a/src/Misc/FiveLemma/Group/Exact.agda
+++ b/src/Misc/FiveLemma/Group/Exact.agda
@@ -15,4 +15,4 @@ private
     ℓ ℓ' : 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)
+isExact {B = B} f g = (b : ⟨ B ⟩) → (isInKer g b) ≃ (isInIm' f b)
\ No newline at end of file
diff --git a/src/Misc/FiveLemma/Group/ExactSequence.agda b/src/Misc/FiveLemma/Group/ExactSequence.agda
new file mode 100644
index 0000000..0b2125f
--- /dev/null
+++ b/src/Misc/FiveLemma/Group/ExactSequence.agda
@@ -0,0 +1,36 @@
+{-# OPTIONS --cubical #-}
+
+module Misc.FiveLemma.Group.ExactSequence where
+
+open import Agda.Primitive
+open import Cubical.Algebra.Group.Base
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Data.Nat
+open import Data.Fin
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure
+open import Misc.FiveLemma.Group.Exact
+open import Misc.FiveLemma.Group.Morphisms
+
+private
+  variable
+    ℓ ℓ' : Level
+
+pattern 1+ n = suc n
+pattern 2+ n = suc (suc n)
+
+inj1 = λ {m : ℕ} (n : Fin m) → inject₁ n
+inj2 = λ {m : ℕ} (n : Fin m) → inject₁ (inject₁ n)
+
+FiniteLES : {len : ℕ}
+  → (groupSeq : (n : Fin (2+ len)) → Group ℓ)
+  → (homSeq : (m : Fin (1+ len)) → GroupHom (groupSeq (inj1 m)) (groupSeq (suc m)))
+  → Type ℓ
+FiniteLES {len = len} groupSeq homSeq = (m : Fin len) → isExact (homSeq (inj1 m)) (homSeq (suc m))
+
+InfiniteLES :
+  (groupSeq : (n : ℕ) → Group ℓ)
+  → (homSeq : (n : ℕ) → GroupHom (groupSeq n) (groupSeq (suc n)))
+  → Type ℓ
+InfiniteLES groupSeq homSeq = (m : ℕ) → isExact (homSeq m) (homSeq (suc m))
diff --git a/src/Misc/FiveLemma/SnakeLemma.agda b/src/Misc/FiveLemma/SnakeLemma.agda
deleted file mode 100644
index 4d54730..0000000
--- a/src/Misc/FiveLemma/SnakeLemma.agda
+++ /dev/null
@@ -1,34 +0,0 @@
-{-# OPTIONS --cubical #-}
-
-module Misc.SnakeLemma 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.Foundations.Equiv
-open import Cubical.Foundations.Pointed
-open import Cubical.Foundations.Prelude
-open import Cubical.Foundations.Structure
-open import Cubical.Functions.Embedding
-open import Cubical.Functions.Surjection
-
-open import Misc.Exact
-
-private
-  variable
-    ℓ ℓ' : Level
-
-module snakeLemma (AC : AbelianCategory ℓ ℓ') where
-  open AbelianCategory AC
-
-  module _
-    (A B C A' B' C' : ob)
-    (asdf : exactHomSeq ?)
-    (f : Hom[ A , B ]) (g : Hom[ B , C ])
-    (f' : Hom[ A' , B' ]) (g' : Hom[ B' , C' ])
-    (a : Hom[ A , A' ]) (b : Hom[ B , B' ]) (c : Hom[ C , C' ])
-    where
-