diff --git a/Cubical/Algebra/Group/Instances/Unit.agda b/Cubical/Algebra/Group/Instances/Unit.agda
index e0a237cf5a..ed6baed8e6 100644
--- a/Cubical/Algebra/Group/Instances/Unit.agda
+++ b/Cubical/Algebra/Group/Instances/Unit.agda
@@ -58,6 +58,23 @@ rightInv (fst rUnitGroupIso) _ = refl
 leftInv (fst rUnitGroupIso) _ = refl
 snd rUnitGroupIso = makeIsGroupHom λ _ _ → refl
 
+-- lifted version
+lUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'}
+  → GroupIso (DirProd (UnitGroup {ℓ}) G) G
+fun (fst lUnitGroupIso^) = snd
+inv (fst lUnitGroupIso^) = tt* ,_
+rightInv (fst lUnitGroupIso^) g = refl
+leftInv (fst lUnitGroupIso^) (tt* , g) = refl
+snd lUnitGroupIso^ = makeIsGroupHom λ _ _ → refl
+
+rUnitGroupIso^ : ∀ {ℓ ℓ'} {G : Group ℓ'}
+  → GroupIso (DirProd G (UnitGroup {ℓ})) G
+fun (fst rUnitGroupIso^) = fst
+inv (fst rUnitGroupIso^) = _, tt*
+rightInv (fst rUnitGroupIso^) g = refl
+leftInv (fst rUnitGroupIso^) (g , tt*) = refl
+snd rUnitGroupIso^ = makeIsGroupHom λ _ _ → refl
+
 lUnitGroupEquiv : {G : Group ℓ} → GroupEquiv (DirProd UnitGroup₀ G) G
 lUnitGroupEquiv = GroupIso→GroupEquiv lUnitGroupIso
 
diff --git a/Cubical/Cohomology/EilenbergMacLane/Base.agda b/Cubical/Cohomology/EilenbergMacLane/Base.agda
index f9cfc50b98..c22bc28635 100644
--- a/Cubical/Cohomology/EilenbergMacLane/Base.agda
+++ b/Cubical/Cohomology/EilenbergMacLane/Base.agda
@@ -4,15 +4,25 @@ module Cubical.Cohomology.EilenbergMacLane.Base where
 
 open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
 open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Properties
 open import Cubical.Homotopy.EilenbergMacLane.Order2
 
 open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Path
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.Isomorphism
+
+open import Cubical.HITs.PropositionalTruncation as PT
 
 open import Cubical.Data.Nat
+open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.Group.Base
 open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.Group.Morphisms
 open import Cubical.Algebra.AbGroup.Base
 open import Cubical.Algebra.Monoid
 open import Cubical.Algebra.Semigroup
@@ -101,6 +111,163 @@ is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomGr n G A)))))) = sq
 ·InvL (isGroup (isAbGroup (snd (coHomGr n G A)))) = lCancelₕ n
 +Comm (isAbGroup (snd (coHomGr n G A))) = commₕ n
 
+-- reduced cohomology groups
+coHomRed : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ') → Type _
+coHomRed n G A = ∥ (A →∙ EM∙ G n) ∥₂
+
+0ₕ∙ : (n : ℕ) {G : AbGroup ℓ} {A : Pointed ℓ'} → coHomRed n G A
+0ₕ∙ n = ∣ (λ _ → 0ₖ n) , refl ∣₂
+
+-- operations
+module _ {n : ℕ} {G : AbGroup ℓ} {A : Pointed ℓ'} where
+  _+ₕ∙_ : coHomRed n G A → coHomRed n G A → coHomRed n G A
+  _+ₕ∙_ = ST.rec2 squash₂
+    λ f g → ∣ (λ x → fst f x +ₖ fst g x)
+            , cong₂ _+ₖ_ (snd f) (snd g) ∙ rUnitₖ n (0ₖ n) ∣₂
+
+  -ₕ∙_ : coHomRed n G A → coHomRed n G A
+  -ₕ∙_ = ST.map λ f → (λ x → -ₖ (fst f x))
+                    , cong -ₖ_ (snd f)
+                    ∙ -0ₖ n
+
+-- group laws
+-- Note that→∙Homogeneous≡ (in Foundations.Pointed.Homogeneous) is
+-- purposely avoided to minimise the size of the proof terms
+module coHomRedAxioms (n : ℕ) {G : AbGroup ℓ} {A : Pointed ℓ'} where
+  commₕ∙ : (x y : coHomRed n G A) → x +ₕ∙ y ≡ y +ₕ∙ x
+  commₕ∙ =
+    ST.elim2 (λ _ _ → isSetPathImplicit)
+      λ f g → cong ∣_∣₂ (ΣPathP (funExt (λ x → commₖ n (fst f x) (fst g x))
+                              , help n _ (sym (snd f)) _ (sym (snd g))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+                    (g0 : EM G n) (g1 : 0ₖ n ≡ g0)
+        → PathP (λ i → commₖ n f0 g0 i ≡ 0ₖ n)
+                 (sym (cong₂ _+ₖ_ f1 g1) ∙ rUnitₖ n (0ₖ n))
+                 (sym (cong₂ _+ₖ_ g1 f1) ∙ rUnitₖ n (0ₖ n))
+    help zero _ _ _ _ =
+      isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> (J> refl)
+    help (suc (suc n)) = J> (J> refl)
+
+  rCancelₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ (-ₕ∙ x)) ≡ 0ₕ∙ n
+  rCancelₕ∙ =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → rCancelₖ n (fst f x)))
+                    , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → rCancelₖ n f0 i ≡ 0ₖ n)
+               (cong₂ _+ₖ_ (sym f1) (cong -ₖ_ (sym f1) ∙ -0ₖ n)
+                                  ∙ rUnitₖ n (0ₖ n))
+               refl
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> (sym (rUnit _) ∙ sym (rUnit _))
+    help (suc (suc n)) = J> (sym (rUnit _) ∙ sym (rUnit _))
+
+  lCancelₕ∙ : (x : coHomRed n G A) → ((-ₕ∙ x) +ₕ∙ x) ≡ 0ₕ∙ n
+  lCancelₕ∙ x = commₕ∙ (-ₕ∙ x) x ∙ rCancelₕ∙ x
+
+  rUnitₕ∙ : (x : coHomRed n G A) → (x +ₕ∙ 0ₕ∙ n) ≡ x
+  rUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+     λ f → cong ∣_∣₂ (ΣPathP ((funExt λ x → rUnitₖ n (fst f x))
+                   , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → rUnitₖ n f0 i ≡ 0ₖ n)
+               (cong (_+ₖ 0ₖ n) (sym f1) ∙ rUnitₖ n (0ₖ n))
+               (sym f1)
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> sym (rUnit refl)
+    help (suc (suc n)) = J> sym (rUnit refl)
+
+  lUnitₕ∙ : (x : coHomRed n G A) → (0ₕ∙ n +ₕ∙ x) ≡ x
+  lUnitₕ∙ = ST.elim (λ _ → isSetPathImplicit)
+    λ f → cong ∣_∣₂ (ΣPathP ((funExt (λ x → lUnitₖ n (fst f x)))
+                  , help n _ (sym (snd f))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+      → PathP (λ i → lUnitₖ n f0 i ≡ 0ₖ n)
+               (cong (0ₖ n +ₖ_) (sym f1) ∙ rUnitₖ n (0ₖ n))
+               (sym f1)
+    help zero _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) = J> sym (rUnit refl)
+    help (suc (suc n)) = J> sym (rUnit refl)
+
+  assocₕ∙ : (x y z : coHomRed n G A) → x +ₕ∙ (y +ₕ∙ z) ≡ (x +ₕ∙ y) +ₕ∙ z
+  assocₕ∙ =
+    ST.elim3 (λ _ _ _ → isSetPathImplicit)
+     λ f g h → cong ∣_∣₂
+       (ΣPathP ((funExt (λ x → assocₖ n (fst f x) (fst g x) (fst h x)))
+      , help n _ (sym (snd f)) _ (sym (snd g)) _ (sym (snd h))))
+    where
+    help : (n : ℕ) (f0 : EM G n) (f1 : 0ₖ n ≡ f0)
+                    (g0 : EM G n) (g1 : 0ₖ n ≡ g0)
+                    (h0 : EM G n) (h1 : 0ₖ n ≡ h0)
+        → PathP (λ i → assocₖ n f0 g0 h0 i ≡ 0ₖ n)
+                 (cong₂ _+ₖ_ (sym f1)
+                  (cong₂ _+ₖ_ (sym g1) (sym h1) ∙ rUnitₖ n (0ₖ n))
+                    ∙ rUnitₖ n (0ₖ n))
+                 (cong₂ _+ₖ_ (cong₂ _+ₖ_ (sym f1) (sym g1)
+                   ∙ rUnitₖ n (0ₖ n)) (sym h1) ∙ rUnitₖ n (0ₖ n))
+    help zero _ _ _ _ _ _ = isOfHLevelPathP' 0 (is-set (snd G) _ _) _ _ .fst
+    help (suc zero) =
+      J> (J> (J> cong (_∙ refl)
+        (cong (cong₂ _+ₖ_ refl) (sym (rUnit refl))
+        ∙ (cong (λ z → cong₂ (+ₖ-syntax {G = G} 1) z (refl {x = 0ₖ {G = G} 1}))
+          (rUnit refl)))))
+    help (suc (suc n)) =
+      J> (J> (J> flipSquare ((sym (rUnit refl))
+        ◁ flipSquare (cong (_∙ refl)
+        (cong (cong₂ _+ₖ_ refl) (sym (rUnit refl))
+        ∙ (cong (λ z → cong₂ (+ₖ-syntax {G = G} (suc (suc n))) z
+                              (refl {x = 0ₖ {G = G} (suc (suc n))}))
+          (rUnit refl)))))))
+
+coHomRedGr : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ') → AbGroup _
+fst (coHomRedGr n G A) = coHomRed n G A
+0g (snd (coHomRedGr n G A)) = 0ₕ∙ n
+AbGroupStr._+_ (snd (coHomRedGr n G A)) = _+ₕ∙_
+- snd (coHomRedGr n G A) = -ₕ∙_
+is-set (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A)))))) = squash₂
+·Assoc (isSemigroup (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A)))))) = coHomRedAxioms.assocₕ∙ n
+·IdR (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A))))) = coHomRedAxioms.rUnitₕ∙ n
+·IdL (isMonoid (isGroup (isAbGroup (snd (coHomRedGr n G A))))) = coHomRedAxioms.lUnitₕ∙ n
+·InvR (isGroup (isAbGroup (snd (coHomRedGr n G A)))) = coHomRedAxioms.rCancelₕ∙ n
+·InvL (isGroup (isAbGroup (snd (coHomRedGr n G A)))) = coHomRedAxioms.lCancelₕ∙ n
++Comm (isAbGroup (snd (coHomRedGr n G A))) = coHomRedAxioms.commₕ∙ n
+
+coHom≅coHomRed : (n : ℕ) (G : AbGroup ℓ) (A : Pointed ℓ')
+  → AbGroupEquiv (coHomGr (suc n) G (fst A)) (coHomRedGr (suc n) G A)
+coHom≅coHomRed n G A =
+  GroupIso→GroupEquiv (invGroupIso main)
+  where
+  con-lem : (n : ℕ) (x : EM G (suc n)) → ∥ x ≡ 0ₖ (suc n) ∥₁
+  con-lem n =
+    EM-raw'-elim G (suc n)
+     (λ _ → isProp→isOfHLevelSuc (suc n) squash₁)
+       (EM-raw'-trivElim G n (λ _ → isProp→isOfHLevelSuc n squash₁)
+         ∣ EM-raw'→EM∙ G (suc n) ∣₁)
+
+  main : GroupIso _ _
+  Iso.fun (fst main) = ST.map fst
+  Iso.inv (fst main) = ST.map λ f → (λ x → f x -ₖ f (pt A))
+                            , rCancelₖ (suc n) (f (pt A))
+  Iso.rightInv (fst main) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → PT.rec (squash₂ _ _)
+        (λ p → cong ∣_∣₂
+          (funExt λ x → cong (λ z → f x +ₖ z)
+            (cong -ₖ_ p ∙ -0ₖ (suc n)) ∙ rUnitₖ (suc n) (f x)))
+        (con-lem n (f (pt A)))
+  Iso.leftInv (fst main) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
+             (funExt λ x → cong (fst f x +ₖ_) (cong -ₖ_ (snd f) ∙ -0ₖ (suc n))
+                          ∙ rUnitₖ (suc n) (fst f x)))
+  snd main =
+    makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+      λ _ _ → refl)
 
 -- ℤ/2 lemmas
 +ₕ≡id-ℤ/2 : ∀ {ℓ}  {A : Type ℓ} (n : ℕ) (x : coHom n ℤ/2 A) → x +ₕ x ≡ 0ₕ n
@@ -128,3 +295,16 @@ fst (coHomHom n f) = coHomFun n f
 snd (coHomHom n f) =
   makeIsGroupHom (ST.elim2 (λ _ _ → isOfHLevelPath 2 squash₂ _ _)
    λ f g → refl)
+
+coHomFun∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
+            (n : ℕ) (f : A →∙ B)
+         → coHomRed n G B → coHomRed n G A
+coHomFun∙ n f = ST.map λ g → g ∘∙ f
+
+coHomHom∙ : ∀ {ℓ''} {A : Pointed ℓ} {B : Pointed ℓ'} {G : AbGroup ℓ''}
+            (n : ℕ) (f : A →∙ B)
+         → AbGroupHom (coHomRedGr n G B) (coHomRedGr n G A)
+fst (coHomHom∙ n f) = coHomFun∙ n f
+snd (coHomHom∙ n f) =
+  makeIsGroupHom (ST.elim2 (λ _ _ → isSetPathImplicit)
+    λ g h → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))
diff --git a/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda
new file mode 100644
index 0000000000..0cd001a289
--- /dev/null
+++ b/Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda
@@ -0,0 +1,282 @@
+{-# OPTIONS --safe --lossy-unification #-}
+
+module Cubical.Cohomology.EilenbergMacLane.EilenbergSteenrod where
+
+open import Cubical.Homotopy.EilenbergMacLane.GroupStructure
+open import Cubical.Homotopy.EilenbergMacLane.Base
+open import Cubical.Homotopy.EilenbergMacLane.Properties
+open import Cubical.Homotopy.EilenbergSteenrod
+
+open import Cubical.Cohomology.EilenbergMacLane.Base
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Pointed
+open import Cubical.Foundations.Pointed.Homogeneous
+open import Cubical.Foundations.GroupoidLaws
+open import Cubical.Foundations.Function
+open import Cubical.Foundations.Equiv
+open import Cubical.Foundations.HLevels
+open import Cubical.Foundations.Isomorphism
+open import Cubical.Foundations.Univalence
+
+open import Cubical.Algebra.Group
+open import Cubical.Algebra.Group.Morphisms
+open import Cubical.Algebra.Group.MorphismProperties
+open import Cubical.Algebra.AbGroup
+open import Cubical.Algebra.AbGroup.Instances.Unit
+open import Cubical.Algebra.Group.Instances.Unit
+
+open import Cubical.HITs.Wedge
+open import Cubical.HITs.Pushout
+open import Cubical.HITs.Susp
+open import Cubical.HITs.Truncation as T
+open import Cubical.HITs.SetTruncation as ST
+open import Cubical.HITs.PropositionalTruncation as PT
+
+open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Nat
+open import Cubical.Data.Bool
+open import Cubical.Data.Sigma
+open import Cubical.Data.Int
+open import Cubical.Data.Unit
+
+open Iso
+open coHomTheory
+
+-- This module verifies the (reduced) Eilenberg-Steenrod axioms for
+-- the following ℤ-indexed cohomology theory
+
+coHomRedℤ : ∀ {ℓ ℓ'} → AbGroup ℓ' → ℤ → Pointed ℓ → AbGroup (ℓ-max ℓ ℓ')
+coHomRedℤ G (pos n) A = coHomRedGr n G A
+coHomRedℤ G (negsuc n) A = UnitAbGroup
+
+module coHomRedℤ {ℓ ℓ'} {G : AbGroup ℓ} where
+  Hmap∙ : (n : ℤ) {A B : Pointed ℓ'}
+     → A →∙ B
+     → AbGroupHom (coHomRedℤ G n B) (coHomRedℤ G n A)
+  Hmap∙ (pos n) = coHomHom∙ n
+  Hmap∙ (negsuc n) f = idGroupHom
+
+  suspMap : (n : ℤ) {A : Pointed ℓ'} →
+      AbGroupHom (coHomRedℤ G (sucℤ n) (Susp (typ A) , north))
+      (coHomRedℤ G n A)
+  fst (suspMap (pos n) {A = A}) =
+    ST.map λ f → (λ x → ΩEM+1→EM n
+                          (sym (snd f)
+                        ∙∙ cong (fst f) (merid x ∙ sym (merid (pt A)))
+                        ∙∙ snd f))
+      , cong (ΩEM+1→EM n)
+             (cong (sym (snd f) ∙∙_∙∙ snd f)
+               (cong (cong (fst f))
+               (rCancel (merid (pt A))))
+           ∙ ∙∙lCancel (snd f))
+      ∙ ΩEM+1→EM-refl n
+  snd (suspMap (pos n) {A = A}) =
+    makeIsGroupHom
+     (ST.elim2 (λ _ _ → isSetPathImplicit)
+      (λ f g → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
+        (funExt λ x → main n _ (sym (snd f)) _ (sym (snd g))
+                      (cong (fst f) (merid x ∙ sym (merid (pt A))))
+                      (cong (fst g) (merid x ∙ sym (merid (pt A))))))))
+    where
+    main : (n : ℕ) (x : EM G (suc n)) (f0 : 0ₖ (suc n) ≡ x)
+           (y : EM G (suc n)) (g0 : 0ₖ (suc n) ≡ y)
+           (f1 : x ≡ x) (g1 : y ≡ y)
+           → ΩEM+1→EM n (sym (cong₂ _+ₖ_ (sym f0) (sym g0)
+                        ∙ rUnitₖ (suc n) (0ₖ (suc n)))
+                        ∙∙ cong₂ _+ₖ_ f1 g1
+                        ∙∙ (cong₂ _+ₖ_ (sym f0) (sym g0)
+                        ∙ rUnitₖ (suc n) (0ₖ (suc n))))
+            ≡ ΩEM+1→EM n (f0 ∙∙ f1 ∙∙ sym f0)
+      +[ n ]ₖ ΩEM+1→EM n (g0 ∙∙ g1 ∙∙ sym g0)
+    main zero = J> (J> λ f g →
+         cong (ΩEM+1→EM {G = G} zero)
+           (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x)
+           (sym (rUnit refl))
+          ∙∙ sym (rUnit _)
+          ∙∙ cong₂+₁ f g)
+         ∙∙ ΩEM+1→EM-hom zero f g
+         ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM zero) (rUnit f))
+                       (cong (ΩEM+1→EM zero) (rUnit g)))
+    main (suc n) =
+      J> (J> λ f g →
+         cong (ΩEM+1→EM {G = G} (suc n))
+           (cong (λ x → sym x ∙∙ cong₂ _+ₖ_ f g ∙∙ x)
+           (sym (rUnit refl))
+          ∙∙ sym (rUnit _)
+          ∙∙ cong₂+₂ n f g)
+         ∙∙ ΩEM+1→EM-hom (suc n) f g
+         ∙∙ cong₂ _+ₖ_ (cong (ΩEM+1→EM (suc n)) (rUnit f))
+                       (cong (ΩEM+1→EM (suc n)) (rUnit g)))
+  fst (suspMap (negsuc n)) _ = tt*
+  snd (suspMap (negsuc n)) = makeIsGroupHom λ _ _ → refl
+
+  toSusp-coHomRed : (n : ℕ) {A : Pointed ℓ'}
+    → A →∙ EM∙ G n → (Susp (typ A) , north) →∙ EM∙ G (suc n)
+  fst (toSusp-coHomRed n f) north = 0ₖ (suc n)
+  fst (toSusp-coHomRed n f) south = 0ₖ (suc n)
+  fst (toSusp-coHomRed n f) (merid a i) = EM→ΩEM+1 n (fst f a) i
+  snd (toSusp-coHomRed n f) = refl
+
+  suspMapIso : (n : ℤ) {A : Pointed ℓ'} →
+      AbGroupIso (coHomRedℤ G (sucℤ n) (Susp (typ A) , north))
+                 (coHomRedℤ G n A)
+  fun (fst (suspMapIso n)) = suspMap n .fst
+  inv (fst (suspMapIso (pos n))) = ST.map (toSusp-coHomRed n)
+  inv (fst (suspMapIso (negsuc zero))) _ = 0ₕ∙ zero
+  inv (fst (suspMapIso (negsuc (suc n)))) _ = tt*
+  rightInv (fst (suspMapIso (pos n) {A = A})) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
+        (funExt λ x → cong (ΩEM+1→EM n)
+                   (sym (rUnit _)
+                   ∙∙ cong-∙ (toSusp-coHomRed n f .fst)
+                       (merid x) (sym (merid (pt A)))
+                   ∙∙ cong (EM→ΩEM+1 n (fst f x) ∙_)
+                           (cong sym (cong (EM→ΩEM+1 n) (snd f)
+                                    ∙ EM→ΩEM+1-0ₖ n))
+                    ∙ sym (rUnit _))
+                   ∙ Iso.leftInv (Iso-EM-ΩEM+1 n) (fst f x)))
+  rightInv (fst (suspMapIso (negsuc zero))) tt* = refl
+  rightInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl
+  leftInv (fst (suspMapIso (pos n) {A = A})) =
+    ST.elim (λ _ → isSetPathImplicit)
+            λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
+              (funExt λ { north → sym (snd f)
+                        ; south → sym (snd f) ∙ cong (fst f) (merid (pt A))
+                        ; (merid a i) j → lem a f j i}))
+    where
+    lem : (a : typ A) (f : Susp∙ (typ A) →∙ EM∙ G (suc n))
+      → PathP (λ i → snd f (~ i) ≡ (sym (snd f) ∙ cong (fst f) (merid (pt A))) i)
+               (EM→ΩEM+1 n (ΩEM+1→EM n (sym (snd f)
+                                      ∙∙ cong (fst f) (toSusp A a)
+                                      ∙∙ snd f)))
+               (cong (fst f) (merid a))
+    lem a f = Iso.rightInv (Iso-EM-ΩEM+1 n) _
+            ◁ λ i j → hcomp (λ k
+              → λ { (i = i1) → fst f (merid a j)
+                   ; (j = i0) → snd f (~ i ∧ k)
+                   ; (j = i1) → compPath-filler'
+                               (sym (snd f)) (cong (fst f) (merid (pt A))) k i})
+                 (fst f (compPath-filler (merid a)
+                         (sym (merid (pt A))) (~ i) j))
+  leftInv (fst (suspMapIso (negsuc zero) {A = A})) =
+    ST.elim (λ _ → isSetPathImplicit)
+            λ f → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _)
+                            (funExt (suspToPropElim (pt A)
+                              (λ _ → hLevelEM G 0 _ _)
+                              (sym (snd f)))))
+  leftInv (fst (suspMapIso (negsuc (suc n)))) tt* = refl
+  snd (suspMapIso n) = suspMap n .snd
+
+satisfies-ES : ∀ {ℓ ℓ'} (G : AbGroup ℓ) → coHomTheory {ℓ'} (coHomRedℤ G)
+Hmap (satisfies-ES G) = coHomRedℤ.Hmap∙
+fst (Suspension (satisfies-ES G)) n = GroupIso→GroupEquiv (coHomRedℤ.suspMapIso n)
+snd (Suspension (satisfies-ES G)) f (pos n) =
+  funExt (ST.elim (λ _ → isSetPathImplicit) λ f
+    → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
+                (funExt λ { north → refl
+                          ; south → refl
+                          ; (merid a i) → refl})))
+snd (Suspension (satisfies-ES G)) f (negsuc zero) =
+  funExt λ {tt* → cong ∣_∣₂ (Σ≡Prop (λ _ → hLevelEM G 0 _ _) refl)}
+snd (Suspension (satisfies-ES G)) f (negsuc (suc n)) = refl
+Exactness (satisfies-ES G) {A = A} {B = B} f (pos n) = isoToPath help
+  where
+  To : (x : coHomRed n G B)
+    → isInKer (coHomHom∙ n f) x
+    → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x
+  To = ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInIm _ _))
+    λ g p → PT.map (λ id → ∣ (λ { (inl x) → 0ₖ n
+                                 ; (inr x) → fst g x
+                                 ; (push a i) → id (~ i) .fst a})
+                            , snd g ∣₂
+                  , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
+                            refl))
+             (Iso.fun ST.PathIdTrunc₀Iso p)
+
+  From : (x : coHomRed n G B)
+    → isInIm (coHomHom∙ n (cfcod (fst f) , refl)) x
+    → isInKer (coHomHom∙ n f) x
+  From =
+    ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
+      λ g → PT.rec (isPropIsInKer _ _)
+        (uncurry (ST.elim (λ _ → isSetΠ λ _ → isProp→isSet (isPropIsInKer _ _))
+          λ h p → PT.rec (squash₂ _ _)
+            (λ id → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
+              (funExt λ x → sym (funExt⁻ (cong fst id) (fst f x))
+                                ∙ cong (fst h) (sym (push x)
+                                              ∙ push (pt A)
+                                              ∙ λ i → inr (snd f i))
+                                ∙ snd h)))
+            (Iso.fun ST.PathIdTrunc₀Iso p)))
+
+  help : Iso (Ker (coHomHom∙ n f))
+             (Im (coHomHom∙ n (cfcod (fst f) , refl)))
+  fun help (x , p) = x , To x p
+  inv help (x , p) = x , From x p
+  rightInv help (x , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl
+  leftInv help (x , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl
+Exactness (satisfies-ES {ℓ} {ℓ'} G) {A = A} {B = B} f (negsuc n) =
+  isoToPath help
+  where
+  help : Iso (Ker (coHomRedℤ.Hmap∙ {G = G} (negsuc n) f))
+             (Im (coHomRedℤ.Hmap∙ {G = G} (negsuc n) {A = B}
+              (cfcod (fst f) , refl)))
+  fun help (tt* , p) = tt* , ∣ tt* , refl ∣₁
+  inv help (tt* , p) = tt* , refl
+  rightInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInIm _ _) refl
+  leftInv help (tt* , p) = Σ≡Prop (λ _ → isPropIsInKer _ _) refl
+Dimension (satisfies-ES G) (pos zero) p = ⊥.rec (p refl)
+fst (Dimension (satisfies-ES G) (pos (suc n)) _) = 0ₕ∙ (suc n)
+snd (Dimension (satisfies-ES G) (pos (suc n)) _) =
+    ST.elim (λ _ → isSetPathImplicit)
+      λ f → T.rec (isProp→isOfHLevelSuc n (squash₂ _ _))
+        (λ p → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM (suc n))
+          (funExt λ { (lift false) → sym p
+                    ; (lift true) → sym (snd f)})))
+        (Iso.fun (PathIdTruncIso (suc n))
+         (isContr→isProp (isConnectedEM {G' = G} (suc n))
+           ∣ fst f (lift false) ∣ ∣ 0ₖ (suc n) ∣))
+Dimension (satisfies-ES G) (negsuc n) _ = isContrUnit*
+BinaryWedge (satisfies-ES G) (pos n) {A = A} {B = B} =
+  GroupIso→GroupEquiv main
+  where
+  main : GroupIso _ _
+  fun (fst main) =
+    ST.rec (isSet× squash₂ squash₂)
+      λ f → ∣ f ∘∙ (inl , refl) ∣₂ , ∣ f ∘∙ (inr , sym (push tt)) ∣₂
+  inv (fst main) =
+    uncurry (ST.rec2 squash₂
+      λ f g → ∣ (λ { (inl x) → fst f x
+                   ; (inr x) → fst g x
+                   ; (push a i) → (snd f ∙ sym (snd g)) i})
+              , snd f ∣₂)
+  rightInv (fst main) =
+    uncurry
+      (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+      λ f g → ΣPathP
+        ((cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))
+       , cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)))
+  leftInv (fst main) =
+    ST.elim (λ _ → isSetPathImplicit)
+     λ f → cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n)
+       (funExt λ { (inl x) → refl
+                 ; (inr x) → refl
+                 ; (push a i) j → lem (snd f) (cong (fst f) (push tt)) j i}))
+    where
+    lem : ∀ {ℓ} {A : Type ℓ} {x y z : A}
+      → (p : x ≡ y) (q : x ≡ z)
+      → (refl ∙ p) ∙ sym (sym q ∙ p) ≡ q
+    lem p q = cong₂ _∙_ (sym (lUnit p)) (symDistr (sym q) p)
+            ∙ assoc p (sym p) q
+            ∙ cong (_∙ q) (rCancel p)
+            ∙ sym (lUnit q)
+  snd main =
+    makeIsGroupHom
+     (ST.elim2 (λ _ _ → isOfHLevelPath 2 (isSet× squash₂ squash₂) _ _)
+     λ f g → ΣPathP
+       (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl)
+      , (cong ∣_∣₂ (→∙Homogeneous≡ (isHomogeneousEM n) refl))))
+BinaryWedge (satisfies-ES G) (negsuc n) {A = A} {B = B} =
+  invGroupEquiv (GroupIso→GroupEquiv lUnitGroupIso^)